딥마인드, AI로 시그널 암호화 코드 수학적 검증

구글 딥마인드가 인간 전문가와 AI 에이전트를 결합한 AlphaProof Code로 암호화 메신저 시그널(Signal)의 실제 코드가 핵심 보안 속성을 지키는지 수학적으로 증명했습니다. 시그널 프로토콜의 참조 구현인 libsignal을 AArch64 리눅스 기계어로 컴파일한 뒤 검증을 진행했습니다. 검증한 속성에는 기기가 일시적으로 침해되어도 이전 메시지는 보호되고, 이후 메시지의 보호는 다시 회복되는 성질이 포함됩니다. 전문가가 검토한 수학적 명세를 바탕으로 Gemini Carbon 에이전트가 600만 줄 이상의 Lean 증명을 작성했고, Lean이 이 증명의 정확성을 자동으로 확인했습니다. 이 검증 작업에는 4주가 걸렸습니다.

이 일이 어디서 왔나

AI가 공격 도구로 쓰이며 보안 위협이 커지는 가운데, 전자신문은 10월 26일 크립토랩 천정희 대표의 발언을 통해 공격 탐지만으로는 방어가 충분치 않으며 데이터 자체를 보호하는 근본적 보안이 필요하다고 전한 바 있다. 이번 딥마인드의 작업은 같은 맥락에서, AI를 방어적으로 활용해 실제 상용 암호화 코드가 보안 속성을 지키는지를 수학적으로 증명한 사례다.