AI가 쓴 650만 줄 증명, Signal 암호는 어디까지 확인됐나

AI가 메신저 Signal 암호화의 안전을 증명했다는 기사가 11월 10일 여러 매체에 올라왔습니다. 구글 딥마인드(Google DeepMind)가 AI 에이전트 여러 개를 팀으로 부리는 도구 AlphaProof Code로 Signal의 암호 코드를 검증했다며, 블로그와 논문과 결과물 저장소를 같은 날 공개했기 때문입니다. 논문에 따르면 연구자 5명이 에이전트를 부리며 4주 동안 증명 작업을 했습니다.

AI가 코드의 취약점을 찾아내는 일은 이미 현실입니다. PHP의 치명적 취약점을 찾은 Wiz Research는 구글 Gemini 4 Argon이 취약점 발견에 크게 기여했다고 밝혔습니다(관련 기사). 하지만 그것은 버그를 찾는 일이고, 버그가 없다는 것을 보이는 일은 아닙니다. 이번 발표는 AI가 쓴 증명으로, 정해 둔 보안 성질을 깨는 버그가 없음을 수학으로 보이려는 시도입니다.

그렇다면 무엇을 증명했고, 사람이 읽지 못한 증명을 어떻게 믿을 수 있으며, 증명이 다루는 범위는 어디까지일까요. 순서대로 봅니다. 공개 자료를 정리한 것이고, 증명을 직접 다시 실행해 검사하지는 않았습니다.

Signal 암호화에서 증명한 보안 성질

형식 검증(formal verification)은 코드가 약속한 대로 움직인다는 것을 수학 문장으로 쓰고, 그 문장이 맞는지 컴퓨터가 한 줄씩 따져 보는 방법입니다. 몇 가지 입력을 넣어 보는 시험과 달리 가능한 모든 경우를 따집니다.

논문 초록이 보안 성질로 꼽은 것은 네 가지입니다.

• 열쇠가 나중에 유출돼도 지난 대화는 안전하다는 전방 비밀성(forward secrecy)
• 기기가 잠시 뚫린 뒤에도 대화가 다시 안전해진다는 침해 후 보안(post-compromise security)
• 대화 상대가 맞는지 확인하는 인증
• 처음 연결을 맺을 때 합의한 열쇠가 비밀로 남는 것

딥마인드 블로그는 지금까지 프로토콜 검증이 대개 설계도 수준에서 멈췄고, 이번에는 컴파일된 기계어까지 내려갔다고 밝혔습니다. 기계어는 컴퓨터가 실제로 실행하는 명령입니다. 다만 논문에 따르면 검증 대상은 Signal 앱이 아닙니다. Signal이 공개한 암호 라이브러리 libsignal이 있고, 이를 불러 쓰는 명령줄 도구를 빌드한 파일이 대상입니다.

650만 줄을 사람이 읽지 않고 믿는 이유

증명을 쓰려면 먼저 무엇을 증명할지 정해야 합니다. 이 "증명할 문장"을 명세(specification)라고 부릅니다. 논문에 따르면 명세는 사람과 AI 에이전트가 주고받으며 썼고, Gemini 4 Carbon(출시 기사)과 Claude Opus 5.5 기반 에이전트가 관여했으며, 다른 모델 계열의 에이전트가 초안을 검토했습니다. 블로그는 사람 전문가가 명세를 하나하나 검토했다고 밝혔습니다.

명세가 정해진 뒤의 증명은 전부 Gemini 4 Carbon 기반 에이전트 팀이 썼고, 저자 누구도 증명 코드를 쓰지 않았다고 논문은 적었습니다. 한 번 돌릴 때 에이전트 40~80개가 컴퓨터 한 대에서 24~72시간 일하는 식이었습니다.

사람이 읽지 못한 증명을 믿어도 될까요. 답안은 AI가 쓰고 채점은 Lean이 합니다. Lean은 증명이 논리적으로 맞는지를 한 줄씩 기계적으로 검사하는 프로그램이어서, 답안을 쓴 AI를 믿을 필요가 없습니다. 블로그는 이렇게 적었습니다. 에이전트가 증명을 점검해 사람이 다시 볼 곳을 골랐는데, 그것이 "코드베이스의 1%"였다는 것입니다. 명세는 사람이 전부 검토했습니다. 무엇의 1%인지는 밝히지 않았고, 논문에는 이 수치가 없습니다.

채점이 믿을 만해도 무엇을 채점할지는 사람이 정합니다. 그래서 사람이 직접 믿어야 하는 부분이 따로 남습니다. 믿어야 하는 것은 명세, 그리고 ARM 칩(AArch64)이 명령을 어떻게 실행하는지를 Lean으로 옮긴 규칙입니다. 논문 초록에 따르면 둘을 합쳐 약 2만 6천 줄입니다. 이 밖에 Lean 검사기와 암호 함수에 대한 가정도 믿어야 합니다.

