Google DeepMind AI-ды Signal-дың криптографиялық кодын тексеру үшін пайдаланады

2026 жылғы 10 қарашада Google DeepMind Signal криптографиялық протоколының негізгі қауіпсіздік механизмдерін математикалық тексеруге көмектескен AI агенттерінің зерттеу нәтижелерін ұсынды. Бұл жұмыс үшін ғалымдар AlphaProof Code жүйесін әзірледі, ол үлкен тілдік модельдерді, формальды тексеру құралдарын және мамандардың бақылауын біріктіреді. Зерттеушілердің айтуынша, олар алғаш рет кеңінен қолданылатын криптографиялық протоколдың қауіпсіздік дәлелдерін оның өзгертілмеген іске асырылуының машина кодымен байланыстыра алды.

Жоба төрт аптаға созылды және бес зерттеушінің қатысуын талап етті. Осы уақыт ішінде Gemini 4 Carbon негізіндегі агенттер Lean тілінде шамамен 6,5 миллион жол дәлелдер жасады, олар осы жүйенің математикалық ядросымен тексерілді. Нәтижелер техникалық құжаттамамен және бастапқы кодпен бірге жарияланды, осылайша басқа мамандар тексеруді зерттеп, қайталауға мүмкіндік алды.

Зерттеушілер тексерген Signal қауіпсіздік механизмдері

Зерттеудің негізгі назары Signal криптографиялық протоколын жүзеге асыратын libsignal кітапханасына бағытталды. Бұл протокол тек аттас мессенджерде ғана емес, сонымен қатар WhatsApp және Google Messages сияқты басқа байланыс қызметтерінде де хабарламаларды шифрлауды қамтамасыз етеді. Зерттеушілер екі маңызды механизмді қарастырды: байланыс орнату кезінде қауіпсіз кілт алмасуға жауапты PQXDH және сөйлесу барысында криптографиялық кілттерді жаңартатын Triple Ratchet.

Тексеру бірнеше қауіпсіздік қасиеттерін қамтыды. Олардың ішінде хабарламалардың құпиялылығы мен түпнұсқалығы, кейінгі кілттің бұзылуы жағдайында алдыңғы хат алмасуды қорғау және белгілі бір бұзылу түрлерінен кейінгі алмасулардың қауіпсіздігін қалпына келтіру мүмкіндігі болды. Зерттеушілер сондай-ақ кванттық қауіп-қатерлерді ескере отырып, байланыс орнату процедурасының нақты қауіпсіздік қасиеттерін талдады.

Протоколдың математикалық моделін дәстүрлі тексеруден айырмашылығы, DeepMind компиляцияланған іске асыруды тікелей зерттеді. Бұл үшін зерттеушілер libsignal 0.105.4 нұсқасын пайдаланып, Arm процессорларында қолданылатын AArch64 архитектурасына арналған орындалатын кодты зерттеді. Бұл тәсіл тек криптографиялық схеманы ғана емес, оның бағдарламалық қамтамасыз ету іске асырылуының көрсетілген қауіпсіздік қасиеттеріне қаншалықты сәйкес келетінін де тексеруге мүмкіндік береді.

AlphaProof Code бағдарламаларды тексеру үшін AI-ды қалай қолданады

Формальды тексеру әдеттегі тестілеуден айырмашылығы, жеке сценарийлерді тексерудің орнына, әзірлеушілер белгілі бір талаптардың орындалуын математикалық дәлелдейді. Мысалы, рұқсат етілмеген қатысушы хабарламаның мазмұнына қол жеткізбеуі керек деген шартты құруға болады, содан кейін бұл шарт модель ұсынған барлық жағдайларда орындалатыны тексеріледі.

AlphaProof Code жүйесінде бұл процесс тексерілетін қасиеттердің нақты математикалық сипаттамасы болып табылатын формальды спецификацияны жасаудан басталады. AI агенттері қауіпсіздік талаптарын Lean тіліндегі өрнектерге аударуға көмектеседі, бірақ соңғы тұжырымдар адамдармен тексеріліп, мақұлданады. Осыдан кейін басқа агенттер тобы дәлелдер жасайды, оларды Lean жүйесі олардың қалай алынғанына қарамастан тәуелсіз тексереді.

