Signal 암호화, AI가 쓴 650만 줄 수학 증명 통과

시그널의 암호화 코드에는 이제 널리 쓰이는 소프트웨어 가운데 거의 찾아보기 힘든 것이 하나 생겼다. 약속한 대로 작동한다는 수학적 증명이다. AI 에이전트 팀은 시그널 프로토콜을 구동하는 라이브러리인 libsignal을 분석해 일대일 대화가 비밀로 유지되고, 상대방이 누구인지 확인하며, 키를 도난당한 뒤에도 다시 공격자를 차단한다는 점을 증명했다. 새로운 결함은 발견되지 않았다.

이 성과는 시그널 이용자에게만 중요한 일이 아니다. 이 프로토콜은 종단 간 암호화 메시징의 세계 표준이며, 변형된 프로토콜이 WhatsApp, Messenger, Google Messages의 대화를 보호한다. 실제 배포된 코드를 이 정도 깊이까지 검증하는 일은 과거에는 시간이 너무 오래 걸려 거의 시도되지 않았다. 이 분야의 가장 큰 성과 가운데 하나인 검증된 운영체제 커널을 만드는 데는 20인년이 들었다. 이번 작업은 4주 만에 끝났다.

Google DeepMind가 만든 도구의 이름은 AlphaProof Code다. 먼저 인간 전문가와 AI 모델이 시그널의 보안 목표를 수학적 증명을 위해 설계된 프로그래밍 언어 Lean의 형식 명제로 옮겼고, 이를 모두 사람이 검토했다. 이후 Gemini Carbon으로 구동되는 에이전트 40~80개로 구성된 팀이 증명을 작성했다. 한 대의 컴퓨터에서 한 번에 24~72시간씩 작업을 진행했다. 완성된 결과물은 Lean 코드 약 650만 줄에 달한다.

이 수백만 줄을 사람들이 일일이 믿을 필요는 없다. Lean의 커널이 모든 단계를 확인하고 성립하지 않는 증명은 걸러내기 때문에, 어떤 모델이 작성했는지 또는 그 과정에서 몇 번이나 실수했는지는 중요하지 않다. 사람이 신뢰해야 하는 부분은 훨씬 작다. 명세 약 2만 6,000줄과 ARM 프로세서가 코드를 실행하는 방식을 나타낸 모델이다.

이번 증명은 대화를 지키는 시그널의 핵심 부분을 다룬다. 대화를 시작하는 PQXDH 핸드셰이크와 메시지마다 키를 바꾸는 Triple Ratchet, 그리고 미래의 양자 컴퓨터에 대한 저항을 목표로 하는 포스트양자 계층이 포함된다. 실질적으로는 휴대전화의 현재 키를 훔쳐도 이전 메시지를 열어볼 수 없으며, 양쪽이 새 키를 교환하면 도둑은 다시 접근할 수 없게 된다는 뜻이다.

시스템이 정상적인 코드와 문제가 있는 코드를 구별할 수 있는지 보여주기 위해 연구진은 이미 수정된 libsignal의 과거 버그 두 개를 다시 적용했다. 그중 하나는 라이브러리가 폐기했어야 할 비밀 키의 복사본을 계속 보관하게 만드는 버그였다. 두 경우 모두 AlphaProof Code는 버그가 있는 빌드가 안전하지 않다는 기계 검증 가능한 증명을 만들어냈다.

물론 한계도 분명하다. 이번 증명이 적용되는 것은 일대일 세션뿐이며, DeepMind는 그룹 메시징을 향후 과제로 꼽았다. 검증 대상은 ARM Linux에서 표준 Rust 컴파일러로 컴파일한 libsignal 버전 0.105.4를 작은 테스트 프로그램 안에서 실행한 경우다. iPhone, Android, 데스크톱용 시그널 앱 전체를 검증한 것은 아니다. 저수준 암호화 구성 요소는 안전하다고 가정했을 뿐, 증명된 것은 아니다. 사람이 승인한 명세에 오류가 있으면 보장도 약해진다. WhatsApp을 비롯한 다른 앱은 각자 프로토콜을 변형해 사용하므로 이번 결과가 자동으로 적용되지도 않는다. Google은 분석에 비용이 얼마나 들었는지, 또는 이를 서비스로 판매할 계획이 있는지 Wired에 밝히지 않았다.

시그널은 이번 성과를 환영했다. 시그널 최고기술책임자 에런 크렛(Ehren Kret)은 성명을 통해 “AI를 활용한 보안 위협이 커지는 가운데, 시그널 프로토콜 구현을 엄격하게 검증함으로써 코드가 개인정보를 보호한다는 보장에 더욱 큰 확신을 갖게 됐다”고 말했다. DeepMind 연구 과학자 스와랏 차우두리(Swarat Chaudhuri)는 한층 신중한 입장을 보였다. 그는 Wired에 이 방법을 “전 세계의 모든 소프트웨어”로 확장하기까지는 “갈 길이 멀다”고 말했다.

시그널을 쓰는 사람은 아무것도 설치하거나 설정을 바꿀 필요가 없다. 이번 증명은 이미 앱에 들어 있는 코드를 대상으로 한다.

DeepMind는 11월 10일 기술 논문과 함께 이번 연구를 공개했으며, 명세와 증명 자료를 GitHub에 오픈소스로 내놓았다. DeepMind는 시그널 프로젝트를 4월에 제시한 형식 검증의 대담한 도전 과제를 향한 이정표로 설명하며, 다음 검증 대상으로 의료기기 펌웨어와 전력망 소프트웨어 같은 시스템을 들었다.

차우두리는 이 작업에서 기계가 맡아야 할 범위에도 선을 그었다. 그는 Wired에 “AI가 목표를 만들고 AI가 증명까지 만들어내는 식의 분위기를 원하지 않는다”고 말했다. 무엇이 안전한지를 판단하는 것은 여전히 사람이며, AI는 그것을 증명할 뿐이다.

태그: 사이버 보안, Google DeepMind, AlphaProof Code, libsignal, Signal, 종단간 암호화