Google DeepMind folosește agenți IA pentru a verifica codul mașină de bază al Signal

Google DeepMind a lansat AlphaProof Code pe 10 noiembrie 2026, folosind echipe de agenți IA pentru a produce demonstrații Lean, verificate automat, ale unor proprietăți de securitate specificate pentru codul compilat libsignal al Signal. Echipa de cercetare, formată din cinci persoane, a finalizat demonstrațiile în patru săptămâni și a publicat specificațiile și materialele de verificare pentru evaluare externă.

Cercetarea a depășit nivelul unui model abstract al proiectării protocolului Signal, ajungând la implementarea sa compilată. Cercetătorii au integrat crate-urile nemodificate libsignal v0.105.4 și SPQR v1.6.0 într-un mic program de linie de comandă, apoi au folosit versiunea standard a rustc pentru a construi un executabil Linux AArch64 cu legare statică. Lucrarea tehnică descrie rezultatul drept primele demonstrații de securitate la nivel de protocol pentru codul nemodificat al unei implementări de protocol criptografic utilizate pe scară largă.

Cum a împărțit AlphaProof Code munca

Cinci cercetători au lucrat timp de patru săptămâni la demonstrații, rulând continuu agenți pe stațiile lor de lucru și elaborând în paralel demonstrații simbolice și computaționale. Potrivit lucrării, agenții au generat aproximativ 6,5 milioane de linii de cod Lean pentru demonstrații verificate automat, bazate pe circa 26.000 de linii de specificații de încredere și de semantică AArch64.

Oamenii au ales proprietățile, au clarificat ambiguitățile și compromisurile de securitate, au verificat specificațiile și au păstrat aprobarea finală. Agenți bazați pe Gemini 4 Carbon și Claude Opus 5.5 au redactat și verificat specificațiile, inclusiv printr-o verificare realizată de o familie diferită de modele. Echipele de agenți Gemini 4 Carbon au generat apoi tot codul demonstrațiilor; niciunul dintre autori nu a scris cod pentru demonstrații. În mod obișnuit, campaniile au folosit între 40 și 80 de agenți pe o singură mașină, timp de 24 până la 72 de ore. Un orchestrator și liderii de echipă coordonau agenții care elaborau demonstrațiile, în timp ce rolurile de arhitect și integrator mențineau baza comună de demonstrații.

Un mecanism de control a acceptat o demonstrație numai după ce nucleul Lean a verificat-o, iar un comparator a confirmat că aceasta corespundea specificației păstrate separat și aprobate de oameni, inclusiv tuturor definițiilor tranzitive, folosind doar axiomele standard Lean. Agenții puteau propune modificări minore atunci când demonstrațiile scoteau la iveală probleme în specificații, însă modificările aduse ipotezelor de încredere necesitau aprobarea oamenilor sau o politică stabilită de utilizator și erau înregistrate împreună cu justificările. Acest mecanism contracarează un risc documentat al demonstrațiilor generate de agenți: o specificație poate fi slăbită indirect prin una dintre definițiile sale.

Acoperirea securității și testarea cu vulnerabilități istorice

Ținta verificată a fost codul pentru sesiunile unu-la-unu, care acoperă handshake-ul PQXDH și schimbul de mesaje prin Triple Ratchet. Cercetătorii raportează două demonstrații independente: zece teoreme simbolice formulate pe baza unor ipoteze criptografice idealizate și o demonstrație computațională care limitează avantajul unui atacator prin ipoteze criptografice și termeni statistici. Proprietățile includ secretul direct, care protejează mesajele anterioare după furtul stării curente; autentificarea; securitatea după compromitere, care privește recuperarea după o compromitere; și secretul handshake-ului. În plus, demonstrația simbolică acoperă secretul handshake-ului în cazul unei compromiteri ulterioare a Diffie–Hellman.

Pentru a verifica dacă specificațiile puteau detecta erori reale, echipa a anulat remedierile pentru două vulnerabilități libsignal remediate anterior, cunoscute drept „stare slabă” și „subgrup mic”, apoi a recompilat binarele modificate. În ambele cazuri, a produs demonstrații Lean care arătau că teorema simbolică de securitate nu era valabilă. Depozitul public de verificare separă materialele computaționale, simbolice, binare comune și cele privind semantica AArch64 și documentează cum pot fi reconstruite și verificate independent demonstrațiile.

Directorul de tehnologie al Signal, Ehren Kret, a declarat că această cercetare „ne oferă și mai multă încredere în garanțiile de confidențialitate ale codului nostru”.

Limite și pașii următori

Garanțiile sunt departe de a certifica aplicațiile Signal în ansamblu. Ele vizează versiunea libsignal-cli a cercetătorilor, rulată ca proces nou; generarea cheilor nu a fost verificată, mesageria de grup a fost lăsată pentru lucrări viitoare, iar canalele laterale și starea pe mai multe dispozitive nu fac parte din scenariul analizat. Primitivele criptografice de nivel jos și anumite rutine de ieșire și de bibliotecă sunt reprezentate prin contracte de încredere. Prin urmare, rezultatul depinde și de aceste contracte, de specificațiile aprobate, de nucleul Lean, de semantica AArch64 și de ipotezele privind primitivele.

Lucrarea precizează că niciuna dintre demonstrații nu dovedește capacitatea de refacere postcuantică pe care SPQR este conceput să o adauge: teorema computațională acoperă atacatorii clasici, în timp ce teoremele simbolice despre ratchet îi permit atacatorului să aleagă cheile SPQR. Modelul computațional restricționează, de asemenea, mai multe acțiuni ale atacatorului și devine lipsit de conținut la valori suficient de mari ale numărului de mesaje și sesiuni. Aceste limite stabilesc ce trebuie să considere de încredere un evaluator extern înainte de a trata demonstrațiile verificate automat drept o garanție de securitate pentru o anumită implementare.

Următorii pași menționați de cercetători sunt consolidarea teoremelor, reducerea bazei de încredere prin verificarea unui număr mai mare de rutine instrumentate și conectarea contractelor criptografice la implementări verificate, precum și extinderea acoperirii la mesageria de grup, expeditorul sigilat și protocoalele de pe server. Obiectivul de a verifica noile versiuni libsignal înainte de lansare este un scop de cercetare, nu o implementare anunțată.

Semnificația imediată a rezultatului constă în diviziunea muncii pe care o ilustrează: agenții s-au ocupat de construirea demonstrațiilor, în timp ce garanțiile se bazează în continuare pe specificații revizuite de oameni și pe ipoteze explicite. Publicarea demonstrațiilor și a procedurilor de verificare le oferă evaluatorilor externi o modalitate de a testa această bază, în timp ce cercetătorii lucrează la integrarea fluxului de lucru în dezvoltarea continuă a libsignal.