Google DeepMind says its AI agents have mathematically verified that the code underpinning Signal’s encryption meets its core security guarantees.
The research laboratory announced the development on November 10, alongside the introduction of a new framework called AlphaProof Code and a technical paper detailing the findings.
The Signal protocol provides encryption for conversations on Signal, WhatsApp, Messenger and Google Messages. DeepMind researchers examined libsignal, the open-source library that implements Signal’s encryption protocol, tracing its security properties down to the machine code executed on devices.
In a blog post, DeepMind described the exercise as the first formal verification of the code behind such a widely deployed communication protocol. It said no one had previously formally verified the implementation using any method, either with or without artificial intelligence.
The accompanying technical paper outlines the verification process, the methods used and the limitations of the research.
“As AI-driven security threats grow, having the core Signal protocol rigorously verified with automated theorem proving gives us even greater confidence that our code delivers on its privacy guarantees,” Ehren Kret, Signal’s chief technology officer, said in a statement published by DeepMind.
Formal verification uses mathematical methods to prove that software behaves as intended, rather than identifying bugs individually. The approach can eliminate entire categories of potential vulnerabilities but has traditionally been time-consuming and expensive.
The research paper noted that verifying the seL4 microkernel required 20 person-years of work.
AlphaProof Code is designed to simplify the process by dividing the workload between humans and AI agents.
Human researchers identified the security properties that needed to be proven, while the AI agents helped translate Signal’s security objectives into formal specifications. Human experts then reviewed each specification to ensure its accuracy.
