AlphaProof Code: Signal 증명에서 사람이 여전히 책임지는 것

AI가 증명 코드를 써도 무엇을 증명해야 하는지는 자동으로 정해지지 않는다. DeepMind가 11월 10일 공개한 AlphaProof Code 연구는 Signal의 참조 구현 libsignal의 핵심 보안 속성을 기계어 수준에서 검증했다고 보고한다. Signal 앱 전체에 취약점이 없다는 선언과는 범위가 다르다.

생성된 증명은 검사기가 받아들여야 한다

연구의 2장은 사람이 방향을 정하는 명세 작성 에이전트, AArch64 기계어의 형식 의미론, 자율 증명 에이전트의 역할을 나눈다. 에이전트가 작성한 Lean 증명은 승인된 명세에 대해 Lean 커널이 검사해야 인정된다. 자연어 리뷰어의 동의 대신 명시된 정리와 규칙이 결과를 판정한다.

개념적으로는 ‘승인한 명세 → 증명 생성 → 커널 검사’의 경로다. 이는 논문의 구조를 설명한 것이며 이 글에서 증명 검사기를 실행한 결과가 아니다. 사람이 잘못된 속성을 승인했다면, 올바른 증명도 의도한 보안 요구사항을 대신 보장하지 못한다.

650만 줄과 신뢰해야 하는 코드는 다르다

7장에 따르면 5명이 4주 동안 작업했고 약 650만 줄의 Lean 증명이 생성됐다. 신뢰해야 하는 명세·정의는 저장소 코드 약 18,000줄과 AArch64 의미론 약 8,000줄 등으로 설명된다. 증명 줄 수를 안전성 점수로 읽어서는 안 된다. 검증 대상과 환경을 연결하는 정의가 어떤 가정을 두는지가 더 중요하다.

논문은 libsignal-cli 실행 파일의 동작과 Lean 모델을 연결하고, 모델에 대한 보안 게임의 결과를 기계어로 옮긴다. 암호학적 기본 요소의 계약과 실행 환경 가정도 검토 범위에 들어간다. 다른 빌드나 운영체제, 주변 서비스까지 같은 결론이 자동으로 확장되지는 않는다.

고쳤던 버그를 다시 넣는 이유

6장에서는 과거에 수정된 libsignal 버그 두 개를 재도입하고, 바뀐 바이너리가 상징적 보안 정리를 위반한다는 것을 Lean으로 증명했다. 이는 명세가 그 두 종류의 잘못된 동작을 구별하는지 확인하는 실험이다. 아직 알려지지 않은 모든 결함을 탐지한다는 근거는 아니다.

실무에서는 테스트에 일부러 결함을 넣어 탐지 여부를 확인하는 방식과 목적이 닮았다. 다만 여기서는 특정 보안 정리의 위반을 증명한다. 테스트가 실행한 입력의 결과를 관찰하는 것과 논리적 가정 아래의 속성을 다루는 것을 구분해야 한다.

작은 불변식부터 검토할 수 있다

팀이 먼저 정할 것은 도구 설치가 아니라 상태의 의미다. 예를 들어 권한을 철회한 뒤 이전 자격증명으로 보호된 연산을 허용하지 않는다는 조건을 정한다면, 철회 시점·동시 요청·캐시된 권한을 명세에 포함해야 한다. 이 예시는 편집상 적용 제안이며 이번 연구가 해당 업무를 검증했다는 뜻은 아니다.

명세가 안정되고 실패 비용이 큰 좁은 함수부터 시작할 이유가 있다. 요구사항이 계속 바뀌는 화면 전체에 같은 수준의 증명을 적용하려면 유지 비용을 먼저 판단해야 한다. 이 연구의 실무적 의미는 테스트를 없애는 데 있지 않다. 사람이 승인할 속성과 기계가 검사할 증거 사이의 경계를 구체화했다는 데 있다.