Google DeepMind, AlphaProof Code를 사용해 Signal 프로토콜의 기계어 코드를 정식 검증했다고 밝혀

Google DeepMind의 Pushmeet Kohli는 자신의 팀이 Signal 메시징 프로토콜의 기반이 되는 기계어 코드의 핵심 보안 속성을 증명했다고 발표했습니다. DeepMind는 널리 배포된 프로토콜의 운영 코드가 이 정도 깊이로 어떤 방법을 통해서든 정식 검증된 것은 이번이 처음이라고 밝혔습니다. 이는 DeepMind 자체의 주장입니다.

이번 작업에는 DeepMind가 Gemini Carbon을 비롯한 LLM에서 실행되는 정식 검증용 새로운 에이전트 프레임워크라고 설명하는 AlphaProof Code가 사용됐습니다. DeepMind는 검증이 기기에서 실행되는 코드까지 이르렀으며, 작업에 약 한 달이 걸렸다고 밝혔습니다. 비슷한 작업에는 여러 팀이 총력을 기울여도 수십 년이 걸릴 수 있다고 덧붙였습니다. Signal 팀을 협력자로 언급했습니다.

DeepMind는 다른 이들이 이를 바탕으로 작업할 수 있도록 정식 명세와 검증 자료를 오픈 소스로 공개하고 있습니다. 11월 10일 오전 기준 X 게시물은 좋아요 1,297개를 받았습니다.