DeepMind, AI로 Signal 암호 코드 4주 만에 형식 검증
Google DeepMind가 11월 10일 21시(한국 시각, 12:02 UTC) AlphaProof Code를 공개했습니다. 사람 전문가와 여러 LLM 에이전트가 함께 일하는 형식 검증 프레임워크로, Signal 프로토콜의 실제 코드가 핵심 보안 속성을 만족한다는 것을 수학적으로 증명했다고 밝혔습니다. DeepMind는 널리 쓰이는 암호 프로토콜의 구현이 이 깊이로 형식 검증된 것은 AI를 쓰든 안 쓰든 처음이라고 설명합니다.
1/설계가 아니라 실제 코드를 증명했습니다
형식 검증은 코드가 결함 없이 동작함을 수학적으로 증명하는 일로, 보안 보증의 가장 높은 수준으로 꼽힙니다. 기존 프로토콜 검증은 대부분 설계 단계에서 멈췄는데, 이번에는 컴파일된 코드가 보안 속성을 만족하는지까지 증명했다고 합니다. 증명 대상 속성의 예로는 기기가 일시적으로 탈취되기 전후에도 메시지가 보호되는 것이 있습니다. 실제 취약점은 설계와 구현 사이의 틈에 숨는 경우가 많아, 이 틈을 메우는 증명이 훨씬 복잡하다고 원문은 설명합니다.
2/사람이 무엇을 증명할지 정하고, 에이전트가 증명합니다
AlphaProof Code는 여러 LLM으로 구성된 에이전트 프레임워크입니다. 먼저 연구진이 여러 모델과 함께 Signal의 보안 목표를 형식 수학 명세로 옮겼고, 사람 전문가가 명세를 전부 검토했습니다. 이어 Gemini Carbon 기반 에이전트들이 증명을 맡아 Lean(코드의 정확성을 수학적으로 검증하는 언어)으로 600만 줄이 넘는 코드를 생성했습니다. 이후 에이전트가 증명을 스스로 감사해 사람이 다시 봐야 할 부분을 코드베이스의 1%로 추렸고, 나머지는 Lean이 자동으로 검사했습니다.
3/4주 걸렸고, 오류 코드는 걸러냈습니다
검증 작업은 4주 걸렸습니다. DeepMind는 전문가 팀이 보통 수년 걸리는 작업이라고 비교했습니다. 시스템이 올바른 코드와 버그 있는 코드를 구분하는지 확인하려고, 이미 수정된 실제 버그 2건을 Signal 코드의 격리된 버전에 다시 넣었습니다. 두 경우 모두 시스템은 버그 버전이 안전하지 않다는 기계 검증 증명을 내놓았습니다. Signal의 CTO Ehren Kret은 실제 코드를 Lean 정리로 옮기는 AI 에이전트 활용을 큰 진전이라고 평가했습니다.
4/검증 산출물 공개, 적용 확대는 추가 연구 필요
DeepMind는 형식 검증 산출물(formal verification artifacts)을 오픈소스로 공개하며, 기술 논문도 함께 냈습니다. 이용 방법이나 제공 지역, 가격은 공지에 없습니다. 원문은 이 기법을 확대하려면 추가 연구가 필요하다고 밝혔습니다. 향후 의료기기 펌웨어나 전력망 소프트웨어 같은 시스템으로 넓히는 기반이 될 수 있다고 하며, 자동 방어 에이전트 CodeMender와 함께 쓰는 구상도 내놓았습니다.
5/증명 비용이 병목이었다는 신호AMEET 해석
그동안 구현 수준의 형식 검증은 전문가 수작업 비중이 커서 범위를 넓히기 어려웠습니다. 이번 발표는 사람이 명세 작성과 1% 검토에 집중하고 나머지 증명을 에이전트와 Lean 검사기에 맡기는 분업이 가능하다는 사례입니다. 다만 근거는 Signal 한 건이고, 다른 코드베이스에서도 같은 시간과 비용으로 되는지는 공개된 논문과 산출물로 외부에서 확인할 부분입니다. 또 증명은 사람이 쓴 명세가 맞아야 의미가 있어서, 명세 검토의 질이 결과의 신뢰를 좌우합니다.