Signal Shot은 Signal 프로토콜을 Lean으로 검증하는 공개 프로젝트입니다. 이를 이끄는 Beneficial AI Foundation은 같은 날 글에서, 칩의 명령 실행 규칙을 옮긴 부분을 다른 팀이 따로 검증해야 한다고 밝혔습니다.

증명이 다루는 범위

논문은 이번 증명의 범위를 직접 정리해 두었습니다. 대표적인 것은 다음과 같습니다.

안드로이드와 iOS 앱도 같은 코드를 쓰니 결과가 이어질 것이라고 논문은 말합니다. 다만 조건이 있습니다. 빌드 설정과 운영체제 연결이 프로토콜 코드의 동작을 그대로 보존한다고 믿어야 합니다. 이 믿음은 증명 대상이 아닙니다. Beneficial AI Foundation은 x86-64 같은 다른 칩 구조도 남은 일로 꼽았습니다.

WhatsApp은 이 증명의 직접 대상이 아닙니다. 논문은 WhatsApp·Messenger·Google Messages가 이 프로토콜의 변형을 쓴다고 소개했을 뿐, 그쪽 구현을 검증했다고는 쓰지 않았습니다. Signal과 WhatsApp이 모두 안전함을 증명했다는 취지의 9to5Mac 제목은 이 범위보다 넓게 읽힙니다. Beneficial AI Foundation도 같은 취지로, 헤드라인만 보고 Signal이 완전히 안전하다고 받아들이면 남은 검증을 끝낼 연구자들의 동기가 떨어질 수 있다고 밝혔습니다.

증명이 버그를 잡아내는지 본 시험

명세가 느슨하면 버그가 있는 코드가 증명에서 걸러지지 않을 수 있습니다. 딥마인드는 이를 시험하려고 빌드를 하나 만들었습니다. 과거에 발견돼 이미 고쳐진 Signal 버그 두 건을 일부러 되돌려 넣은 것입니다. 그 빌드가 보안 성질을 지키지 못한다는 증명, 곧 이 코드는 안전하지 않다는 증명을 에이전트가 써냈고, Lean이 맞다고 검사했습니다.

논문은 증명을 두 가지 모델로 썼습니다. 기호 모델은 암호를 완벽한 상자로 가정하고 공격 절차만 따지는 방식이고, 계산 모델은 공격자가 성공할 확률의 상한을 계산하는 방식입니다. 버그를 되돌린 빌드가 안전하지 않다는 것은 기호 모델에서 증명됐고, 계산 모델에서는 아직 증명하지 못했습니다. 논문에 따르면 그러려면 암호를 깨기가 정말 어렵다는 가정 자체를 증명해야 하는데, 이는 아직 풀리지 않은 문제입니다.

계산 모델의 증명은 양자 컴퓨터를 쓰는 공격자는 다루지 않습니다.

이 시험은 새 취약점을 찾는 일이 아니라 알려진 버그를 증명이 걸러 내는지 보는 일이었습니다. 와이어드(Wired)는 딥마인드가 분석한 범위에서 새 취약점을 찾지 못했다고 보도했습니다.

첫 사례라는 의미와 증명의 규모

블로그는 이번이 처음이라고 밝혔습니다. 널리 쓰이는 프로토콜의 구현을 형식 검증한 일로는, AI를 썼든 안 썼든 처음이라는 것입니다. 논문은 같은 주장에 조건을 붙여 씁니다. 프로토콜이 지켜야 할 보안 성질을, 수정하지 않은 코드에서, 널리 쓰이는 구현에 대해 증명한 첫 사례라는 것입니다. 본문 8절에는 "우리가 아는 한"도 붙였습니다. 딥마인드가 내세우는 것은 AI가 쓴 증명을 Lean이 검사하는 방식을 널리 쓰이는 암호 라이브러리의 빌드에 적용했다는 점입니다.

증명에 든 비용은 공개되지 않았고, 와이어드에 따르면 구글이 공개를 거절했습니다. 규모는 줄 수로 가늠할 수 있는데, 증명 코드의 줄 수는 자료마다 다르게 적혀 있습니다.

세 값 모두 Signal 코드가 아니라 AI가 쓴 증명 코드의 줄 수입니다.

같은 방향의 시도는 이미 있었습니다. 앤트로픽은 10월 22일 Claude가 컴파일된 오픈소스 코드에서 프로그램이 충돌해 멈추는 일이 없음을 증명했다고 발표했습니다(관련 기사). 증명하는 성질은 다르지만, 기계가 쓴 증명을 기계가 검사하는 구조가 큰 코드로 번지고 있다는 점은 같습니다.

형식 검증 발표를 읽을 때 볼 세 가지

형식 검증 결과를 읽을 때는 세 가지를 보십시오.

• 대상: 앱인지 명령줄 도구 빌드인지, 어느 버전과 어떤 사용 조건인지
• 가정: 증명 밖에서 믿고 받아들이는 것이 무엇이고 누가 따로 검증하는지
• 명세: 증명할 문장을 누가 썼고 사람이 읽었는지