AlphaProof Code - Signal 암호화 구현을 기계어 수준에서 형식 검증

Google DeepMind가 인간 전문가와 AI 에이전트를 결합한 AlphaProof Code로 Signal 프로토콜의 실제 코드가 지정된 핵심 보안 속성을 충족함을 수학적으로 증명함 Signal 프로토콜의 참조 구현인 libsignal을 AArch64 Linux 기계어로 컴파일해 검증함. 검증한 속성에는 기기가 일시적으로 침해돼도 이전 메시지를 보호하고, 이후 메시지의 보호를 회복하는 성질이 포함됨 전문가가 검토한 수학적 명세를 바탕으로 Gemini Carbon 에이전트가 600만 줄 이상의 Lean 증명을 생성하고, Lean이 증명의 정확성을 자동으로 확인함 검증에는 4주가 걸렸으며, 에이전트의 증명 감사 결과 사람이 재검토해야 할 영역은 코드베이스의 1% 였음 이미 수정된 실제 버그 2개를 격리된 코드에 다시 넣은 실험에서는 두 경우 모두 안전하지 않다는 기계 검증 증명을 생성함 Signal의 설계에서 실제 구현까지 검증 Signal 프로토콜은 Signal과 Google Messages 같은 앱에서 수십억 건의 사적 대화를 보호하는 기술임 Google DeepMind 연구진은 AI 에이전트를 이끌어 실제 구현 코드의 핵심 보안 속성을 수학적으로 증명함 Google DeepMind에 따르면, 널리 배포된 암호화 프로토콜을 이 깊이까지 AI로 형식 검증한 첫 사례임 AI 사용 여부와 관계없이, 이처럼 널리 쓰이는 프로토콜의 구현을 해당 깊이까지 형식 검증한 것도 처음임 형식 검증은 코드가 올바르게 동작함을 수학적으로 증명하는 높은 수준의 보안 보증 수단이지만, 어렵고 많은 수작업을 요구하는 경우가 많음 암호화 프로토콜은 온라인 뱅킹부터 웹 브라우징까지 거의 모든 디지털 통신의 기반이며, 결함 하나가 수백만 명을 한꺼번에 노출할 수 있어 전문가들이 수십 년간 형식 분석을 수행해 왔음 기존 프로토콜 검증은 대부분 설계 수준에서 멈췄지만, 이번 검증은 기기에서 실행되는 컴파일된 코드가 지정된 보안 속성을 충족하는지까지 확인함 검증 대상에는 기기가 일시적으로 침해되기 전후에도 메시지를 보호하는 속성이 포함됨 실제 취약점은 설계와 구현 사이의 간극에 숨어 있는 경우가 많으며, 이 간극까지 다루면 증명이 훨씬 복잡해짐 전문가와 다중 LLM 에이전트의 역할 분담 AlphaProof Code는 연구팀처럼 형식 검증 작업을 나누는 다중 LLM 에이전트 프레임워크임 인간 전문가와 AI가 무엇을 증명할지 결정하고, AI 에이전...