Google DeepMind, AlphaProof Code로 Signal 프로토콜의 실제 코드 형식 검증
Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
Google DeepMind는 다중 LLM 기반 에이전트 프레임워크 AlphaProof Code를 활용해 Signal 프로토콜의 실제 코드에 대한 주요 보안 특성을 수학적으로 증명했다고 밝혔다. Gemini Carbon을 사용하는 에이전트가 600만 줄이 넘는 Lean 코드를 생성했으며, 검증은 4주 만에 완료됐다고 한다. 형식 검증 결과물은 오픈소스로 공개될 예정이다.
AlphaProof Code는 사람 전문가가 AI에게 무엇을 증명할지 정하고, AI 에이전트 무리가 증명을 맡는 역할 분담형 프레임워크다. 먼저 연구자들이 여러 모델과 함께 Signal의 보안 목표를 형식적인 수학 명세로 바꿨고, 모든 명세는 사람 전문가가 확인했다. 이후 Gemini Carbon을 사용하는 에이전트가 증명을 수행해 600만 줄이 넘는 Lean 코드를 생성했다.
에이전트는 스스로 증명을 감사해, 사람이 다시 확인해야 할 부분을 코드베이스의 1%로 좁혔다. 나머지는 Lean이 자동으로 검사하므로, 전문가들은 사람의 판단이 필요한 부분에 집중할 수 있었다. 많은 프로토콜 검증은 설계 수준에서 멈추지만, 이번에는 단말에서 실제로 돌아가는 코드가 기기가 일시적으로 침해된 전후에도 메시지를 보호하는 등 핵심 속성을 충족한다는 것까지 증명했다. 검증에는 4주가 걸렸으며, 기존에는 전문가 팀이 수년이 걸리던 작업으로 알려져 있다.
방법의 타당성을 확인하기 위해, 과거에 수정된 실제 버그 2건을 Signal 코드의 격리된 버전에 다시 넣었다. 두 경우 모두 시스템은 버그가 들어간 버전이 안전하지 않다는 것을 보여주는 기계 검사 완료 증명을 내놓았다. DeepMind는 이 성과가 의료기기 펌웨어나 전력망 소프트웨어 등 다른 중요 시스템을 지키는 토대가 될 것이라고 밝혔다. 방법을 확장하려면 추가 연구가 필요하며, CodeMender와 같은 자동 방어 에이전트와의 결합도 구상하고 있다.
설계뿐 아니라 실제 코드까지 형식 검증을 수행한 절차와, 사람의 확인 범위를 1%로 좁힌 역할 분담 구조가 구체적으로 기술되어 있다.
출처: Google DeepMind Blog · deepmind.google