구글 딥마인드 연구진은 AI 시스템이 시그널 메시징 프로토콜의 중요한 보안 특성을 수학적으로 증명할 수 있음을 보였다. 연구진은 AlphaProof Code라는 새 프레임워크를 사용해 여러 암호학적 보장을 정형 검증했다. 이 작업은 약 4주 동안 진행된 연구 프로젝트로, 상용 제품은 아니다. 검토한 부분에서는 새로운 버그가 발견되지 않았으며, 프로토콜의 이전 버전에 적용했을 때 AI는 과거에 발견돼 이미 수정된 결함을 정확히 찾아냈다.
정형 검증은 소프트웨어가 의도한 대로 정확히 작동하는지 수학적으로 확인해 숨겨진 취약점이 끼어들 여지를 없애는 방법이다. 전통적으로는 전문가가 상세한 명세를 작성하고 이를 수식으로 옮긴 뒤 증명을 구성해야 했다. 손이 많이 드는 작업이라 몇 달이 걸리기도 했다. 딥마인드는 자체 하위 목표를 세우고 추진할 수 있는 에이전트형 AI에 작업의 상당 부분을 맡겨 기간을 몇 주로 줄였다. 연구진은 주요 단계에서 여전히 사람의 감독이 필요했지만, AI가 스스로 증명을 제안하고 오류를 바로잡을 수 있었다고 밝혔다.
시그널의 최고기술책임자(CTO)인 에런 크렛은 기존 검증 작업이 작은 코드 조각에만 적용됐다고 말했다. 그는 딥마인드의 접근법으로 검증 범위를 “크게 넓힐” 수 있다고 덧붙였다. 연구진은 다른 팀도 이를 토대로 작업을 이어갈 수 있도록 자신들이 만든 명세와 증명을 공개한다. 결과는 유망하지만, 딥마인드는 이를 앱 전체나 소프트웨어 공급망 전반으로 확대하는 일은 여전히 과제라고 경고했다. AI 기반 검증에 드는 비용도 공개되지 않았다.
왜 중요한가
AI가 암호화 프로토콜의 보안을 신뢰성 있게 증명할 수 있다면, 시그널과 Google Messages, WhatsApp 등 유사한 앱을 쓰는 일반 사용자들은 메시지가 비공개로 유지된다는 확신을 더 크게 가질 수 있다. 암호화된 통신에 의존하는 은행, 의료기관, 언론인 등은 이 기술을 통해 소프트웨어에 중대한 결함이 없다는 점을 법적으로 검증 가능한 방식으로 입증할 수 있게 될 가능성이 있다.
왜 중요한가
일반 사용자에게 이번 소식은 채팅을 보호하는 암호화가 추가적인 수학적 검증을 거쳐 숨겨진 버그가 있을 가능성을 낮췄다는 의미다. 개인정보 보호 규정 준수를 입증해야 하는 기업에는 AI 지원 검증이 오랜 수작업 감사 없이도 보안을 입증하는 새로운 방법이 될 수 있다.
