AlphaProof Code verifica proprietà di Signal nel codice macchina: cosa significa davvero
Lean controlla le dimostrazioni generate; specifiche e modello di minaccia definiscono i limiti del risultato.
Google DeepMind afferma che AlphaProof Code ha verificato proprietà di sicurezza fondamentali dell'implementazione crittografica di Signal a livello di codice macchina. L'annuncio è significativo perché collega il ragionamento formale al codice compilato, invece di fermarsi a una descrizione ideale del protocollo.
Il risultato richiede però un perimetro preciso. Il documento tecnico riguarda proprietà dell'handshake PQXDH e del Triple Ratchet di libsignal, con modelli e ipotesi specificati. Non certifica ogni componente dell'app Signal, qualsiasi dispositivo che la esegua o tutti i possibili attacchi ai messaggi di un utente.
La verifica non si affida alla sicurezza esibita dall'agente
AlphaProof Code utilizza un processo guidato da persone per scrivere specifiche formali in Lean. Dopo l'approvazione umana della specifica, gli agenti costruiscono il codice delle dimostrazioni. Il kernel di Lean verifica che queste stabiliscano effettivamente il risultato richiesto.
La separazione affronta un problema noto del ragionamento generato: una spiegazione scorrevole può essere sbagliata pur sembrando completa. Una dimostrazione controllabile automaticamente deve superare un verificatore distinto. Non si chiede quindi al lettore di considerare la fiducia espressa dall'agente come prova della sicurezza del software.
La specifica rimane decisiva. Dimostrare perfettamente una proprietà sbagliata non stabilisce quella di cui l'utente ha bisogno. Definizioni fidate, modello delle istruzioni macchina e ipotesi sui componenti crittografici costituiscono la base della dimostrazione.
Il lavoro riporta circa 6,5 milioni di righe di prove Lean controllate, sostenute da circa 26.000 righe di specifiche fidate e semantica AArch64. La scala descrive la quantità di lavoro formale generato. Non è un punteggio da confrontare direttamente con le righe dell'applicazione, né indica quante vulnerabilità siano state eliminate.
Il codice compilato riduce una distanza importante
Un protocollo può essere sicuro nel modello astratto e avere un'implementazione che non lo rispetta. Verificare il codice macchina cerca di collegare l'argomento di sicurezza alle istruzioni eseguite dal processore. Il riferimento ad AArch64 è quindi parte sostanziale del risultato.
Gli autori descrivono proprietà di autenticazione, segretezza e recupero sotto i rispettivi modelli di minaccia. Sono risultati rilevanti per un protocollo di messaggistica, ma non vanno riassunti con un'etichetta generica come “impossibile da violare”.
Il documento esclude esplicitamente i canali laterali e alcuni segreti presenti in memoria da uno dei modelli di attaccante. Spiega inoltre limiti relativi alla ripetizione dei messaggi e al rapporto tra i teoremi del ratchet e il recupero post-quantistico. Queste condizioni fanno parte del risultato: mostrano cosa afferma davvero la dimostrazione.
Intorno al protocollo rimane un sistema
I messaggi continuano a passare attraverso applicazioni, sistemi operativi e dispositivi. Un endpoint compromesso può introdurre rischi esterni alla proprietà dimostrata. Anche un errore d'interfaccia o un'azione pericolosa dell'utente non sono automaticamente coperti da un teorema su un componente crittografico compilato.
I ricercatori descrivono anche prove con bug già corretti e poi reintrodotti. Servono a mostrare che il metodo distingue comportamenti errati pertinenti; non dimostrano che in ogni caso sia stata scoperta una nuova vulnerabilità attiva o che ogni errore possibile sia escluso.
Il progresso è una forma di garanzia più ispezionabile per software reale e difficile. L'IA fornisce gran parte del lavoro, mentre un verificatore formale stabilisce l'accettazione. Rimane essenziale che la specifica approvata descriva il rischio importante. Una prova controllata merita fiducia proprio perché è precisa su ciò che dimostra, senza allargarne la conclusione.
