구글 딥마인드, AI 에이전트로 Signal 일대일 대화 암호 코드의 보안 성질 증명

구글 딥마인드 연구진은 2026년 11월 10일 AI 에이전트 프레임워크 AlphaProof Code로 Signal 프로토콜 참조 구현체 libsignal의 특정 보안 성질을 증명했다고 발표했습니다. 4주간 진행한 이번 연구는 수정하지 않은 libsignal 코드를 명령행 프로그램에 연결해 컴파일한 실행 파일을 기계어 수준에서 검증했습니다.

정형 검증은 프로그램이 지켜야 할 조건과 적용할 가정을 수학적 명세로 정하고, 코드가 그 명세를 만족한다는 증명을 만드는 방식입니다. 테스트가 일부 입력과 실행 사례를 확인하는 데 비해, 이런 증명은 명세가 허용하는 실행을 대상으로 성립합니다. 이전 암호 프로토콜 검증은 주로 설계 자체를 추상화한 모델이나 검증하기 쉽게 바꾼 구현을 다뤘습니다. 실제 배포 코드까지 검증하면 설계와 구현 사이에서 생길 수 있는 오류도 보안 성질과 함께 살필 수 있습니다.

AlphaProof Code에서는 사람과 AI 에이전트가 명세를 만들고, 사람이 승인한 뒤 다른 에이전트들이 증명을 작성합니다. 연구자들은 기존 연구에 나온 보안 성질을 바탕으로 Lean 언어의 명세를 작성했고, 검토 에이전트들의 비판을 거쳐 사람이 내용을 승인했습니다. 증명 에이전트가 만든 Lean 증명은 Lean의 커널이 검사합니다. 별도의 비교기는 증명이 사람이 승인한 명세의 정리와 정의를 그대로 다루는지 확인합니다. 따라서 증명 에이전트의 설명이나 자체 판단만으로 결과를 확정하지 않습니다.

연구진은 Signal의 PQXDH 핸드셰이크와 Triple Ratchet을 대상으로 삼았습니다. 핸드셰이크는 대화 양쪽이 공유 비밀을 만드는 단계이고, 래칫은 그 비밀을 바탕으로 메시지마다 새 암호화 키를 유도합니다. 이전 메시지 키를 지우는 구조는 현재 세션 상태가 노출돼도 과거 메시지를 복호화하기 어렵게 하는 전방향 비밀성을 뒷받침합니다. 또 새 DH 값을 섞는 교환에 공격자가 개입하지 못하면, 세션 상태가 노출된 뒤에도 이후 메시지의 보호가 회복됩니다. 이를 침해 후 보안이라고 합니다. 핸드셰이크의 상대 인증과 비밀성도 증명 대상에 포함됐습니다.

검증 대상은 libsignal v0.105.4와 SPQR v1.6.0을 작은 명령행 하네스에 연결한 일대일 세션 코드입니다. 연구진은 이를 표준 Rust 컴파일러로 AArch64 리눅스 실행 파일로 만들고, 실행 파일의 동작을 Lean으로 표현한 기계어 의미론에 대조했습니다. 즉 Rust 소스의 동작을 추정해 증명한 것이 아니라, 컴파일 뒤 나온 실행 파일을 대상으로 삼았습니다. 정리는 세션 시작과 메시지 송수신을 다루며 키 생성은 범위에서 제외했습니다. 그룹 대화와 Signal 모바일 앱의 나머지 기능도 연구 범위에 포함하지 않았습니다.

논문은 보안 주장을 기호적 모델과 계산 보안 모델로 나눠 제시합니다. 기호적 모델은 해시나 키 유도 함수 같은 암호 기본요소를 정해진 성질을 가진 이상적 대상으로 취급합니다. 이 모델은 네트워크를 통제하고 키나 세션 상태를 얻는 공격자뿐 아니라 나중에 DH를 깨는 공격도 다루며, 핸드셰이크 비밀성은 미래의 양자 공격자가 DH를 깨는 경우까지 포함합니다. 다만 SPQR이 양자 공격 뒤 보호를 회복하는 성질은 이 증명 범위에 들어가지 않습니다.

계산 보안 모델은 실제 암호 기본요소에 관한 보안 가정 아래, 계산 능력이 제한된 고전적 공격자를 대상으로 합니다. 이 모델에서 연구진은 메시지 기밀성과 진위성, 전방향 비밀성, 침해 후 보안을 다룹니다. 이 결과는 기호적 모델의 결론과 범위가 같지 않으며 양자 공격자를 포함하지 않습니다. 또한 여러 개의 긴 세션에서 키 갱신 단계가 많이 쌓이는 대규모 상황에서는 계산 모델의 보안 한계값이 실질적인 보증을 주지 못할 수 있다고 논문은 설명합니다.

증명의 범위는 명세와 신뢰 조건에도 달려 있습니다. 암호 기본요소와 일부 외부 함수는 계약으로 가정하며, Lean 커널과 AArch64 실행 의미론도 신뢰 기반에 포함됩니다. 사람이 정하고 승인한 명세가 보안 목표와 공격자 가정을 정의하므로, 그 명세가 목표를 얼마나 충실히 표현했는지가 결과의 의미를 좌우합니다.

연구진은 과거 수정된 libsignal 버그 두 건을 코드에 다시 넣어, 변경된 실행 파일에서 기호적 보안 정리가 성립하지 않는다는 점을 증명했습니다. 이는 명세가 알려진 오류를 포착하는지 시험한 결과입니다. WIRED는 연구진이 분석한 코드에서 새 취약점을 발견하지 않았다고 보도했습니다. 구글 딥마인드는 명세와 증명 자료를 공개했습니다.