구글 딥마인드, 시그널 암호화 라이브러리 형식 검증 완료

구글 딥마인드가 2026년 11월 10일 공식 블로그를 통해 다중 AI 에이전트 형식 검증 시스템인 알파프루프 코드(AlphaProof Code)로 시그널의 핵심 암호화 라이브러리 libsignal을 형식 검증했다고 발표했다. 회사에 따르면 AI 에이전트들은 4주 동안 650만 줄이 넘는 수학적 증명 코드를 작성했다.

이번 검증은 종단간 암호화에 쓰이는 시그널의 PQXDH 핸드셰이크와 트리플 래칫(Triple Ratchet)을 대상으로 했다. 검증 결과 컴파일된 기계어 코드에서 기밀성, 인증, 전방향 비밀성, 침해 후 보안이 유지되는 것으로 나타났다. 양자컴퓨터 공격을 가정한 일부 보안 속성은 별도의 수학적 모델에서 검증됐다.

연구진은 이전에 수정된 시그널 버그 2개를 코드에 다시 삽입한 뒤, 두 버그 모두 보안 조건을 충족하지 못한다는 사실을 알파프루프 코드가 수학적으로 증명하도록 했다. 또한 추가적인 사람의 검토가 필요한 코드 영역은 전체의 약 1%로 좁혀졌다.

시그널 CTO 에런 크렛은 AI 에이전트가 형식 검증의 범위를 제한된 영역에서 실제 구현 코드로 크게 확장했다고 밝혔다. 구글 딥마인드는 이번 검증에 사용된 수학적 명세와 증명을 깃허브에 오픈소스로 공개했다.

다만 이번 검증은 특정 실행 환경에서 컴파일된 일대일 메시징 암호화 코드로 한정됐으며, 그룹 메시징과 다중 기기 상태는 다루지 않았다.

최근 암호 분야 AI 연구 흐름

구글은 2026년 11월 6일 AI가 RSA 암호에서 취약점 2개를 찾아냈다고 밝히고, 암호 키 소인수분해 비용을 최대 30분의 1로 줄이는 알고리즘을 공개한 바 있다. 이달 초 앤스로픽은 AI 모델의 응답이 특정 모델에서 나왔음을 암호학적으로 증명하는 FlashProve를 선보였다.