Google DeepMind a prezentat AlphaProof Code, un cadru de lucru cu agenți AI conceput pentru verificarea formală a software-ului. Proiectul a fost folosit pentru a demonstra matematic anumite proprietăți de securitate din codul care implementează protocolul de mesagerie Signal.
De la analizarea codului la demonstrații matematice
Verificarea formală încearcă să demonstreze, prin metode matematice, că o implementare respectă proprietățile definite. Nu este același lucru cu o simplă scanare de vulnerabilități sau cu rularea testelor automate. În proiectul descris de Google, experții au stabilit specificațiile, iar agenții AI au contribuit la construirea demonstrațiilor folosind Lean, un limbaj și instrument pentru verificarea teoremelor.
Potrivit companiei, agenții au generat peste șase milioane de linii de cod Lean. Procesul a durat aproximativ patru săptămâni, iar sistemul a evidențiat pentru revizuire umană o mică parte din implementare. Fiecare demonstrație a fost verificată automat de Lean, iar specialiștii au rămas implicați în definirea proprietăților și controlul rezultatelor.
Ce înseamnă pentru securitatea aplicațiilor
Protocolul Signal protejează conversații private, iar verificarea implementării sale este relevantă deoarece o eroare în cod poate compromite garanțiile de securitate chiar dacă proiectarea teoretică este corectă. Metoda ar putea fi explorată și pentru alte sisteme critice, însă extinderea ei necesită cercetare și validare suplimentară.
Citește prezentarea AlphaProof Code de la Google DeepMind. Pentru proiecte de identitate vizuală și decor, vezi și gama de stickere decorative.
