Google DeepMind uses AlphaProof Code to formally verify Signal's PQXDH handshake and Triple Ratchet
Google DeepMind researchers used the multi-agent framework AlphaProof Code to formally verify the design of Signal's post-quantum PQXDH handshake and Triple Ratchet as implemented in libsignal. The team claims this is the first time AI has helped produce a proof linking protocol-level security guarantees to a widely used cryptographic implementation. The proof validates libsignal's forward secrecy, authentication, post-compromise security and handshake secrecy. The result is theoretical, since it assumes perfect cryptography and does not guarantee computational secrecy of the bytes. The article reports no vulnerability, no attack and no exploitation, so the operational risk to defenders is limited.
Detalhes técnicos
AlphaProof Code uses a human-guided agent that writes a Lean specification of Signal's security goals, assesses machine code semantics, and produces an agent-authored proof that the Lean kernel checks against that specification. The researchers assigned Gemini Carbon agents to generate Lean code proving the correctness of the libsignal implementation. The agents produced 6.5 million lines of Lean code, and an auditing pass flagged the parts that required human review. The project took four weeks for a team of five people and consumed "quite a few tokens". The article compares this with the roughly 20 person-years needed to verify the seL4 microkernel and the six years spent on the CompCert C compiler. The authors present the work as a step toward a challenge the Beneficial AI Foundation issued in April to verify the Signal protocol and app in Lean. The research paper is titled "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level". According to the article, Swarat Chaudhuri said the next frontier is specification rather than proof, and that the approach should be extended from cryptographic protocols to code in general.
Linha do tempo
-
Google DeepMind uses AlphaProof Code to formally verify Signal's PQXDH handshake and Triple Ratchet
ler a análise desta fonte ocultar
Google DeepMind researchers used the multi-agent framework AlphaProof Code to formally verify the design of Signal's post-quantum PQXDH handshake and Triple Ratchet as implemented in libsignal. The team claims this is the first time AI has helped produce a proof linking protocol-level security guarantees to a widely used cryptographic implementation. The proof validates libsignal's forward secrecy, authentication, post-compromise security and handshake secrecy. The result is theoretical, since it assumes perfect cryptography and does not guarantee computational secrecy of the bytes. The article reports no vulnerability, no attack and no exploitation, so the operational risk to defenders is limited.
Technical Details
AlphaProof Code uses a human-guided agent that writes a Lean specification of Signal's security goals, assesses machine code semantics, and produces an agent-authored proof that the Lean kernel checks against that specification. The researchers assigned Gemini Carbon agents to generate Lean code proving the correctness of the libsignal implementation. The agents produced 6.5 million lines of Lean code, and an auditing pass flagged the parts that required human review. The project took four weeks for a team of five people and consumed "quite a few tokens". The article compares this with the roughly 20 person-years needed to verify the seL4 microkernel and the six years spent on the CompCert C compiler. The authors present the work as a step toward a challenge the Beneficial AI Foundation issued in April to verify the Signal protocol and app in Lean. The research paper is titled "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level". According to the article, Swarat Chaudhuri said the next frontier is specification rather than proof, and that the approach should be extended from cryptographic protocols to code in general.