암호 통신의 설계가 안전하다는 것과, 실제 코드가 그 설계의 보안 속성을 지킨다는 것은 별도의 문제다. 메시지를 늦게 받았을 때 어떤 키를 꺼내고, 실패한 통신 뒤에 어떤 상태를 저장하는지에 따라 구현에서 문제가 생길 수 있다.
구글 딥마인드는 2026년 11월 10일 AlphaProof Code를 발표하며, Signal 프로토콜의 참조 구현인 libsignal의 핵심 보안 속성을 기계어 수준에서 증명했다고 밝혔다. AI 에이전트가 증명을 작성하고 증명 보조 도구 Lean이 이를 확인하는 방식이다. 무엇이 안전하다는 뜻인지 정하는 명세는 사람이 검토하고 승인했다.
설계와 실행 파일 사이를 연결하다
공개 연구 자료에 따르면, 연구진은 수정하지 않은 libsignal v0.105.4와 SPQR 코드를 작은 명령행 프로그램에 연결한 뒤, 표준 Rust 컴파일러로 AArch64 Linux 실행 파일을 만들었다. 증명은 이 실행 파일의 동작을 대상으로 한다. 검증을 쉽게 하려고 새로 만든 암호 구현을 분석한 경우와 구별되는 지점이다.
검증 대상은 일대일 대화에서 PQXDH로 세션을 시작하고 Triple Ratchet으로 메시지를 암호화하고 복호화하는 동작이다. PQXDH는 대화 상대와 공유할 비밀을 마련하고, Triple Ratchet은 메시지를 주고받으며 키를 갱신한다. 키를 처음 생성하는 동작과 그룹 대화는 이번 검증 범위에 포함되지 않는다.
그 결과가 뜻하는 보호의 한 예가 전방향 비밀성이다. 메시지마다 이전 상태에서 새 키를 도출하고 사용한 키를 삭제하면, 나중에 현재 상태가 유출돼도 과거 메시지의 키까지 그대로 드러나지는 않는다.
침해 이후의 보호에는 다른 조건이 붙는다. 현재 상태를 훔친 공격자를 이후의 메시지에서 배제하려면 새로운 비밀값을 교환해 키에 섞는 과정이 필요하다. 연구 자료는 새 Diffie–Hellman 비밀값을 교환하는 동안 공격자가 수동적으로 머무르는 조건을 설명한다. 기기를 잠시 침해당한 뒤 모든 메시지가 즉시 안전해진다는 뜻으로 읽어서는 안 된다.
AI가 증명해도 사람이 정해야 하는 것
AlphaProof Code의 역할 분담은 무엇을 증명할지 정하는 일과, 정해진 주장을 증명하는 일을 나누는 데서 출발한다.
연구진이 사용한 검증 흐름이다. 결과는 명세와 실행 환경 모델, 암호 루틴 등에 둔 가정에 의존한다.
명세부터 증명 확인까지
- 명세 작성과 승인AI가 보안 목표와 환경을 Lean으로 표현하고, 사람이 검토해 승인본을 정한다.
- 실행 파일 준비수정하지 않은 Rust 코드를 컴파일하고, 실행 파일을 AArch64 동작 모델과 함께 Lean에 불러온다.
- AI의 증명 작성에이전트 팀이 실행 파일이 승인된 명세를 만족한다는 증명을 만든다.
- 증명과 대상 확인Lean 커널이 증명을 확인하고, comparator가 정리와 의존 정의를 보관된 승인본과 대조한다.
이 구조에서는 증명을 만든 AI의 판단을 그대로 믿을 필요가 없다. 증명이 논리적으로 성립하는지는 Lean이 확인하고, 증명 대상이 몰래 약해지지 않았는지는 승인본과의 비교로 확인한다. 비교 대상에는 정리의 문장뿐 아니라 그 문장이 의존하는 정의도 포함된다. 겉으로 같은 주장이라도 정의가 달라지면 더 약한 결과를 증명할 수 있기 때문이다.
반면 Lean이 증명을 받아들였다고 해서 보안 목표를 충분히 강하게 정했다는 사실까지 자동으로 확인되는 것은 아니다. 예를 들어 명세가 공격자의 능력을 실제보다 약하게 잡았다면, 그 명세를 만족한다는 증명도 기대한 만큼의 보호를 주지 못한다. 연구진은 사람의 검토와 함께 비판적으로 명세를 살피는 에이전트, 정리의 전제가 실제로 성립할 수 있는지 확인하는 증명 등을 사용했다고 설명한다.
보장은 어떤 가정 위에 놓였나
연구진은 암호를 이상적인 연산으로 다루는 기호적 모델과, 공격 성공 가능성을 바탕이 되는 암호 기술의 안전성에 연결하는 계산적 모델에서 각각 증명했다.
두 증명은 같은 보장을 서로 다른 표현으로 반복한 것이 아니다. 기호적 증명은 충돌이 없는 실행이라는 조건 아래 여러 키 유출 상황을 다루며, 핸드셰이크 이후 공격자가 Diffie–Hellman을 깨는 경우의 비밀성도 포함한다. 계산적 증명은 고전적 공격자를 대상으로 메시지의 기밀성과 진위를 다룬다. 이쪽은 양자 공격자를 포함하지 않으며, 여러 긴 세션에서 키 갱신이 많아지면 공격 성공 가능성의 상한이 유의미한 보장을 주지 못하는 한계도 연구 자료에 명시돼 있다.
또 일부 저수준 암호 루틴과 입출력 함수 등은 실제 기계어를 끝까지 증명하는 대신, 해당 함수가 어떻게 동작한다고 가정하는 계약으로 대체했다. 암호 기술 자체의 안전성, Lean 커널, AArch64와 운영체제의 동작을 표현한 모델도 결과가 의존하는 기반이다.
따라서 이번 결과는 특정 실행 환경에서 암호 구현과 보안 명세를 연결한 증명으로 이해해야 한다. Android와 iOS의 Signal 앱도 같은 Rust 코드를 사용하지만, 연구진은 다른 환경으로 결과를 옮기려면 컴파일 설정과 운영체제 인터페이스 등이 해당 코드의 동작을 보존한다고 믿을 수 있어야 한다고 설명한다. Signal 앱 전체나 모든 기기 환경을 그대로 검증한 결과는 아니다.
연구진이 생성한 Lean 증명 코드는 약 650만 줄이다. 이 규모보다 구현 검증의 의미를 구체적으로 보여 주는 것은 결함을 다시 넣은 사례다. 연구진은 과거에 수정된 libsignal 버그 두 개를 다시 넣고, 그 실행 파일이 기호적 보안 정리를 위반한다는 증명도 Lean으로 확인했다고 밝혔다.
그중 하나는 보관된 과거 세션으로만 복호화되는 메시지를 받았는데도 새 세션의 상태를 저장하던 버그다. 그 상태에는 서명된 사전 키의 비밀값 사본이 포함됐다. 이 사례는 암호 알고리즘의 설계만으로는 드러나지 않는 상태 저장 동작까지 보안 주장과 연결했다는 점을 보여 준다. 두 버그에 대한 결과가 모든 취약점을 찾아낸다는 보장은 아니지만, 적어도 정해진 명세가 실제 구현의 결함을 배제하는지 확인한 사례다.
