Google DeepMind researchers used agent AI to mathematically prove, or “formally verify,” several of the Signal protocol’s key cryptographic guarantees, a landmark development for widely used cryptography and AI itself.
Completed as a kind of proof-of-concept project in just four weeks, the work is significant in two ways. It serves as an additional independent validation of the cryptography that protects massive amounts of global communications on platforms like the Signal app, Google Messages, and WhatsApp. And it demonstrates Google DeepMind’s formal verification capabilities using a new AI framework called AlphaProof Code.
More generally, AI-assisted formal verification is having its moment, but it’s unclear how practical it will be for widespread use and how effective it can be at protecting large amounts of code. Proponents of formal verification have long referred to it as a kind of holy grail in software security, because it uses mathematics to check and validate that software works as intended; in other words, it has no critical vulnerabilities.
Before the age of AI, it took people a long time to describe the features of the software they wanted to test, convert these summaries into formulas, and then develop the test. Agent AI can significantly reduce the time of this latter project, enabling analyzes such as DeepMind signal evaluation. But even this analysis was limited in scope (for example, it did not formally verify the entire Signal mobile app) and DeepMind researchers emphasize that their findings are just one milestone in a broader process.
“We’re very excited about this result, but there’s a long way to go before we can scale this to all the software in the world, and we want to do that,” Swarat Chaudhuri, a research scientist at DeepMind, tells WIRED.
DeepMind’s analysis did not find any new vulnerabilities in the parts of the Signal protocol it analyzed, but when researchers used AlphaProof Code on older versions of Signal that contain known and long-fixed vulnerabilities, they correctly identified them and showed that the protocol could not be formally verified. The researchers are publishing the specification and test they developed for the analysis of the Signal protocol to aid further formal verification work.
