Google DeepMind Uses Agentic AI to Formally Verify Signal Protocol

Google DeepMind researchers used agentic AI to mathematically prove, or formally verify, a number of the Signal protocol's key cryptographic guarantees in a proof of concept completed in four weeks. The work serves as further independent validation of the cryptography that protects communications on platforms like the Signal app, Google Messages and WhatsApp, and it demonstrates DeepMind's formal verification capabilities using a new AI framework called AlphaProof Code.

What the analysis found

The DeepMind analysis did not find any new vulnerabilities in the portions of the Signal protocol it examined. When the researchers used AlphaProof Code on older versions of Signal that contain known and long fixed vulnerabilities, it correctly identified them and showed that the protocol could not be formally verified. The analysis did not formally verify the entire Signal mobile app, and DeepMind researchers describe their findings as one milestone in a larger process. The researchers are releasing the specification and proof they developed for the Signal protocol analysis to aid other formal verification work.

Why formal verification matters

Formal verification uses math to check and validate that software is functioning as intended, which is why proponents have long called it a sort of holy grail in software security. Before the AI era, it was incredibly time consuming for people to describe the characteristics of software they wanted to prove, turn those summaries into formulas and then develop the proof. Agentic AI can significantly cut down the time of that last task, enabling analyses like DeepMind's Signal evaluation. DeepMind's crucial advancements include a human AI collaboration process that lets agents contribute and self correct at almost every phase while still seeking human input and review at key junctures. "We don't want this sort of vibe world where AI is generating the goals and AI is generating the proofs and basically taking tests that are self written," Swarat Chaudhuri, a DeepMind research scientist, tells WIRED. "There's a middle ground."

Open questions about scale and cost

It remains unclear how practical AI aided formal verification will be for widespread use and how effective it can be at securing large amounts of code. DeepMind conducted the Signal analysis free of charge as a research project, and Google declined to share the cost of the analysis or comment on whether it has plans to release a commercial formal verification product or service. Ehren Kret, Signal's chief technology officer, says in a statement that prior formal verification focused on smaller portions of the code, while Google DeepMind's approach enables significant expansion. "As AI driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees," Kret says. Pushmeet Kohli, chief scientist at Google Cloud and DeepMind's vice president of research, says that if the correctness of implementations can now be verified, companies that rely on assurances and worry about bugs could say they can prove those properties. Chaudhuri says DeepMind is excited by the result but that there is a long distance to go before scaling this to all the software of the world.

Sources: Wired