Google DeepMind 称用 AI 验证 Signal 协议底层代码的关键安全性质

Big achievement by Google DeepMind for showing that an AI system that proves a software is secure mathematically, with no need to trust the AI. > They just used AI agents to mathematically prove that Signal’s real running code keeps messages secret. Google's AI agents wrote 6.5M lines of math proving Signal’s compiled code keeps chats private. checked at the level of the instructions a processor actually runs. The lab says no one had done this before for any widely used protocol. > Normal testing tries many inputs and hopes to hit the bad one. A proof shows the security rules hold in every case, and the Lean proof checker rejects any wrong step the AI writes. > Real bugs often creep in when a design gets turned into code, so checking the processor-level code closes that gap. The Rust compiler isn’t trusted either, so a mistake by the compiler would also get caught. > The work took 4 weeks, where expert teams used to need years. Teams of 40 to 80 Gemini Carbon agents wrote about 6.5M lines of Lean, while humans set the security goals and reviewed the 1% the agents flagged. > To check that the system can’t just approve any code, the researchers put 2 old, already fixed Signal bugs back into a copy. Both times it produced a machine-checked proof that the code was insecure. > The bigger shift is cost, now that AI can produce machine-checked proofs in weeks, rather than years-long projects and become routine checks for device firmware, power grid software and other critical code.

Announcing a major milestone achieved by my team @GoogleDeepMind: we have proven key security properties of the machine code underlying the Signal messaging protocol. This is the first time the actual production code of a widely deployed protocol has been formally verified – by any method, with or without AI – and at this depth. More than a research breakthrough, it’s a prime example of how frontier AI can be a force multiplier to counter the speed and scale of modern cyber threats. Formal verification offers a higher standard of security; however, it’s extremely complex and time consuming, which is why in many cases it’s considered to be impractical. Similar efforts could take teams decades of combined effort. We did it in a month’s time. Using AlphaProof Code, Google DeepMind's new agentic framework for formal verification that runs on LLMs including Gemini Carbon, we verified the Signal protocol down to the actual code running on devices.  This milestone lays the groundwork for a future in which vital systems, from medical device firmware to power grid software, ship with mathematical proof that their protections work. Reaching that future will take continued research from our community. In that spirit, we're open-sourcing our formal specifications and verification artifacts so others can build on this work. On a personal note, this moment is of deep significance to me. I started my own research journey more than two decades ago as an intern working on checking the consistency of complex software systems. Seeing this grand challenge made practical with modern AI is extraordinary. I'm extremely proud of my team members: Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger,  Karn Seth, Jonathan Katz, and Charles Sutton for taking on this grand challenge and delivering, and grateful to the Signal team for their partnership. https://t.co/kN1eRYQ8fF