Зерттеу барысында шамамен 6,5 миллион жол машинамен тексерілген дәлелдер дайындалды. Олар шамамен 26,000 жол сенімді спецификацияларға және процессор архитектурасының жұмыс сипаттамаларына негізделді. Жүйе сондай-ақ қосымша адам тексеруін талап ететін аймақтарды белгіледі, бұл зерттеушілерге ең маңызды болжамдарға назар аударуға мүмкіндік берді.

AlphaProof Code жүйесінің нақты мәселелерді анықтау қабілетін тексеру үшін команда кодтың жеке нұсқаларына бұрын түзетілген екі осалдықты қайта енгізді. Екі жағдайда да жүйе көрсетілген қауіпсіздік қасиеттерінің бұзылуын математикалық түрде көрсете алды. Бұл эксперимент құралдың іске асырудың дұрыстығын растау ғана емес, сонымен қатар белгілі бір қателерді анықтау қабілетін де көрсетті.

Бұл Signal толық қауіпсіз дегенді білдіре ме

Нәтижелерге қарамастан, зерттеу Signal жүйесінің толық қамтылуын білдірмейді. Зерттеушілер екі қатысушы арасындағы хабар алмасу үшін криптографиялық протоколдың нақты іске асырылуын тексерді, мобильді қосымшаның барлық функцияларын емес. Топтық чаттар, құрылғы мен сервер жұмысының нақты ерекшеліктері, сондай-ақ кейбір бағдарламалық шабуылдар түрлері бұл жұмыстың ауқымынан тыс қалды.

Сонымен қатар, математикалық дәлелдер қолданылатын криптографиялық алгоритмдердің қауіпсіздігі туралы белгілі бір болжамдар негізінде жарамды. Зерттеушілер екі модельді қолданды: криптографиялық операциялар идеалдандырылған түрде қарастырылатын символдық және берілген жағдайларда шабуылдаушылардың мүмкіндіктерін ескеретін есептеу моделі. Алайда, есептеу дәлелі кванттық қарсыластарға таралмайды және Triple Ratchet-тің кейбір посткванттық қасиеттері әлі де жеке тексеруді қажет етеді.

Зерттеушілер ағымдағы іске асырудың тексерілген компоненттерінде жаңа осалдықтарды таппады. Алайда, бұл қосымшаның басқа бөліктеріндегі мәселелерді жоққа шығармайды және барлық жағдайларда жүйенің қауіпсіздігін қамтамасыз етпейді.

Зерттеу бағдарламалық қамтамасыз етуді әзірлеу үшін неге маңызды

Google DeepMind мәліметі бойынша, AlphaProof Code күрделі бағдарламалық қамтамасыз етудің формальды тексеруіне қажетті еңбекті айтарлықтай азайтуы мүмкін. Бұрын мұндай жобалар мамандардың жылдар бойы жұмысын талап ететін: мысалы, seL4 операциялық жүйесінің микроядросының формальды тексеруі шамамен 20 адам-жыл қажет етті, ал тексерілген CompCert C компиляторын әзірлеу алты жылға созылды.

Жаңа тәсілдің ең еңбекқор бөлігі дәлелдерді генерациялау емес, бағдарламалық қамтамасыз етудің қандай қасиеттерін тексеру керектігін анықтау болды. Адам мен AI-дың ынтымақтастығы дәлелдерді дайындауды жеделдетті, бірақ математикалық модельдерді және олардың шектеулерін сараптамалық бағалауды қажет етуді жойған жоқ.

Болашақта Google DeepMind осындай әдістерді басқа күрделі бағдарламалық жүйелерге, соның ішінде банк бағдарламалық қамтамасыз етуіне және маңызды инфрақұрылымға қолдануды жоспарлап отыр. Алайда, технологияны үлкен код базаларына масштабтау мүмкіндігі, есептеулердің құны және қажетті адам бақылауының көлемі ашық сұрақтар болып қала береді.