Google DeepMind는 Signal 메시징 프로토콜의 참조 구현인 libsignal에서 주요 보안 속성을 수학적으로 검증하는 데 AlphaProof Code를 사용했다고 밝혔다. 작업에는 4주가 걸렸다. DeepMind에 따르면 비슷한 검증 작업은 과거 전문가 팀이 진행할 경우 수년이 걸리곤 했다.
이 시스템은 인간 연구자와 AI 에이전트를 결합했다. 연구자와 AI는 Signal의 보안 목표를 수학적 명세로 바꾸는 작업을 도왔고, 사람들은 이를 검토했다. 이후 Gemini Carbon 기반 에이전트가 Lean 증명 코드 약 650만 줄을 생성했다. Lean은 수학적 증명이 정해진 규칙을 따르는지 검사기가 검증할 수 있는 프로그래밍 언어다. 에이전트는 코드베이스의 약 1%를 사람의 검토가 필요한 부분으로 표시했다.
증명으로 무엇을 검증했나?
연구진은 libsignal의 포스트양자 PQXDH 핸드셰이크와 Triple Ratchet이 컴파일된 기계어 코드를 검사했다. 전방향 보안성, 인증, 기기가 침해된 뒤의 보호 등 구체적인 속성을 증명했다. 연구 논문에 따르면 코드는 수정하지 않은 Rust 소스에서 표준 컴파일러로 컴파일한 뒤 AArch64 기계어 코드 상태로 검사했다.
이번 작업은 추상적인 설계가 안전하다는 점을 증명하는 데서 더 나아가, 명시된 보안 보장을 컴파일된 코드와 연결한다. DeepMind는 널리 배포된 암호화 프로토콜의 구현을 이 정도 깊이로 정형 검증한 것은 처음이라고 밝혔다. 연구팀은 이전에 수정된 버그 두 건도 격리된 코드 버전에 다시 넣었다. 그러자 시스템은 버그가 있는 버전이 명시된 보안 속성을 충족하지 못한다는 증명을 만들어냈다.
증명에는 한계가 있다
이번 결과가 Signal의 모든 부분이나 해당 프로토콜을 사용하는 모든 앱에 보안 문제가 없다는 수학적 보장은 아니다. 증명은 libsignal의 특정 속성만 다루며 앱 전체를 검증하지 않는다. 또한 승인된 명세, Lean 검사기, 저수준 암호화 루틴에 대한 계약에 의존한다. The Register는 이번 결과가 실제 메시지 바이트의 계산적 비밀성을 증명하지는 않는다고 지적했다. DeepMind의 논문은 기호 모델과 계산 모델 모두에서 증명했다고 설명하지만, 두 모델은 기초가 되는 암호화 기본 요소에 대한 가정에 의존한다.
DeepMind는 다른 이들도 사용할 수 있도록 검증 자료를 공개한다고 밝혔다. 의료기기 펌웨어와 전력망 소프트웨어 같은 분야에도 이 접근법을 적용하길 바라지만, 방법을 확장하려면 추가 연구가 필요하다고 덧붙였다. 이번 작업은 실제 환경에서 사용되는 코드를 더 많이 검증하기 위한 한 걸음이지, 다른 시스템들도 검증됐다는 증거는 아니다.
왜 중요한가
Signal 사용자에게 이번 작업은 핵심 프로토콜 구현의 특정 보안 속성을 기계적으로 검증한 증거를 더한다. 앱 전체에 버그가 없다는 뜻은 아니며, 증명은 암호화 구성 요소에 관한 가정에 의존한다.
