Google DeepMind는 2026년 11월 10일 AI 에이전트 시스템 ‘AlphaProof Code’를 이용해 메신저 Signal의 암호화 코드가 핵심 보안 조건을 충족한다는 수학적 증명을 만들었다고 발표했습니다. 대상은 Signal 프로토콜의 공식 Rust 구현인 libsignal에서 종단간 암호화에 쓰이는 PQXDH 핸드셰이크와 Triple Ratchet입니다. 이 기술은 Signal뿐 아니라 WhatsApp과 Google Messages 등에서도 사용됩니다.
AI 에이전트들은 4주 동안 수학적 증명 언어 린(Lean)으로 600만 줄이 넘는 증명 코드를 작성했습니다. Google DeepMind는 이를 사람이 전문가 팀과 함께 수행하면 수년이 걸릴 수 있는 작업이라고 설명했습니다. The Register는 실제로 이 연구에 5명으로 구성된 팀이 참여했다고 전했습니다.
무엇을 확인했나
연구진은 먼저 보안 목표를 수학적 명세로 바꾸고, 사람이 각 명세를 검토했습니다. 이후 Gemini Carbon 기반 에이전트들이 코드가 명세를 충족한다는 증명을 만들었고, 린의 검사 시스템이 증명의 논리적 오류를 확인했습니다. Google DeepMind에 따르면 시스템은 사람이 추가로 살펴볼 부분을 전체의 약 1%로 좁혔습니다.
검증한 조건에는 메시지 기밀성과 인증, 과거 대화 보호인 순방향 비밀성, 기기 침해 뒤 보안을 회복하는 사후 침해 보안이 포함됩니다. 연구진은 과거 수정된 실제 버그 두 개를 코드에 다시 넣어 시험했고, 두 경우 모두 해당 코드가 보안 조건을 충족하지 않는다는 증명을 얻었습니다. 구글은 널리 쓰이는 암호 프로토콜의 실제 구현을 이 깊이로 정형 검증한 첫 사례라고 밝혔습니다.
검증이 다루지 않은 범위
이번 결과는 Signal 앱 전체가 안전하다는 보증은 아닙니다. Google DeepMind가 공개한 GitHub 자료에 따르면 증명 대상은 특정 AArch64 컴퓨터 코드로 만든 libsignal의 명령행 프로그램이며, 암호 기능 일부는 정해진 모델로 연결해 다뤘습니다. AI Times는 그룹 메시징과 여러 기기 간 상태가 검증에 포함되지 않았다고 전했습니다. 일부 보안 성질은 별도의 수학적 모델과 가정 아래 확인됐습니다.
The Register는 이번 작업이 암호가 완벽하다고 가정하는 이론적 검증이며, 실제 데이터의 비밀이 모든 상황에서 보장되는 것은 아니라고 짚었습니다. 또 연구의 어려움은 무엇을 증명할지 정하는 데에도 있다고 연구진은 설명했습니다. Google DeepMind는 명세와 증명 자료를 공개했으며, 의료기기 소프트웨어와 전력망 같은 다른 시스템에 적용하는 방안도 제시했습니다. 다만 그런 분야에서 실제 검증이 이뤄졌다는 뜻은 아닙니다.
왜 중요한가
Signal 등에서 쓰이는 암호 코드의 일부를 수학적으로 점검해, 개발자와 보안 검토자가 구현 오류를 찾는 데 활용할 수 있는 공개 자료가 생겼습니다. 하지만 그룹 대화와 다중 기기 기능은 범위 밖이어서, 이 결과만으로 이용자가 쓰는 Signal 앱 전체의 안전성을 판단할 수는 없습니다.
