Google DeepMind's AlphaProof Code formally verifies Signal's PQXDH and Triple Ratchet in libsignal, finding no new flaws
Matéria consolidada. Reúne 2 matérias que o Tifon tinha publicado separadamente sobre a mesma história. A IA reescreveu o relatório com o que as 2 fontes trouxeram em 10/11/2026 12:18; os links antigos trazem para cá.
Fontes: theregister.com ↗ wired.com ↗
Google DeepMind used its multi-agent framework AlphaProof Code to formally verify parts of the Signal protocol, the cryptography that also protects Google Messages and WhatsApp (wired.com). The work covers the design of Signal's post-quantum PQXDH handshake and the Triple Ratchet as implemented in libsignal (theregister.com). The researchers claim this is the first time AI has helped produce a proof linking protocol-level security guarantees to a widely used cryptographic implementation (theregister.com). The proof validates forward secrecy, authentication, post-compromise security and handshake secrecy (theregister.com). No new vulnerabilities were found in the parts examined, and the tool also flagged older Signal versions with known, long-fixed flaws as failing verification (wired.com). The result is theoretical, because it assumes perfect cryptography, and the full Signal mobile app was not verified. There is no reported attack or exploitation, so operational risk for defenders is limited (theregister.com, wired.com).
Detalhes técnicos
- Method: a human-guided agent writes a Lean specification of Signal's security goals and assesses machine-code semantics. It then produces an agent-authored proof that the Lean kernel checks against that specification (theregister.com). Gemini Carbon agents generated the Lean code proving the libsignal implementation correct (theregister.com).
- Output and review: the agents produced 6.5 million lines of Lean code, and an auditing pass flagged the parts needing human review (theregister.com). DeepMind stresses a human-AI collaboration model with human review at key junctures (wired.com).
- Effort: the proof-of-concept took four weeks (wired.com, theregister.com) for a team of five, consuming "quite a few tokens" (theregister.com). The Register contrasts this with about 20 person-years for the seL4 microkernel and six years for the CompCert C compiler.
- Prior work: earlier formal verification by the Signal Foundation gave the team a head start (wired.com).
- Context: the work is presented as a step toward a challenge the Beneficial AI Foundation issued in April to verify the Signal protocol and app in Lean (theregister.com). The paper is titled "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level" (theregister.com).
- Limits: the guarantee is theoretical and does not cover computational secrecy of the bytes (theregister.com). Swarat Chaudhuri said the next frontier is specification rather than proof, and that the approach should be extended from cryptographic protocols to code in general (theregister.com).
- Release: DeepMind is releasing the specification and proof to support other verification work (wired.com). Cost and any commercial product plans were not disclosed, and the analysis was run free of charge as research (wired.com).
Remediação
No patch or configuration change is needed. No new vulnerability or CVE is reported. Anyone wishing to use the released specification and proof should obtain them from DeepMind's or the Signal Foundation's official channels, since the sources do not point to a publication location.
Relatos divergentes
- Scope: wired.com describes verification of unspecified "portions" of the Signal protocol and stresses that the whole mobile app was not verified. theregister.com names the verified components (PQXDH and Triple Ratchet in libsignal) and describes machine-code-level verification. The accounts are compatible. The Register is more specific on technical scope, while Wired is more cautious about overall coverage.
- Cost: wired.com says the analysis was run free of charge and no cost was disclosed. theregister.com says only that it consumed "quite a few tokens". Neither gives a figure.
Linha do tempo
-
Google DeepMind uses AlphaProof Code to formally verify Signal's PQXDH handshake and Triple Ratchet
ler a análise desta fonte ocultar
Google DeepMind researchers used the multi-agent framework AlphaProof Code to formally verify the design of Signal's post-quantum PQXDH handshake and Triple Ratchet as implemented in libsignal. The team claims this is the first time AI has helped produce a proof linking protocol-level security guarantees to a widely used cryptographic implementation. The proof validates libsignal's forward secrecy, authentication, post-compromise security and handshake secrecy. The result is theoretical, since it assumes perfect cryptography and does not guarantee computational secrecy of the bytes. The article reports no vulnerability, no attack and no exploitation, so the operational risk to defenders is limited.
Technical Details
AlphaProof Code uses a human-guided agent that writes a Lean specification of Signal's security goals, assesses machine code semantics, and produces an agent-authored proof that the Lean kernel checks against that specification. The researchers assigned Gemini Carbon agents to generate Lean code proving the correctness of the libsignal implementation. The agents produced 6.5 million lines of Lean code, and an auditing pass flagged the parts that required human review. The project took four weeks for a team of five people and consumed "quite a few tokens". The article compares this with the roughly 20 person-years needed to verify the seL4 microkernel and the six years spent on the CompCert C compiler. The authors present the work as a step toward a challenge the Beneficial AI Foundation issued in April to verify the Signal protocol and app in Lean. The research paper is titled "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level". According to the article, Swarat Chaudhuri said the next frontier is specification rather than proof, and that the approach should be extended from cryptographic protocols to code in general.
-
Google DeepMind's AlphaProof Code formally verifies parts of the Signal protocol and finds no new flaws
ler a análise desta fonte ocultar
Google DeepMind used a new AI framework, AlphaProof Code, to formally verify portions of the Signal protocol, the cryptography that also protects messages on Google Messages and WhatsApp. The four-week proof-of-concept found no new vulnerabilities in the parts it examined. Run against older Signal versions with known, long-fixed flaws, the tool identified them and showed those builds could not be formally verified. The scope was limited: the entire Signal mobile app was not verified, and the researchers present the work as one milestone toward scaling AI-assisted formal verification. DeepMind is releasing the specification and proof to support other verification work, and stresses a human-AI collaboration model with human review at key junctures.
Technical Details
- Scope: only selected portions of the Signal protocol were analysed, not the full Signal mobile application.
- Results: no new flaws in the examined portions; the tool correctly flagged older vulnerable versions as failing verification.
- Prior work: earlier formal verification by the Signal Foundation gave the team a head start.
- Cost: the analysis was run free of charge as research; Google did not disclose its cost or any plans for a commercial product.
Remediation
No patch or configuration change is required: the article reports no new vulnerability and names no CVE. The search did not locate DeepMind's or the Signal Foundation's own publication of this work, so the specification and proof should be checked on their official channels before use.