구글 딥마인드, AlphaProof Code 공개

구글 딥마인드가 11월 10일(현지 시간) AI 에이전트 여럿이 소프트웨어의 보안 성질을 수학적으로 증명하는 형식 검증 프레임워크 AlphaProof Code를 공개했다. 연구진은 이 도구로 시그널 프로토콜의 참조 구현인 libsignal이 실제 기기에서 돌아가는 기계어 수준에서 핵심 보안 성질을 지킨다는 것을 증명했다. 시그널 프로토콜은 시그널 앱과 구글 메시지에 쓰이고, 변형판이 왓츠앱과 메타 메신저에도 들어가 있어 수십억 명의 대화를 보호한다. 딥마인드는 널리 배포된 암호 프로토콜을 AI로 이 깊이까지 형식 검증한 것은 처음이며, AI를 쓰든 안 쓰든 이런 프로토콜의 구현 자체가 형식 검증된 것도 처음이라고 밝혔다. 작업은 5명의 연구진이 4주 만에 끝냈다.

형식 검증은 코드가 결함 없이 정해진 대로 돈다는 것을 수학으로 증명하는 일이다. 테스트나 코드 리뷰가 버그를 찾아내는 방식이라면, 형식 검증은 명세가 금지한 종류의 버그와 공격이 아예 존재할 수 없다는 것을 보인다. 그만큼 비싸다. 논문에 따르면 이 분야의 대표 성공 사례인 seL4 마이크로커널은 검증에 20인년이 들었고, 검증된 C 컴파일러 CompCert는 6인년이 들었다. 두 사례 모두 처음부터 검증을 염두에 두고 짠 코드였다. 이미 쓰이고 있는 산업용 코드를 최적화 컴파일러가 만든 그대로 검증하는 일은 더 어렵다.

AlphaProof Code는 이 일을 연구팀처럼 나눈다. 사람은 무엇을 증명할지 정하고, 에이전트 무리가 증명을 해낸다. 명세 작성 에이전트가 연구 논문의 보안 모델을 증명 언어 Lean의 정리로 옮기면, 다른 모델 계열의 검토 에이전트가 원 논문과 실제 코드에 충실한지 비판하고, 사람이 최종 승인한다. 명세 작업에는 Gemini 4 Carbon과 Claude Opus 5.5 기반 에이전트가 함께 쓰였다. 증명은 전부 Gemini 4 Carbon 기반 에이전트 팀이 만들었고, 논문 저자 가운데 증명 코드를 직접 쓴 사람은 없었다. 한 팀은 보통 40~80개 에이전트로 꾸려져 한 대의 컴퓨터에서 24~72시간 돌았다. 작업을 나누는 오케스트레이터, 팀 리더, 전체 구조를 설계하는 아키텍트, 증명을 합치는 통합 담당이 역할을 나눠 맡는다.

규모는 이렇다. 에이전트가 만든 증명은 약 650만 줄의 Lean 코드다. 이 가운데 530만 줄이 실행 파일 자체에 관한 증명이고, 계산 모델 증명이 약 86만 줄, 기호 모델 증명이 약 35만 줄이다. 검증 대상인 libsignal 코드는 약 560KB, AArch64 명령어로 약 14만 개다. 사람이 읽고 믿어야 하는 부분은 명세 약 1만 8,000줄과 AArch64 의미론 약 8,000줄을 합친 약 2만 6,000줄로 줄었다. 연구진이 Lean으로 작성한 이 기계어 의미론은 명령어 467개와 시스템 호출 31개를 다룬다. 딥마인드는 에이전트가 증명을 스스로 감사해 사람의 재검토가 필요한 곳으로 표시한 부분이 코드베이스의 1%뿐이었다고 밝혔다. 나머지는 Lean이 자동으로 검사한다.

