DeepMind's AI Mathematically Verifies Signal Messenger's Security Code

At a glance

Google DeepMind's AI agent AlphaProof Code formally verified core security properties of the Signal messaging protocol at the machine-code level. Formal verification, which uses mathematics to prove that code behaves as specified, has been costly and used only in limited areas until now.

Key points

1. 1

   DeepMind says the AI produced over 6 million lines of Lean proof code and finished the work in four weeks.

2. 2

   Human experts reviewed only about 1% of the whole codebase, and they took part in turning security goals into mathematical specifications.

3. 3

   The verified properties included protection of past conversations, sender authentication, and recovery after a device is compromised.

4. 4

   The published proof materials can serve as a starting point for researchers and security developers to apply the method to other protocols.

Why it matters

It opens a way to confirm the security of everyday services like messaging and financial verification with proofs rather than only trust.

Also reported by

• WIREDA New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure
• Ars TechnicaSignal’s encryption just passed an AI-powered mathematical checkup
• Google DeepMind blogIntroducing AlphaProof Code: a breakthrough in verifying complex software at depth
• 뉴스N연합구글 딥마인드 '알파프루프 코드', 시그널 암호화 프로토콜 기계어 수준 정식 검증 성공…보안 인증 시장 재편 압력 가시화
• Unite.AIGoogle DeepMind, AI 에이전트로 Signal의 핵심 기계어 코드 검증
• GeekNewsAlphaProof Code - Signal 암호화 구현을 기계어 수준에서 형식 검증
• knpp.co.kr구글 딥마인드 '알파프루프 코드', 시그널 암호화 프로토콜 기계어 수준 정식 검증 성공…보안 인증 시장 재편 압력 가시화
• VOI.ID구글 딥마인드, 신호 및 WhatsApp 암호화 프로토콜의 보안을 입증