구글 딥마인드, AI를 활용해 시그널의 암호화 코드 검증

2026년 11월 10일, Google DeepMind는 AI 에이전트가 Signal 암호화 프로토콜의 주요 보안 메커니즘을 수학적으로 검증하는 데 도움을 준 연구 결과를 발표했습니다. 이 작업을 위해 과학자들은 대형 언어 모델, 형식 검증 도구 및 전문가의 감독을 결합한 AlphaProof Code 시스템을 개발했습니다. 연구자들에 따르면, 널리 사용되는 암호화 프로토콜의 보안 증명을 수정되지 않은 구현의 기계 코드와 연결하는 데 처음으로 성공했습니다.

이 프로젝트는 4주가 걸렸으며 5명의 연구자가 참여했습니다. 이 기간 동안 Gemini 4 Carbon을 기반으로 한 에이전트들은 Lean 언어로 약 650만 줄의 증명을 생성했으며, 이는 이 시스템의 수학적 코어에 의해 검증되었습니다. 결과는 기술 문서 및 소스 코드와 함께 발표되어 다른 전문가들이 검증을 연구하고 재현할 수 있도록 했습니다.

연구자들이 검증한 Signal 보안 메커니즘

연구의 주요 초점은 Signal 암호화 프로토콜을 구현하는 libsignal 라이브러리였습니다. 이 프로토콜은 동명의 메신저뿐만 아니라 WhatsApp 및 Google Messages를 포함한 다른 통신 서비스에서도 종단 간 메시지 암호화에 사용됩니다. 연구자들은 연결 설정 중 안전한 키 교환을 담당하는 PQXDH와 대화가 진행됨에 따라 암호화 키를 업데이트하는 Triple Ratchet이라는 두 가지 중요한 메커니즘을 조사했습니다.

검증은 여러 보안 속성을 다루었습니다. 그 중에는 메시지의 기밀성과 진위성, 이후 키가 손상된 경우 이전 통신의 보호, 특정 유형의 손상 후 추가 교환의 보안을 복원할 수 있는 능력이 포함되었습니다. 연구자들은 또한 잠재적인 양자 위협을 고려하여 연결 설정 절차의 특정 보안 속성을 분석했습니다.

전통적인 프로토콜의 수학적 모델 검증과 달리, DeepMind는 컴파일된 구현을 직접 연구했습니다. 이를 위해 연구자들은 libsignal의 0.105.4 버전을 사용하고 Arm 프로세서에서 사용되는 AArch64 아키텍처의 실행 코드를 조사했습니다. 이 접근 방식은 암호화 스킴뿐만 아니라 소프트웨어 구현이 지정된 보안 속성을 얼마나 잘 준수하는지도 검증할 수 있게 합니다.

AlphaProof Code가 AI를 사용하여 프로그램을 검증하는 방법

형식 검증은 개별 시나리오를 확인하는 대신 개발자가 특정 요구 사항의 충족을 수학적으로 증명하는 점에서 일반적인 테스트와 다릅니다. 예를 들어, 승인되지 않은 참가자가 메시지의 내용에 접근해서는 안 된다는 조건을 수립하고, 모델이 제공하는 모든 경우에 이 조건이 유지되는지 확인합니다.

AlphaProof Code에서는 이 과정이 검증할 속성의 정확한 수학적 설명인 형식 사양을 작성하는 것으로 시작됩니다. AI 에이전트는 보안 요구 사항을 Lean 언어의 표현으로 번역하는 데 도움을 주지만, 최종 공식은 사람이 확인하고 승인합니다. 이후 또 다른 에이전트 그룹이 증명을 생성하며, Lean 시스템은 그것들이 어떻게 얻어졌는지와는 무관하게 독립적으로 검증합니다.

연구 중에 약 650만 줄의 기계 검증된 증명이 준비되었습니다. 이들은 약 26,000줄의 신뢰할 수 있는 사양과 프로세서 아키텍처 작동 설명에 의존했습니다. 시스템은 또한 추가적인 인간 검증이 필요한 영역을 강조하여 연구자들이 가장 중요한 가정에 집중할 수 있도록 했습니다.

AlphaProof Code의 실제 문제 탐지 능력을 테스트하기 위해 팀은 코드의 개별 버전에 이전에 수정된 두 가지 취약점을 다시 도입했습니다. 두 경우 모두 시스템은 지정된 보안 속성의 위반을 수학적으로 입증할 수 있었습니다. 이 실험은 도구가 구현의 정확성을 확인할 뿐만 아니라 특정 오류를 식별할 수 있음을 보여주었습니다.

이것이 Signal이 완전히 안전하다는 것을 의미하는가

결과에도 불구하고, 연구는 전체 Signal 시스템을 다루지 않습니다. 연구자들은 두 참가자 간의 메시지 교환을 위한 암호화 프로토콜의 특정 구현을 검증했으며, 모바일 애플리케이션의 모든 기능을 검증한 것은 아닙니다. 그룹 채팅, 장치 및 서버 작동의 특정 기능, 일부 유형의 소프트웨어 공격은 이 작업의 범위 밖에 있었습니다.

또한, 수학적 증명은 사용된 암호화 알고리즘의 보안에 대한 특정 가정 하에서 유효합니다. 연구자들은 암호화 작업이 이상화된 형태로 간주되는 상징적 모델과 주어진 조건 하에서 공격자의 능력을 고려한 계산적 모델을 적용했습니다. 그러나 계산적 증명은 양자 적대자에게까지 확장되지 않으며, Triple Ratchet의 일부 양자 이후 속성은 여전히 별도의 검증이 필요합니다.

연구자들은 현재 구현의 검증된 구성 요소에서 새로운 취약점을 발견하지 못했습니다. 그러나 이는 애플리케이션의 다른 부분에서의 문제를 배제하지 않으며, 모든 상황에서 시스템 보안을 보장하지 않습니다.

이 연구가 소프트웨어 개발에 중요한 이유

Google DeepMind에 따르면, AlphaProof Code는 복잡한 소프트웨어의 형식 검증에 필요한 노동을 크게 줄일 수 있습니다. 이전에는 이러한 프로젝트가 전문가들의 수년간의 작업을 필요로 했습니다. 예를 들어, seL4 운영 체제 마이크로커널의 형식 검증에는 약 20인년이 필요했고, 검증된 CompCert C 컴파일러의 개발에는 6년이 걸렸습니다.

새로운 접근 방식에서 가장 노동 집약적인 부분은 증명의 생성이 아니라 소프트웨어의 어떤 속성을 검증해야 하는지를 결정하는 것이었습니다. 인간과 AI의 협업은 증명의 준비를 가속화했지만, 수학적 모델과 그 한계에 대한 전문가 평가의 필요성을 없애지는 않았습니다.

미래에 Google DeepMind는 은행 소프트웨어 및 중요한 인프라를 포함한 다른 복잡한 소프트웨어 시스템에 유사한 방법을 적용할 계획입니다. 그러나 더 큰 코드베이스로 기술을 확장할 가능성, 계산 비용, 필요한 인간 감독의 양은 여전히 열린 질문으로 남아 있습니다.