참고X
구글 DeepMind(딥마인드), AI 에이전트로 Signal 암호화 코드 형식 검증 성공
기존 전문가 팀이 수년 걸릴 작업을 AI로 4주 만에 완료. AI를 활용한 형식 검증(Formal Verification)의 실용 가능성을 입증함.
요약
Google DeepMind가 AI 에이전트를 활용해 Signal의 암호화 프로토콜을 머신 코드 수준까지 검증하는 데 성공했다. AlphaProof Code라 불리는 이 시스템은 Signal의 핸드쉐이크 및 메시지 래칫의 핵심 보안 속성을 다루는 약 650만 줄의 Lean 증명을 생성했다. 기존에 전문가 팀이 수년 걸리던 작업을 단 4주 만에 완료한 성과다. 연구진은 이전에 수정된 2개의 Signal 버그를 다시 도입해 테스트했으며, 시스템은 해당 버그들이 보안 보장을 깨뜨린다는 사실을 정확히 입증했다. 이번 사례는 AI가 복잡한 실무 소프트웨어의 정형 검증을 실용적인 수준으로 끌어올릴 수 있음을 보여주는 중요한 이정표가 될 전망이다.
AI가 원문을 요약한 내용으로, 부정확할 수 있습니다.
원문 제목 @mark_k: Google DeepMind has used AI agents to verify the actual compiled code behind Signal's encryption, down to the machine-code level.
원문 보기 ↗