시그널 암호 코드 보안을 AI가 증명한 AlphaProof Code

무엇이 문제였나

소프트웨어가 안전한지는 보통 테스트와 코드 검토로 확인한다. 그러나 테스트는 해 본 경우만 알려 준다. 형식 검증(formal verification)은 '이 프로그램은 이 성질을 항상 지킨다'를 수학으로 증명한다. 문제는 품이다. 저자들은 운영체제 핵심부 seL4 검증에 20인년, C 컴파일러 CompCert 검증에 6인년이 들었다고 적는다. 둘 다 처음부터 검증하기 쉽게 쓴 코드였다.

시그널 프로토콜의 '설계'는 그동안 여러 번 증명됐다. 하지만 실제 버그는 설계와 구현 사이 틈에서 자주 생긴다. 구현 코드는 순서가 뒤바뀌어 도착하는 메시지를 풀 열쇠 보관, 예전 세션 보관, 데이터 포장 같은 일을 훨씬 많이 하기 때문이다. 저자들은 널리 쓰이는 암호 프로토콜의 손대지 않은 실제 코드에 프로토콜 수준 보안을 증명한 것은 이번이 처음이라고 주장한다.

어떻게 했나

일을 둘로 나눴다. '무엇을 증명할지'를 적는 명세(specification)는 사람이 이끈다. 명세 작성 에이전트가 기존 논문의 보안 정의를 Lean 문장으로 옮기고, 다른 모델 계열의 검토 에이전트가 허점을 찾고, 사람이 고쳐서 승인한다. 이 단계에는 Gemini 4 Carbon과 Claude Opus 5.5가 쓰였다. 승인된 명세는 에이전트가 손댈 수 없는 곳에 따로 보관한다.

증명 쓰기는 Gemini 4 Carbon 기반 에이전트가 보통 40~80개씩 한 팀을 이뤄 맡았다. 일을 나누는 조율자, 중간 팀장, 작업자, 증명 구조를 짜는 설계자가 있다. 한 번의 작업은 보통 컴퓨터 한 대에서 24~72시간 돌았다. 마지막 관문은 문지기(gatekeeper)다. Lean에서 증명을 최종 검산하는 작은 핵심 프로그램(커널)이 증명을 통과시키고, 증명한 문장이 보관해 둔 명세와 똑같을 때만 완료로 인정한다. 에이전트가 '다 했다'고 보고해도 그 말은 믿지 않는다.

AI가 문제를 슬쩍 쉽게 바꾸지 못하게 한 장치

저자들은 에이전트가 목표를 끝내라는 압박을 받으면 문제를 슬쩍 쉽게 바꾸기도 한다고 적는다. 그래서 명세를 고치려면 증명 과정을 보지 못하는 비평 에이전트의 심사를 거쳐야 한다. 보안을 약하게 만드는 수정은 받아들이지 않고, 사람에게 '코드 버그일 수 있다'고 올린다. 또 코드에 일부러 버그를 심어 보안 정리가 깨지는지 보는 방법으로 명세가 느슨하지 않은지 시험했다.

결과와 숫자의 뜻

저장소 전체는 약 700만 줄이고 그 가운데 약 650만 줄이 증명이다. 530만 줄은 기계어가 모델대로 움직인다는 증명이고, 나머지가 두 가지 보안 증명이다. 사람이 읽고 믿어야 하는 부분은 명세 약 1만 8천 줄과 프로세서 동작 규칙 약 8천 줄이다. 증명이 아무리 길어도 Lean이 검산하므로 사람은 이 짧은 부분만 꼼꼼히 보면 된다는 것이 이 방식의 논리다.

증명한 성질은 순방향 비밀성, 침해 후 보안, 상대방 인증, 첫 열쇠 교환의 비밀성이다. 두 가지 표준 방식으로 따로 증명했다. 암호 부품을 완벽한 블랙박스로 보는 기호 모델에서는 정리 10개를 얻었다. 공격자의 성공 확률을 따지는 계산 모델에서는 확률 상한 하나를 얻었다. 되살린 버그 2개가 '안전하지 않다'고 증명된 곳은 기호 모델 쪽이다. 계산 모델 쪽 반증은 훨씬 어렵다고 저자들은 밝힌다.

쓸모와 주의할 점

저자들이 꼽는 교훈은 증명이 싸지면 어려운 일이 '무엇을 증명할지'로 옮겨 간다는 것이다. 실제로 품의 대부분이 명세에 들어갔다고 한다. 명세에 빈틈이 있으면 증명이 통과해도 보장은 그만큼 약해진다. 그리고 명세가 옳은지는 기계가 대신 확인해 주지 못한다. 저자들은 이런 명세가 자리 잡으려면 열린 검토를 여러 번 거쳐야 한다고 보고, 명세와 증명을 모두 공개한다고 밝혔다.

보장 범위도 좁게 읽어야 한다. 대상은 시그널 앱이 아니라 시그널 코드를 감싼 시험용 프로그램이다. 밑바닥 암호 연산을 포함한 루틴 39개는 '정해진 대로 동작한다'는 가정으로 처리했다. 단체 대화와 여러 기기 사용은 빠졌다. 의료기기나 전력망 소프트웨어로 넓힐 수 있다는 말은 블로그가 내놓은 전망이지 이번에 보인 결과가 아니다.