Criptarea Signal a trecut o demonstrație AI de 6,5 milioane de rânduri

Codul de criptare al Signal are acum ceva ce aproape niciun software folosit pe scară largă nu poate revendica: o demonstrație matematică a faptului că face ceea ce promite. O echipă de agenți AI a analizat libsignal, biblioteca pe care se bazează protocolul Signal, și a demonstrat că discuțiile unu-la-unu rămân secrete, confirmă identitatea interlocutorului și îl țin din nou la distanță pe atacator după furtul unei chei. Nu au descoperit nicio vulnerabilitate nouă.

Importanța rezultatului depășește cu mult comunitatea de utilizatori Signal. Protocolul este standardul global pentru mesageria cu criptare end-to-end, iar variante ale sale protejează conversațiile din WhatsApp, Messenger și Google Messages. Verificarea la acest nivel a codului real, deja livrat utilizatorilor, dura atât de mult încât aproape nimeni nu încerca: una dintre cele mai mari reușite din domeniu, un nucleu de sistem de operare verificat, a necesitat douăzeci de ani de muncă ai unei persoane. Proiectul de față a durat patru săptămâni.

Instrumentul, dezvoltat de Google DeepMind, se numește AlphaProof Code. Mai întâi, experți umani și modele AI au transformat obiectivele de securitate ale Signal în enunțuri formale în Lean, un limbaj de programare creat pentru demonstrații matematice, iar fiecare enunț a fost verificat de o persoană. Apoi, echipe de 40 până la 80 de agenți, susținute de Gemini Carbon, au scris demonstrațiile, lucrând câte 24 până la 72 de ore la rând pe o singură mașină. Rezultatul însumează aproximativ 6,5 milioane de linii de Lean.

Nu e nevoie ca cineva să aibă încredere în aceste milioane de linii. Nucleul Lean verifică fiecare pas și respinge orice demonstrație care nu este validă, așa că nu contează ce model a scris-o sau de câte ori a greșit pe parcurs. Încrederea necesară se limitează la elemente mult mai restrânse: aproximativ 26.000 de linii de specificații și un model al modului în care un procesor ARM execută codul.

Demonstrațiile acoperă componentele Signal care protejează o conversație: mecanismul de inițiere PQXDH, care configurează o discuție, și Triple Ratchet, care schimbă cheia pentru fiecare mesaj, inclusiv nivelul post-cuantic, conceput să reziste viitoarelor calculatoare cuantice. În practică, asta înseamnă că furtul cheilor aflate în acel moment pe telefon nu oferă acces la mesajele mai vechi, iar hoțul își pierde din nou accesul după ce cele două părți fac schimb de chei noi.

Pentru a demonstra că sistemul poate deosebi codul sigur de cel vulnerabil, cercetătorii au reintrodus în libsignal două erori mai vechi, deja remediate. Din cauza uneia dintre ele, biblioteca păstra o copie a unei chei secrete pe care ar fi trebuit să o șteargă. În ambele cazuri, AlphaProof Code a produs o demonstrație verificată automat, care arăta că versiunea cu erori nu era sigură.

Există limite clare. Demonstrația acoperă doar sesiunile unu-la-unu, iar DeepMind menționează mesageria de grup printre direcțiile de lucru viitoare. Rezultatul se aplică versiunii 0.105.4 a libsignal, compilată cu compilatorul Rust standard pentru ARM Linux în interiorul unui program de test simplu, nu aplicațiilor Signal complete pentru iPhone, Android sau desktop. Se presupune că primitivele criptografice de nivel inferior sunt sigure; ele nu au fost demonstrate ca atare. O eroare în specificațiile aprobate de oameni ar slăbi garanția, iar WhatsApp și celelalte aplicații folosesc propriile versiuni ale protocolului, astfel că rezultatul nu li se aplică automat. Google a refuzat, de asemenea, să-i spună publicației Wired cât a costat analiza sau dacă intenționează să o ofere contra cost, ca serviciu.

Signal a salutat rezultatul. „Pe măsură ce amenințările de securitate bazate pe AI se înmulțesc, verificarea riguroasă a implementării protocolului Signal ne oferă și mai multă încredere în garanțiile de confidențialitate ale codului nostru”, a declarat într-un comunicat Ehren Kret, directorul tehnic al Signal. Swarat Chaudhuri, cercetător la DeepMind, a fost mai rezervat: el a declarat pentru Wired că mai este „un drum lung” până când metoda va putea fi extinsă „la toate programele informatice din lume”.

Pentru cei care folosesc Signal, nu e nevoie să instaleze nimic și nici să schimbe vreo setare. Demonstrația se referă la codul care se află deja în aplicație.

DeepMind a publicat rezultatele pe 10 noiembrie, împreună cu o lucrare tehnică, și a făcut publice specificațiile și demonstrațiile, cu sursă deschisă, pe GitHub. Compania descrie proiectul Signal drept o etapă importantă în direcția unei provocări majore de verificare formală, lansate în aprilie, și menționează firmware-ul dispozitivelor medicale și software-ul rețelelor electrice printre sistemele pe care vrea să le verifice în continuare.

Chaudhuri a trasat și o limită privind cât de mult din această muncă ar trebui lăsat în seama mașinilor. „Nu ne dorim o lume de tipul «vibe», în care AI-ul stabilește obiectivele și tot AI-ul produce demonstrațiile”, a declarat el pentru Wired. Oamenii decid în continuare ce înseamnă securitate, iar AI-ul doar demonstrează că aceasta este respectată.

Etichete: securitate cibernetică, Google DeepMind, AlphaProof Code, criptare end-to-end, libsignal, Signal