The Register Post-quantum handshake and Triple Ratchet get a formal security check
Google DeepMind researchers have completed a formal verification of Signal's messaging security, marking what they claim is the first time AI has helped devise a proof that links protocol-level security guarantees to a widely used cryptographic implementation.
They did so using AlphaProof Code, a multi-agent framework for formal software specification and verification. AlphaProof Code relies on a human-guided agent that writes a Lean specification, assesses machine code semantics, and crafts an agent-authored proof that the Lean kernel checks against the specification.
In this instance, AlphaProof Code verified Signal’s post-quantum PQXDH handshake and Triple Ratchet, thereby validating the design of libsignal's forward secrecy, authentication, post-compromise security, and handshake secrecy.
In so doing, the Google/DeepMind team – Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli – has taken a step toward a challenge the Beneficial AI Foundation issued in April to formally verify the Signal protocol and Signal app with Lean.
The AlphaProof Code process involves working with various models to turn Signal's security goals into a human-reviewed mathematical specification. Based on this spec, the researchers assigned Gemini Carbon agents to generate Lean code proving the correctness of the libsignal implementation. After the agents generated 6.5 million lines of Lean code, they undertook an auditing pass and flagged bits that required human review.
The result is theoretical in that it assumes perfect cryptography and doesn't guarantee the computational secrecy of bytes. But it's still a meaningful assertion of correctness.
"It's a system that is fundamentally built for human AI collaboration," said Swarat Chaudhuri, research scientist at Google DeepMind and a professor at the University of Texas at Austin, in an interview with The Register.
Traditionally, said Chaudhuri, you start proving theorems with well-defined problems formulated by a mathematician that get submitted to an AI agent for proof. In this case, the researchers had to figure out what to prove.
"In formal methods, we always had this belief that verification is the hard bit," he said. "There's thirty or forty years of work on how to scale up verification. Now we are able to do that. So now the question is what are we verifying? … That process is fundamentally human-in-the-loop, but we devised a process of trying to scale it up to the extent possible with AI."
As Chaudhuri and his colleagues note in their research paper, "AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level," formal verification used to require heroic efforts. Formally verifying the seL4 microkernel took 20 person-years, while developing the verified CompCert C compiler took six years.
AlphaProof Code, they believe, can drastically reduce the cost of formal verification, though their Signal work still took four weeks for a team of five people and "quite a few tokens."
"The dream is definitely to scale this up," said Chaudhuri. "So you know there's been this rise in offensive AI capabilities, right? There are a lot of insecure systems around the world, and they're going to be exploited.
"So what we really need to do is to apply this kind of technology to code at large all over the world and figure out what is it that you want to guard against? How do you write those properties, how do we specify those properties? That's going to be super important, but we have to figure that out."
Pointing to a related DeepMind project, AlphaProof Nexus, which is focused on mathematics, Chaudhuri said the next step is to apply this technology during the software design process – not just to cryptographic protocols but code in general.
"We really believe that the next frontier is not going to be proof but specification in this kind of research," he said. "And so that's why we took on this domain where that was actually a hard problem. And I think that we have some really good insights now about how to go about this, although not the last word by any means." ®
Get AI news in your inbox
Daily digest of what matters in AI.