증명된 내용은 시그널의 양자 내성 핸드셰이크 PQXDH와 트리플 래칫이다. 연구진은 기기가 일시적으로 탈취돼도 그 이전 메시지가 안전하다는 전방 비밀성, 탈취 뒤 새 키 교환이 이뤄지면 다시 안전해지는 사후 침해 보안, 인증, 핸드셰이크 비밀성을 기호 모델과 계산 모델 두 방식으로 증명했다. 검증 대상은 libsignal 0.105.4판의 일대일 대화 코드다. 논문은 수정하지 않은 Rust 코드를 표준 컴파일러로 빌드한 실행 파일에 대해 증명했기 때문에 컴파일러를 신뢰할 필요가 없다고 설명했다. 컴파일러에 버그가 있었다면 증명이 성립하지 않았을 것이라는 뜻이다.

명세가 진짜 버그를 잡아내는지도 확인했다. 연구진은 이미 고쳐진 libsignal의 과거 버그 두 건을 격리된 사본에 되살렸다. 하나는 복호화에 실패한 메시지가 옛 세션으로 재시도될 때 새 세션의 미확정 상태가 저장되는 문제이고, 다른 하나는 핸드셰이크에서 상대 공개키 값을 충분히 검사하지 않아 같은 공유 비밀을 가진 두 번째 세션이 생기는 문제다. 두 경우 모두 AlphaProof Code는 버그가 든 실행 파일이 안전하지 않다는 것을 기계가 검사한 증명으로 내놓았다. 작업 과정에서 기존 학술 분석의 오류도 드러났다. 계산 모델 쪽에서 원 논문과 달라진 지점을 기록한 목록은 200건이 넘고, 그중 15건은 더블 래칫 계산 분석의 빠진 가정이나 공격자가 손쉽게 이기는 게임 조건 같은 결함이었다.

에렌 크렛 시그널 최고기술책임자는 "AI 에이전트로 실제 운영 코드를 유효한 Lean 정리로 옮긴 것은 큰 돌파구"라고 말했다. 그는 "AI가 주도하는 보안 위협이 커지는 가운데 시그널 프로토콜 구현을 엄밀하게 검증해 코드의 프라이버시 보장에 더 큰 확신을 갖게 됐다"고 덧붙였다. 메탈은 앤스로픽이 클로드로 오픈소스 프로젝트 123개를 형식 검증했다고 보도한 바 있는데, 이번에는 대상이 수십억 명이 쓰는 암호 프로토콜의 기계어로 옮겨 갔다. 증명 에이전트를 움직인 모델은 메탈이 10월에 전한 Gemini 4 Carbon이다.

메탈이 확인한 기술 논문은 57쪽 분량이며, 보장이 미치는 범위를 따로 적어 두었다. 기호 모델의 보장은 암호 기본 요소가 완벽하다고 가정하고, 계산 모델의 정리는 양자 컴퓨터를 가진 공격자에 대해서는 보장을 주지 않는다. 사이드 채널 공격은 다루지 않으며, 결과는 연구진이 빌드한 명령줄 프로그램에 대한 것이지 시그널 앱 자체에 대한 것이 아니라고 논문은 밝혔다. 그룹 메시지와 서버 쪽 프로토콜은 다음 과제로 남겼다. 연구진은 논문에서 "증명은 이제 훨씬 싸졌지만 명세는 여전히 어렵다"고 적었다. 노력 대부분이 증명이 아니라 무엇을 증명할지 정하는 명세 작업에 들어갔다는 설명이다.

언론의 눈으로 보면 이번 발표가 바꾸는 것은 보안을 말하는 방식이다. 지금까지 소프트웨어 보안은 버그를 얼마나 빨리 찾아 고치느냐로 평가받았다. AlphaProof Code는 정해진 종류의 공격이 통하지 않는다는 증명서를 코드에 붙이는 길을 보여 준다. 딥마인드는 이번 검증이 의료기기 펌웨어에서 전력망 소프트웨어까지 다른 핵심 시스템을 지키는 토대가 된다고 밝혔고, 자동 방어 에이전트 CodeMender와 짝을 이뤄 쓸 수 있다고 설명했다. 연구진은 Lean 명세와 증명 전체를 오픈소스로 공개했다. 증명 비용이 내려간 만큼 이제 질문은 누가 명세를 쓰고 누가 그것을 검토하느냐로 옮겨 간다. 논문은 널리 쓰이는 시스템의 명세는 그것을 유지하고 분석하고 의존하는 공동체가 함께 합의해야 한다고 적었다.