Google DeepMind, AI 에이전트로 Signal의 핵심 기계어 코드 검증

Google DeepMind는 2026년 11월 10일 AlphaProof Code를 선보였다. AI 에이전트 팀을 활용해 컴파일된 Signal libsignal 코드의 지정된 보안 속성을 검증하는 Lean 기계 검증 증명을 생성했다. 5명으로 구성된 연구팀은 4주 만에 증명 작업을 마쳤으며, 외부 검토를 위해 명세와 검증 산출물을 공개했다.

이번 연구는 Signal 프로토콜 설계의 추상적 모델을 넘어 컴파일된 구현까지 다뤘다. 연구진은 수정하지 않은 libsignal v0.105.4 및 SPQR v1.6.0 크레이트를 간단한 명령줄 하네스에 감싼 뒤, 기본 rustc를 사용해 정적으로 링크된 AArch64 Linux 실행 파일을 빌드했다. 기술 논문은 이번 결과가 널리 배포된 암호 프로토콜 구현의 수정되지 않은 코드를 대상으로 한 최초의 프로토콜 수준 보안 증명이라고 설명한다.

AlphaProof Code의 작업 분담 방식

연구자 5명은 4주 동안 증명 작업을 진행했다. 기호적 증명과 계산적 증명을 병행하는 동안 워크스테이션에서 에이전트를 계속 실행했다. 논문에 따르면 에이전트는 기계 검증을 거친 Lean 증명 코드 약 650만 줄을 생성했으며, 이 코드는 신뢰된 명세와 AArch64 의미론 약 2만 6,000줄을 바탕으로 한다.

사람은 검증할 속성을 선정하고 모호한 부분과 보안상 절충점을 조정했으며, 명세를 검토하고 최종 승인 권한을 유지했다. Gemini 4 Carbon과 Claude Opus 5.5를 기반으로 한 에이전트가 명세 초안을 작성하고 검토했으며, 이 과정에는 다른 모델 계열의 검토도 포함됐다. 이어 Gemini 4 Carbon 에이전트 팀이 모든 증명 코드를 생성했으며, 저자 중 누구도 증명 코드를 작성하지 않았다. 일반적인 작업에서는 한 대의 컴퓨터에서 에이전트 40~80개를 24~72시간 동안 운용했다. 오케스트레이터와 팀 리더가 증명 작업자를 조율하는 한편, 설계자와 통합 담당자는 공유 증명 기반을 관리했다.

검증 관문은 Lean 커널이 증명을 검사하고 비교기가 해당 증명이 별도로 보관된 사람 승인 명세와 일치하는지 확인한 뒤에만 증명을 받아들였다. 이때 모든 전이적 정의를 포함해 대조했으며, Lean의 표준 공리만 사용했다. 증명 과정에서 명세의 문제가 드러나면 에이전트가 작은 수정안을 제안할 수 있었지만, 신뢰된 가정을 변경하려면 사람의 승인이나 사용자가 설정한 정책에 따른 허가가 필요했고, 변경 내용은 근거와 함께 기록됐다. 이 통제 장치는 에이전트가 생성한 증명에서 이미 문서화된 위험을 다룬다. 즉, 명세에 포함된 정의 하나를 통해 명세가 간접적으로 약화될 수 있다는 위험이다.

보안 검증 범위와 과거 버그 테스트

검증 대상은 PQXDH 핸드셰이크와 Triple Ratchet 메시징을 다루는 일대일 세션 코드였다. 연구진은 서로 독립적인 두 가지 논증을 제시한다. 하나는 이상화된 암호학적 가정에 따른 기호적 정리 10개이고, 다른 하나는 암호학적 가정과 통계적 항을 바탕으로 공격자의 이점을 상한 짓는 계산적 증명이다. 검증 대상 속성에는 현재 상태가 탈취된 뒤에도 이전 메시지를 보호하는 순방향 비밀성, 인증, 침해 이후 복구를 다루는 침해 후 보안성, 핸드셰이크 기밀성이 포함된다. 기호적 논증은 이후 Diffie–Hellman이 깨진 경우의 핸드셰이크 기밀성도 추가로 다룬다.

이러한 명세가 실제 오류를 찾아낼 수 있는지 시험하기 위해 연구팀은 과거에 수정된 libsignal 버그 두 건, 즉 취약한 상태와 작은 부분군 문제의 수정 사항을 되돌린 뒤 변경된 바이너리를 다시 컴파일했다. 두 경우 모두 기호적 보안 정리가 성립하지 않는다는 Lean 증명을 생성했다. 공개 검증 저장소는 계산적 증명, 기호적 증명, 공통 바이너리 및 AArch64 의미론 관련 자료를 구분해 제공하며, 증명을 다시 빌드하고 독립적으로 검증하는 방법을 문서화한다.

Signal 최고기술책임자 Ehren Kret은 이번 연구가 “우리 코드의 개인정보 보호 보장에 대한 신뢰를 한층 더 높여 준다”고 말했다.

한계와 향후 과제

이번 보장은 Signal 애플리케이션 전체를 인증하는 수준에는 크게 미치지 못한다. 연구진이 빌드한 libsignal-cli를 새 프로세스로 실행하는 경우에만 해당한다. 키 생성은 검증하지 않았고, 그룹 메시징은 향후 과제로 남겼으며, 부채널과 다중 기기 상태는 검증 시나리오에 포함되지 않는다. 저수준 암호화 기본 요소와 일부 출력 루틴 및 라이브러리 루틴은 신뢰된 계약으로 표현되므로, 결과는 이러한 계약과 승인된 명세, Lean 커널, AArch64 의미론, 기본 요소에 관한 가정에도 의존한다.

논문은 두 논증 모두 SPQR이 추가하도록 설계된 양자 내성 복구를 증명하지는 않는다고 밝힌다. 계산적 정리는 고전적 공격자를 대상으로 하는 반면, 기호적 래칫 정리는 공격자가 SPQR 키를 선택하도록 허용한다. 또한 계산 모델은 공격자의 여러 행동을 제한하며, 메시지와 세션 규모가 충분히 커지면 무의미해진다. 이러한 경계는 외부 검토자가 기계 검증 증명을 특정 배포 환경의 보안 보장으로 받아들이기 전에 무엇을 신뢰해야 하는지를 규정한다.

연구진이 밝힌 다음 단계는 정리를 강화하고, 더 많은 후크 처리 루틴을 검증하고 암호학적 계약을 검증된 구현과 연결해 신뢰 기반을 줄이며, 그룹 메시징과 봉인 발신자 및 서버 측 프로토콜까지 검증 범위를 넓히는 것이다. 새 libsignal 릴리스를 출시 전에 검증한다는 목표는 연구 과제이지, 실제 배포가 발표된 것은 아니다.

이 결과가 갖는 즉각적인 의의는 보여 주는 역할 분담에 있다. 에이전트가 증명 구성을 맡았지만, 신뢰성은 여전히 사람이 검토한 명세와 명시적인 가정에 기반한다. 증명과 검증 절차를 공개하면 외부 검토자도 그 토대를 시험해 볼 수 있으며, 연구진은 이 작업 흐름을 지속적인 libsignal 개발에 적용하기 위해 노력하고 있다.