보안2026. 11. 11. 오전 11:54 UTC·2 분 소요

DeepMind AlphaProof Code, Signal libsignal 보안 형식 검증

최대 80개 AI 에이전트가 4주간 Signal 암호화의 핵심 libsignal이 주요 보안 보장을 지킨다는 것을 증명했습니다. 다만 범위는 제한적입니다.

Abstract illustration of a padlock made of code lines, symbolizing formally verified encryption in the Signal messaging library. — 이미지: Numerama

Google DeepMind는 AI 에이전트 시스템 AlphaProof Code로 Signal의 암호화 라이브러리 libsignal의 보안 보장을 형식적으로 증명했다고 2026년 11월 10일 밝혔습니다. 연구자들이 증명을 직접 작성하지는 않았습니다.

4주 동안 DeepMind 연구원 5명의 머신에서 최대 80개 AI 에이전트 팀이 쉬지 않고 작업했습니다. libsignal은 Signal의 종단간 암호화 프로토콜을 구현한 라이브러리이며, 회사에 따르면 변형 버전이 WhatsApp, Messenger, Google Messages에도 쓰입니다.

테스트가 아닌 수학적 증명

통상 소프트웨어 보안은 테스트와 감사로 점검하며, 이는 문제를 찾지 못했다는 것만 말해 줍니다. 형식 검증은 코드가 특정 속성을 위반할 수 없음을 정리처럼 증명하는 방식이지만 비용이 매우 큽니다. seL4 커널 검증에는 한 사람 기준 약 20년의 작업량이 들었습니다.

연구자들이 증명할 속성을 정하면, Gemini 4 Carbon 모델로 구동되는 에이전트가 Lean 언어로 약 650만 줄의 증명을 작성했습니다. Lean 검증기가 각 단계를 자동으로 확인합니다.

증명에 따르면 공격자가 휴대전화에 저장된 키를 훔쳐도 각 메시지 키가 이전 키에서 파생된 뒤 삭제되므로 과거 메시지는 읽을 수 없습니다. 두 사용자가 새 메시지를 주고받으면 대화 보안이 회복되며, 누구도 두 사람 중 한 명을 사칭할 수 없습니다. 방법을 검증하려고 이미 수정된 과거 버그 2건을 다시 넣자, 시스템은 해당 버전이 보장을 충족하지 못함을 보였습니다.

한계

검증은 2인 대화에만 적용되고, 모바일 앱이 아닌 Linux 테스트 버전을 대상으로 하며, 기초 암호 구성 요소가 완벽하다고 가정합니다. Signal의 CTO Ehren Kret은 "중대한 진전"이라고 평가했습니다. 저자들은 증명이 저렴해진 만큼 무엇을 증명할지가 어려운 문제가 된다고 결론지었습니다.