17:35
DeepMind Signal protokolunun qaydalarını süni intellektlə riyazi yoxladı
“Google DeepMind” tədqiqatçıları “Signal” protokolunun əsas şifrələmə qaydalarını riyazi yolla yoxlayıblar. Təhlildə agent kimi özü addım atan süni intellekt sistemi “AlphaProof Code” işlədilib. “Signal” protokolu “Signal” tətbiqindən başqa, “WhatsApp” və “Google Messages” xidmətlərində də başdan sona şifrələmə üçün işləyir.
Formal yoxlama proqramın təhlükəsizliklə bağlı vədlərini riyazi sübutlarla sınaqdan keçirən üsuldur. Adi testlər məlum zəiflikləri axtarır, amma başqa boşluqların olmadığına tam zəmanət vermir. Formal yoxlama protokolun əvvəlcədən müəyyənləşdirilmiş bütün hallarda düzgün işlədiyini sübut etməyə çalışır. “Google DeepMind” bu sübutun hazırlanmasında çox vaxt aparan işlərin böyük hissəsini süni intellektlə sürətləndirib. Araşdırma bütün “Signal” mobil tətbiqini əhatə etməyib. Yalnız protokolun seçilmiş hissələri və əsas şifrələmə qaydaları yoxlanılıb. Təhlil 4 həftə davam edib və araşdırılan hissələrdə yeni təhlükəsizlik boşluğu tapılmayıb. Sistem daha əvvəl boşluqları aşkarlanaraq düzəldilmiş köhnə versiyaları da sınaqdan keçirib. “AlphaProof Code” həmin problemləri düzgün tapıb və bu versiyaların formal yoxlamadan keçmədiyini göstərib. Layihə tez başa çatsa da, iş sıfırdan başlamayıb. Tədqiqatçılar “Signal Foundation”ın daha əvvəl süni intellektsiz apardığı formal yoxlamaların nəticələrindən yararlanıblar. “Google” layihəyə nə qədər hesablama gücü və pul xərcləndiyini açıqlamayıb. Buna görə bu üsulu böyük proqramlara və bütün kod bazasına münasib xərclə tətbiq etməyin mümkün olub-olmadığı hələ bilinmir.
“Google DeepMind” hazırladığı texniki spesifikasiyanı və riyazi sübutu başqa formal yoxlama layihələrinə kömək üçün yayımlayacaq. Prosesin bir çox mərhələsində süni intellekt agentləri nəticələrini düzəldə bilir, vacib nöqtələrdə isə yoxlamanı insanlar aparır. Tədqiqatçılar məqsəd və sübutların yalnız sistem tərəfindən hazırlanmasını düzgün saymırlar. Onlar insanla süni intellektin nəzarətli şəkildə birlikdə işləməsinə üstünlük verirlər. Nəticələr mesajlaşma xidmətlərini qoruyan şifrələmə sisteminin etibarlılığına əlavə müstəqil təsdiq verir. Gələcəkdə eyni üsulla bankların və başqa mühüm xidmətlərin proqramlarını da yoxlamaq olar. Ancaq layihə tədqiqat məqsədilə ödənişsiz aparılıb. “Google” bu texnologiya əsasında kommersiya məhsulu və ya xidmət hazırlayıb-hazırlamadığını açıqlamayıb. Tədqiqatçıların sözlərinə görə, texnologiyanın bütün proqramlarda işlədilməsi üçün hələ uzun yol var.
Formal yoxlama proqramın təhlükəsizliklə bağlı vədlərini riyazi sübutlarla sınaqdan keçirən üsuldur. Adi testlər məlum zəiflikləri axtarır, amma başqa boşluqların olmadığına tam zəmanət vermir. Formal yoxlama protokolun əvvəlcədən müəyyənləşdirilmiş bütün hallarda düzgün işlədiyini sübut etməyə çalışır. “Google DeepMind” bu sübutun hazırlanmasında çox vaxt aparan işlərin böyük hissəsini süni intellektlə sürətləndirib. Araşdırma bütün “Signal” mobil tətbiqini əhatə etməyib. Yalnız protokolun seçilmiş hissələri və əsas şifrələmə qaydaları yoxlanılıb. Təhlil 4 həftə davam edib və araşdırılan hissələrdə yeni təhlükəsizlik boşluğu tapılmayıb. Sistem daha əvvəl boşluqları aşkarlanaraq düzəldilmiş köhnə versiyaları da sınaqdan keçirib. “AlphaProof Code” həmin problemləri düzgün tapıb və bu versiyaların formal yoxlamadan keçmədiyini göstərib. Layihə tez başa çatsa da, iş sıfırdan başlamayıb. Tədqiqatçılar “Signal Foundation”ın daha əvvəl süni intellektsiz apardığı formal yoxlamaların nəticələrindən yararlanıblar. “Google” layihəyə nə qədər hesablama gücü və pul xərcləndiyini açıqlamayıb. Buna görə bu üsulu böyük proqramlara və bütün kod bazasına münasib xərclə tətbiq etməyin mümkün olub-olmadığı hələ bilinmir. “Google DeepMind” hazırladığı texniki spesifikasiyanı və riyazi sübutu başqa formal yoxlama layihələrinə kömək üçün yayımlayacaq. Prosesin bir çox mərhələsində süni intellekt agentləri nəticələrini düzəldə bilir, vacib nöqtələrdə isə yoxlamanı insanlar aparır. Tədqiqatçılar məqsəd və sübutların yalnız sistem tərəfindən hazırlanmasını düzgün saymırlar. Onlar insanla süni intellektin nəzarətli şəkildə birlikdə işləməsinə üstünlük verirlər. Nəticələr mesajlaşma xidmətlərini qoruyan şifrələmə sisteminin etibarlılığına əlavə müstəqil təsdiq verir. Gələcəkdə eyni üsulla bankların və başqa mühüm xidmətlərin proqramlarını da yoxlamaq olar. Ancaq layihə tədqiqat məqsədilə ödənişsiz aparılıb. “Google” bu texnologiya əsasında kommersiya məhsulu və ya xidmət hazırlayıb-hazırlamadığını açıqlamayıb. Tədqiqatçıların sözlərinə görə, texnologiyanın bütün proqramlarda işlədilməsi üçün hələ uzun yol var.