DeepMind ИИ-агеннара Signal шифрын кодун түөрт нэдиэлэҕэ математиканан бэрэбиэркэлээтилэр

Google DeepMind AlphaProof Code диэн элбэх агеннаах ИИ-тиһиги көрдөрдө. Кини формальнай верификацияҕа — программа спецификациятыгар суруллубуту чопчу толорорун математиканан дакаастааһыҥҥа — аналлаах. Бастакы улахан тургутуу libsignal буолла — Signal, Google Messages уонна атын сыһыарыылар суруйсууларын көмүскүүр Signal протоколун эталон тутула.

Тугу дакаастаатылар

• Эксперттэр ИИ-моделлары кытта Signal куттал суох буолуутун сыалларын формальнай спецификацияларын суруйдулар уонна хас биирдиилэрин бэрэбиэркэлээтилэр.
• Онтон дакаастыыр агеннар (DeepMind этэринэн, Gemini Carbon олоҕор) Lean тылынан 6,5 мөлүйүөн кэриҥэ устуруока дакаастабылы оҥордулар. Кинилэр 26 тыһыынча кэриҥэ устуруока итэҕэллээх спецификацияҕа уонна AArch64 машина кодун формальнай моделыгар олоҕураллар.
• Дакаастабыллар постквант PQXDH илии тутуһуутун уонна Triple Ratchet-ы хабаллар: иннинээҕи кистэлэҥи, аутентификацияны, компрометация кэнниттэн куттал суох буолууну — уларыйбатах libsignal v0.105.4 скомпиляцияламмыт машина кодугар, протокол схематыгар эрэ буолбакка.
• Үлэ түөрт нэдиэлэ барда. Бэрэбиэркэ быһыытынан, хамаанда арааран ылыллыбыт куопуйаҕа икки дьиҥнээх, өрдөөҥҥүтэ көннөрүллүбүт алҕаһы төнүннэрдэ — тиһик бу версиялар куттал суох буолбатахтарын дакаастаата.

Хааччахтар

Криптография примитивтэрэ уонна хас да библиотека функцията итэҕэллээх диэн ааҕыллан бэрэбиэркэлэммэтилэр. Signal мобильнай сыһыарыыта бүтүннүү верификацияламмата, саҥа уязвимость булуллубата. WIRED бэлиэтииринэн, маннык бэрэбиэркэ улахан кээмэйгэ төһө туһалаах уонна сыаната төһө буоларын өссө биллибэт; Google ороскуотун арыйбата. Lean дакаастабыллара аһаҕастык бэчээттэннилэр.