Google DeepMind, AlphaProof Code로 Signal 프로토콜 형식 검증 완료

• Google DeepMind이 Signal 암호 프로토콜의 실제 코드를 형식 검증한 에이전틱 프레임워크 AlphaProof Code를 공개함. 이는 널리 배포된 프로토콜 구현이 어떤 방식으로든 검증된 첫 사례임.
• 시스템은 핵심 보안 속성을 증명하기 위해 Lean 코드 600만 줄 이상을 생성했으며, 전문가 팀이 보통 수년이 걸리는 작업을 4주 만에 완료함.
• AI 에이전트가 증명 생성과 감사의 대부분을 처리하고 Lean이 나머지 작업을 자동 검사했기 때문에, 인간 전문가가 코드베이스의 1%만 검토함.
• 팀은 격리된 Signal 코드 버전에 이전에 수정된 두 가지 버그를 다시 도입해 시스템의 결함 탐지 능력을 확인했으며, 두 경우 모두 기계 검증된 보안 취약성 증명이 생성됨.

Technical Methodology

• AlphaProof Code는 인간 전문가가 AI와 협력해 형식 수학 명세를 정의하고, Gemini Carbon 기반 에이전트가 증명을 실행하는 멀티 LLM 프레임워크로 작동함.
• 검증 과정은 설계 단계 분석을 넘어, 임시 장치 침해 시 메시지 보호와 같은 보안 속성이 장치에서 실행되는 정확한 컴파일된 코드에서 충족됨을 증명함.
• 에이전트가 명세와 증명을 초안 작성하고, AI가 인간 검토가 필요한 영역을 강조한 후 Lean이 최종 검증을 수행하는 워크플로우를 사용함.

Availability and Impact

• Google DeepMind는 커뮤니티 사용을 위해 형식 검증 산출물을 오픈소스로 공개하고, 연구를 상세히 설명한 기술 논문을 발표함.
• 이 프로젝트는 AI가 의료 기기 펌웨어와 전력 그리드 소프트웨어 등 다른 시스템에도 적용될 수 있는 방식으로 핵심 인프라에 엘리트 수준의 보안 보장을 제공할 수 있음을 입증함.