AlphaProof Code: an AI proves security properties of Signal's code
· BehindLines newsroom
Google DeepMind researchers say they used artificial intelligence agents to prove several security guarantees of the real code on which the Signal messaging protocol runs. According to DeepMind's post, this would be the first formal verification, at this level of detail and by an AI, of a widely used cryptographic protocol; The Register reports that this is what the researchers claim.
A team method
The system is called AlphaProof Code. According to DeepMind, human experts and several language models first turn Signal's security goals into mathematical specifications, which people review one at a time. Agents then write the proofs in Lean, a language whose checker automatically validates the demonstrations. According to The Register, the agents produced 6.5 million lines of Lean; DeepMind mentions more than 6 million. They then audited those proofs and flagged about 1% of the code for a second human look, which DeepMind says saves a great deal of time.
What was proved
The proofs target the compiled code, not only the theoretical outline of the protocol, DeepMind stresses. They cover, for example, the protection of messages before and after a device is briefly compromised. The Register also mentions forward secrecy, authentication and the secrecy of the initial key exchange. To make sure the method can tell correct code from buggy code, the team put two real flaws, since fixed, back into a quarantined copy of Signal's code; each time, the system delivered a machine-validated proof that this version was not secure.
Acknowledged limits
The Register specifies that the result remains theoretical: it starts from cryptography assumed to be perfect and does not secure the computational secrecy of bytes. According to the authors cited by the outlet, the work took five people four weeks and used "quite a few tokens". They recall that verifying the seL4 microkernel cost 20 person-years and that the CompCert compiler needed six years of development.
Ehren Kret, Signal's chief technology officer, says in DeepMind's post that this approach clearly extends the scope of formal verification. Swarat Chaudhuri, one of the researchers, tells The Register that the next difficulty will be deciding what to specify, more than producing the proofs.
Why it matters
DeepMind notes that real vulnerabilities often sit in the gap between a protocol's design and its implementation, a gap these proofs aim to close. The company sees a basis for securing other vital systems, such as medical device firmware or power grid software, while specifying that going to a larger scale still requires research.