Google DeepMind agent əsaslı süni intellektlə Signal protokolunu formal yoxlayıb

Google DeepMind tədqiqatçıları agent əsaslı süni intellektdən istifadə edərək Signal protokolunun bir sıra əsas kriptografik zəmanətlərini riyazi yolla sübut ediblər, yəni formal yoxlayıblar. Dörd həftədə tamamlanan bu iş konsept sübutu xarakteri daşıyır. İş iki baxımdan əhəmiyyətlidir: Signal tətbiqi, Google Messages və WhatsApp kimi platformalarda geniş yayılmış kriptografiyanın əlavə müstəqil təsdiqini verir və DeepMind-ın AlphaProof Code adlı yeni süni intellekt çərçivəsi ilə formal yoxlama imkanlarını nümayiş etdirir.

Analiz nə göstərdi

DeepMind analizi yoxladığı Signal protokol hissələrində heç bir yeni zəiflik tapmayıb. Tədqiqatçılar AlphaProof Code-u məlum və çoxdan düzəldilmiş zəifliklər saxlayan köhnə Signal versiyalarında istifadə etdikdə, alət onları düzgün müəyyən edib və protokolun formal yoxlana bilmədiyini göstərib. Analiz Signal-ın bütün mobil tətbiqini formal yoxlamayıb və DeepMind tədqiqatçıları nəticələrini daha böyük bir prosesin yalnız bir mərhələsi adlandırırlar. Tədqiqatçılar Signal protokolunun analizi üçün hazırladıqları spesifikasiya və sübutu digər formal yoxlama işlərinə kömək etmək üçün yayımlayırlar.

Formal yoxlama niyə vacibdir

Formal yoxlama riyaziyyatdan istifadə edərək proqram təminatının nəzərdə tutulduğu kimi işlədiyini, yəni kritik zəifliklərinin olmadığını yoxlayır; buna görə də tərəfdarları onu çoxdan proqram təminatı təhlükəsizliyinin bir növ müqəddəs qədəhi adlandırırlar. Süni intellekt dövründən əvvəl insanlar üçün sübut etmək istədikləri xüsusiyyətləri təsvir etmək, bu xülasələri düsturlara çevirmək və sonra sübutu hazırlamaq son dərəcə vaxt aparırdı. Agent əsaslı süni intellekt bu son mərhələnin vaxtını xeyli azaldır və DeepMind-ın Signal qiymətləndirməsi kimi analizlərə imkan verir. DeepMind-ın əsas irəliləyişlərindən biri insan və süni intellektin əməkdaşlıq prosesidir: agentlər demək olar ki, hər mərhələdə töhfə verə və özlərini düzəldə bilirlər, lakin əsas nöqtələrdə insan müdaxiləsi və rəyi tələb olunur. "Biz süni intellektin hədəfləri yaratdığı, sübutları özü hazırladığı və əsasən özünün yazdığı testlərdən keçdiyi belə bir vibe dünyası istəmirik" deyir DeepMind-ın tədqiqatçı alimi Swarat Chaudhuri WIRED-a. "Ortada bir yol var".

Miqyas və xərc ilə bağlı açıq suallar

Süni intellektlə dəstəklənən formal yoxlamanın geniş istifadə üçün nə dərəcədə praktik olacağı və böyük həcmdə kodu qorumaqda nə qədər effektiv ola biləcəyi hələ aydın deyil. DeepMind Signal analizini tədqiqat layihəsi kimi ödənişsiz aparıb, Google isə analizin dəyərini paylaşmaqdan və kommersiya formal yoxlama məhsulu və ya xidməti buraxmaq planları barədə şərh verməkdən imtina edib. Signal-ın baş texnologiya direktoru Ehren Kret bəyanatda deyir ki, əvvəlki formal yoxlama kodun daha kiçik hissələrinə fokuslanırdı, Google DeepMind-ın yanaşması isə əhəmiyyətli genişlənməyə imkan verir. "Süni intellektlə bağlı təhlükəsizlik təhdidləri artdıqca, Signal protokolunun tətbiqinin ciddi yoxlanması kodumuzun məxfilik zəmanətlərinə inamımızı daha da artırır" deyir Kret. Google Cloud-un baş elmi işçisi və DeepMind-ın tədqiqat üzrə vitse-prezidenti Pushmeet Kohli deyir ki, əgər tətbiqlərin düzgünlüyü indi yoxlana bilirsə, zəmanətlərə güvənən və səhvlərdən narahat olan şirkətlər bu xassələri sübut edə bildiklərini deyə bilərlər. Chaudhuri deyir ki, DeepMind nəticədən məmnundur, lakin bunu dünyanın bütün proqram təminatına miqyaslandırmaq üçün hələ uzun yol var.

Mənbələr: Wired