딥마인드 AI, 시그널 암호 코드 기계어 수준서 증명

구글 딥마인드가 11월 10일(현지시간) 제미나이 기반 AI 에이전트로 암호화 메신저 시그널(Signal)의 핵심 코드가 주요 보안 성질을 갖췄음을 기계 검증 가능한 수학적 증명으로 입증했다고 발표했다. 대상은 시그널 프로토콜의 표준 구현체인 libsignal을 컴파일한 기계어 코드다. 딥마인드는 널리 쓰이는 이런 프로토콜의 실제 구현을 정형 검증한 것은 AI 사용 여부와 관계없이 이번이 처음이라고 밝혔다.

핵심 정리

• 딥마인드의 새 프레임워크 '알파프루프 코드(AlphaProof Code)'가 시그널 컴파일 코드에 대해 약 650만 줄의 린(Lean) 증명을 만들었다.
• 무엇을 증명할지는 사람이 정하고 승인했고, 증명은 에이전트가 썼다. 검증에는 4주가 걸렸다.
• 증명 범위는 일대일 대화에 한정된다. 그룹 메시지와 시그널 앱 전체는 포함되지 않는다.

알파프루프 코드가 검증한 시그널 보안 성질

기술 논문에 따르면 검증 대상은 libsignal v0.105.4다. 연구진은 코드를 고치지 않고 표준 러스트 컴파일러로 AArch64 리눅스 기계어로 빌드했다. 증명은 양자내성 키 교환인 PQXDH 핸드셰이크와 트리플 래칫을 다루며, 전방 비밀성·인증·침해 후 보안·핸드셰이크 비밀성을 입증했다.

기존 시그널 검증 연구는 대부분 추상 모델이나 다시 짠 코드를 다뤘다. 딥마인드는 실제 취약점이 설계와 구현 사이 틈에 숨는 일이 많아 실행 파일 자체를 증명했다고 설명했다.

AI 에이전트는 어떻게 일을 나눴나

딥마인드 블로그에 따르면 연구진은 먼저 여러 모델과 함께 시그널의 보안 목표를 정형 명세로 옮겼고, 전문가가 모든 명세를 검토했다. 이후 제미나이 카본(Gemini Carbon) 기반 에이전트가 모든 단계를 커널이 확인하는 증명 언어 린으로 증명을 작성했다.

논문은 증명 팀 하나가 보통 에이전트 40~80개로 구성돼 컴퓨터 한 대에서 24~72시간 동안 돌았다고 밝혔다. '게이트키퍼' 에이전트는 린 커널이 사람이 승인한 명세 사본과 대조해 확인한 증명만 받아들였다. 에이전트가 사람의 재검토가 필요하다고 표시한 부분은 코드베이스의 약 1%였다.

독자가 믿고 받아들여야 하는 신뢰 기반은 약 2만6000줄이다. 명세 약 1만8000줄과 AArch64 의미론 약 8000줄이며, 의미론 모델은 명령어 467개와 시스템 호출 31개를 다룬다.

실제 시그널 버그로 증명 시험

연구진은 명세가 실제 오류를 잡아내는지 보려고, 이미 고쳐진 libsignal 버그 2건을 격리된 빌드에 다시 넣었다. 두 경우 모두 시스템은 버그가 든 실행 파일이 보안 정리를 어긴다는 기계 검증 증명을 만들어 냈다.

에런 크렛(Ehren Kret) 시그널 최고기술책임자(CTO)는 딥마인드 발표에서 "AI 에이전트로 실제 코드를 유효한 린 정리로 옮긴 것은 큰 돌파구"라고 말했다.

정형 검증이 비쌌던 이유

정형 검증은 오랫동안 인력 부담이 걸림돌이었다. 논문에 따르면 seL4 마이크로커널 검증에는 20인년, C 컴파일러 컴프서트(CompCert)에는 6인년이 들었다. 둘 다 처음부터 검증을 전제로 짠 코드여서 libsignal 같은 실제 제품 코드와는 조건이 다르다.

AI 뉴스웨이가 11월 9일 보도한 마이크로소프트 리서치의 'PDD 키트'처럼, AI로 코드를 증명하려는 시도는 올가을 잇따르고 있다.

이번 증명의 한계

보장은 승인된 명세, 린 커널, 기계어 의미론, 그리고 신뢰 계약으로 처리한 암호 기본 요소에 대한 가정 위에 서 있다. 의미론은 스레드·시그널·동적 링크를 모델링하지 않는다. 논문을 검토한 미국 매체 유나이트AI는 키 생성, 부채널 공격, 다중 기기 상태도 범위 밖이라고 짚었다.

전망

딥마인드는 명세와 증명을 깃허브에 공개해 외부 전문가가 다시 확인할 수 있게 했다. 연구진은 그룹 메시지를 후속 과제로 꼽았고, 의료기기 펌웨어나 전력망 소프트웨어 같은 시스템으로도 확장할 수 있다고 내다봤다.

자주 묻는 질문

시그널에 버그가 하나도 없다는 뜻인가? 아니다. 특정 빌드 하나가 명시된 가정 아래 정해진 보안 성질을 갖췄음을 증명한 것이다. 명세 밖 영역은 다루지 않는다.

시그널 사용자가 할 일이 있나? 없다. 기존 코드를 검증한 연구로, 앱이 바뀌지는 않는다.

참고 자료

• Formal Verification of Signal's Protocol with Gemini — Google DeepMind(2026년 11월 10일)
• AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — Google DeepMind·Google(2026년 11월 10일)
• GitHub - google-deepmind/code-verification: Verifying Signal's security at the machine-code level — Google DeepMind
• Google DeepMind Uses AI Agents to Verify Signal's Core Machine Code — Unite.AI(2026년 11월 10일)