보안2026. 11. 10. 오후 7:46 UTC·2 분 소요

DeepMind AlphaProof Code, Signal 보안 형식 검증

Google DeepMind가 AlphaProof Code로 Signal의 PQXDH 핸드셰이크와 Triple Ratchet을 형식 검증했다고 밝혔습니다. 프로토콜 보증을 실제 코드와 연결했습니다.

Abstract illustration of a padlock and lines of code representing formal verification of Signal's encrypted messaging protocol. — 이미지: theregister

Google DeepMind 연구진이 Signal 메시징 보안에 대한 형식 검증을 마쳤습니다. 연구진은 AI의 도움으로 프로토콜 수준의 보안 보증을 널리 쓰이는 암호 구현과 연결하는 증명을 만든 것은 처음이라고 주장합니다.

검증에는 형식적 소프트웨어 명세와 검증을 위한 멀티 에이전트 프레임워크 AlphaProof Code가 쓰였습니다. 사람이 이끄는 에이전트가 Lean 명세를 작성하고 머신 코드의 의미론을 평가하며, 에이전트가 쓴 증명을 Lean 커널이 명세에 비추어 확인하는 방식입니다. 이번에 Signal의 양자 내성 PQXDH 핸드셰이크와 Triple Ratchet을 검증했고, libsignal의 전방 비밀성, 인증, 침해 후 보안, 핸드셰이크 비밀성 설계를 입증했습니다.

검증 과정

연구진은 여러 모델을 활용해 Signal의 보안 목표를 사람이 검토한 수학적 명세로 바꿨습니다. 이를 바탕으로 Gemini Carbon 에이전트가 libsignal 구현의 정확성을 증명하는 Lean 코드를 생성했습니다. 에이전트는 약 650만 줄의 Lean 코드를 만들었고, 이후 감사 단계에서 사람의 검토가 필요한 부분을 표시했습니다.

이 결과는 완벽한 암호를 가정한 이론적 성격이며 바이트의 계산적 비밀성을 보장하지는 않습니다. 그럼에도 정확성에 대한 의미 있는 입증입니다. 또한 Beneficial AI Foundation이 4월에 제시한, Signal 프로토콜과 앱을 Lean으로 형식 검증하라는 과제를 향한 한 걸음입니다.

비용과 향후 계획

논문에 따르면 seL4 마이크로커널 검증에는 20인년, CompCert C 컴파일러 개발에는 6년이 걸렸습니다. Signal 검증은 5명이 4주 동안 진행했고 상당한 토큰이 들었다고 합니다.

Google DeepMind 연구 과학자이자 텍사스대 오스틴 교수인 Swarat Chaudhuri는 검증을 확장할 수 있게 된 만큼 이제 무엇을 검증할지가 문제라고 말했습니다. 공격적 AI 역량이 커지는 가운데 전 세계의 취약한 시스템에 이 기술을 적용하는 것이 목표입니다. 다음 단계는 암호 프로토콜을 넘어 일반 코드의 소프트웨어 설계 과정에 적용하는 것이며, 그는 다음 개척지가 증명이 아니라 명세라고 말했습니다.