Google DeepMind, AlphaProof Code로 Signal 프로토콜의 핵심 암호 보장 형식 검증

Signal 프로토콜의 일부를 AlphaProof Code로 형식 검증한 결과, 새로운 취약점은 발견되지 않았으나 알려졌지만 수정된 취약점을 포함한 이전 버전에서는 이를 정확히 찾아내고 프로토콜이 형식 검증될 수 없음을 보였다고 한다. 검증 대상은 Signal 프로토콜의 일부였으며 Signal 모바일 앱 전체를 형식 검증한 것은 아니다. 연구진은 사양과 증명을 공개했으며 다른 형식 검증 작업을 촉진할 것이라고 밝혔다.

형식 검증은 소프트웨어가 의도한 대로 동작하는지를 수학적으로 확인하는 기법으로, 보안 분야에서 오랫동안 이상적인 방법으로 여겨져 왔다. 종래에는 검증하려는 속성을 기술하고, 이를 수식으로 바꾸고, 증명을 작성하는 데 많은 시간이 들었다. 에이전트형 AI는 특히 증명 작성에 드는 시간을 크게 줄일 수 있다고 한다. 이번 연구는 Signal Foundation이 과거에 수행한 형식 검증 성과가 출발점이 된 측면도 있다. Signal의 CTO Ehren Kret은 종래의 검증은 주로 작은 범위에 그쳤으나 DeepMind의 기법은 대폭적인 확장을 가능하게 한다고 말했다.

DeepMind의 Swarat Chaudhuri는 이번 결과를 환영하면서도, 전 세계의 모든 소프트웨어로 확대하기까지는 갈 길이 멀다고 말했다. 연구진이 중시한 것은 에이전트가 거의 모든 과정에서 기여하고 스스로 수정하되, 핵심 지점에서는 사람의 입력과 검토를 구하는 인간과 AI의 협업 프로세스이다. 목표와 증명을 모두 AI가 스스로 만드는 상황은 바람직하지 않으며 중간 지점이 있다는 입장이다.

한편 AI 기반 형식 검증이 실용적인 규모와 비용으로 성립할 수 있을지는 업계 전체의 미해결 과제다. 이번 분석은 연구 프로젝트로서 무상으로 수행되었으며, Google은 비용을 공개하지 않았다. 상용 형식 검증 제품이나 서비스를 제공할 계획에 대해서도 언급을 피했다. Pushmeet Kohli는 구현의 정확성을 검증할 수 있다면 은행 등이 속성을 증명할 수 있을 것이라고 말했다.