딥마인드 AI, 시그널 암호 코드의 보안 속성 입증
편집·검토: AI Ping 편집팀
3줄 요약
- 1대1 대화의 세션 시작·메시지 송수신 코드를 검증했다.
- AI 증명은 Lean이 확인하며 명세·가정은 검토 대상이다.
- 과거 버그 재현 시험과 공개 증명 자료를 함께 제시했다.
구글 딥마인드가 11월 10일 AI 에이전트로 시그널 암호 구현의 주요 보안 성질을 수학적으로 검증한 알파프루프 코드(AlphaProof Code) 연구를 공개했다. 연구팀은 4주간 진행한 작업의 명세와 증명을 공개해 외부 연구자가 검증 범위와 전제를 살펴볼 수 있도록 했다. AI가 작성한 증명은 정리 증명기 Lean이 확인하는 방식이다.
검증 대상은 암호 라이브러리 libsignal의 1대1 대화 기능이다. 연구팀은 원래 코드를 작은 명령줄 프로그램에 연결해 AArch64 리눅스 실행 파일로 만들고, 세션 시작과 메시지 송수신을 분석했다. 일부 저수준 암호 연산은 정해진 계약을 충족한다고 가정했다. 키 생성은 검증 범위에서 제외했다. 시그널 모바일 앱 전체의 안전성을 입증한 결과로 확대해서 읽을 수는 없다.
시그널에서 대화를 시작하는 PQXDH는 두 사람이 공유할 비밀 키를 정하는 절차다. 받는 사람이 접속해 있지 않아도 서버에 올려 둔 공개 키 자료를 이용해 시작할 수 있다. 이후의 트리플 래칫은 기존 더블 래칫과 양자내성 키 갱신 체계를 결합한다. 메시지에 쓸 키를 갱신하는 부분까지 검증의 대상에 들어갔다. 시그널 명세는 순서가 뒤바뀐 메시지를 위해 건너뛴 키를 저장하고, 나중에 그 키를 꺼내 쓰면 저장 항목을 삭제하는 절차도 둔다. 메시지가 도착하는 순서와 키를 언제 남기고 지우는지도 구현이 처리해야 하는 상태 변화다.
시그널 명세의 전방향 비밀성은 현재 상태가 나중에 노출돼도 키를 이미 지운 과거 메시지의 비밀을 지키는 성질이다. 손상 후 보안은 침해가 끝난 뒤 새로운 비밀값을 섞어 미래 메시지의 보호를 회복하는 성질이다. PQXDH 명세는 양자내성 전방향 비밀성을 목표로 하면서, 현재의 상호 인증은 타원곡선 문제의 난해성에 의존한다고 명시한다.
연구자는 먼저 어떤 보안 성질을 확인할지 정했다. AI가 이를 수학적 명세로 옮기면 사람이 검토·승인하고, Gemini Carbon 기반 에이전트가 증명을 작성했다. Lean은 제출된 증명이 그 명세로부터 논리적으로 성립하는지 검사한다.
증명 650만 줄과 사람이 확인할 전제
논문에 따르면 AI가 만든 Lean 증명 코드는 약 650만 줄이다. 이와 별도로 독자가 읽고 신뢰해야 하는 명세와 AArch64 실행 의미론은 약 2만6000줄이다. 증명이 길어져도 무엇을 보안이라고 정의했는지, 실행 환경을 어떻게 가정했는지는 검토 대상에 남는다. 연구팀은 기계어까지 연결해 컴파일러의 정확성을 별도 전제로 두는 부담을 줄였다고 설명했다.
검사에는 증명 대상이 바뀌지 않았는지 대조하는 절차도 포함했다. 프로젝트가 사용하는 Comparator는 제출된 정리와 그 정의가 미리 보관한 문제와 일치하는지, 허용한 공리만 사용하는지 확인하고 Lean 커널에서 다시 검사한다. AI가 더 약한 조건을 증명해도 원래 요구를 충족한 것으로 받아들이지 않도록 하는 장치다. Comparator 문서도 문제 파일과 그 의존 정의가 신뢰할 수 있어야 하며 검사 커널의 정확성을 전제로 든다.
연구는 보안 성질을 두 방식으로 다뤘다. 기호적 모델은 암호 연산을 정해진 성질을 갖춘 추상 연산으로 취급한다. 계산적 증명은 공격자의 성공 가능성을 암호의 어려움에 관한 가정과 연결한다. 공개된 계산적 증명의 설명 문서는 고전적 공격자에 대한 부분을 사용한다고 명시한다. 보안 게임과 암호 가정을 담은 명세, Lean이 검사하는 증명, 조건이 빈약하지 않은지 살피는 시험도 나눠 공개했다. 이 결과를 모든 양자 공격에 대한 보장으로 확장할 근거는 제시되지 않았다.
연구팀은 수정이 끝난 과거 버그 두 개를 검증용 코드에 각각 다시 넣었다. 두 경우 모두 선택한 기호적 보안 명제가 성립하지 않는다는 Lean 증명을 작성했다.
공개 저장소는 논문의 정리와 Lean 코드를 연결하는 목록, 실행 파일 재현과 증명 재검사 절차를 제공한다. 문서는 기본 증명 검사에 수시간이 걸리고 최대 메모리 사용량이 약 15~34GiB라고 안내한다.
배포 코드는 기본적으로 Apache 2.0을 따르고, 복사한 시그널 libsignal 코드는 AGPL 3.0 라이선스를 유지한다.
출처
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth — Google DeepMind
- AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level — Google DeepMind / Google
- Formal Verification of Signal’s Security in Lean — repository and verification instructions — Google DeepMind
- Comparator — theorem statement and kernel checking — Lean
- Computational Security Proof — scope and documentation — Google DeepMind
- The PQXDH Key Agreement Protocol — Signal
- The Double Ratchet Algorithm — Triple Ratchet and integration with PQXDH — Signal
정정 내역
- 본문 검증 도식의 글자가 이미지 변환 과정에서 표시되지 않아, 같은 도식을 로컬에서 래스터화한 이미지로 교체했다.
