Google DeepMind 연구진이 에이전트형 AI로 메신저 Signal 프로토콜의 핵심 암호 보장 중 일부를 수학적으로 증명하는 형식 검증을 해냈다. 프로젝트는 개념 증명 성격으로 4주 만에 끝났고, DeepMind는 이 작업에 AlphaProof Code라는 새 AI 프레임워크를 썼다.
이번 결과는 Signal 앱과 Google Messages, WhatsApp 같은 서비스에서 대량의 통신을 지키는 암호 기술을 독립적으로 다시 확인했다는 의미가 있다. DeepMind는 Signal 분석을 연구 프로젝트로 무료 수행했다. Google은 분석 비용을 공개하지 않았고, 상용 형식 검증 제품이나 서비스를 낼 계획이 있는지도 답하지 않았다.
WIRED는 AI의 도움을 받는 형식 검증이 널리 쓰일 만큼 실용적인지, 많은 양의 코드 보안에 얼마나 효과가 있을지는 불확실하다고 지적했다.
검증 범위와 결과
분석 대상은 Signal 프로토콜의 일부였고, 모바일 앱 전체를 형식 검증한 것은 아니다. DeepMind 연구진은 이번 결과가 더 큰 과정의 한 단계라고 강조했다. 검증한 부분에서 새 취약점은 나오지 않았다. 반면 알려져 있고 오래전 수정된 취약점을 담은 옛 Signal 버전에 AlphaProof Code를 적용하자 그 결함을 정확히 짚어내고, 프로토콜을 형식 검증할 수 없다고 판정했다.
연구진은 Signal 프로토콜 분석을 위해 만든 명세와 증명을 공개해 다른 형식 검증 작업에 쓰도록 했다. 작업이 빨랐던 데에는 Signal Foundation이 앞서 진행한 형식 검증 작업 덕에 어느 정도 출발점을 확보한 영향도 있다고 연구진은 설명했다. Signal의 최고기술책임자 Ehren Kret은 성명에서 "이전 형식 검증은 코드의 더 작은 부분에 집중했지만, Google DeepMind의 접근은 범위를 크게 넓힐 수 있게 한다"고 밝혔다.
작동 방식과 남은 과제
형식 검증은 소프트웨어가 의도대로 작동하는지 수학으로 확인하고 검증하는 방법이다. 지지자들은 이를 소프트웨어에 치명적 취약점이 없다는 뜻으로 설명한다. 이때 의도는 사람이 기술한 소프트웨어의 성질을 기준으로 한다. AI 이전에는 증명할 성질을 기술하고, 이를 수식으로 바꾸고, 증명을 만드는 과정이 모두 매우 오래 걸렸다. 에이전트형 AI는 이 가운데 증명을 만드는 단계의 시간을 크게 줄일 수 있고, 그 덕에 DeepMind의 Signal 평가 같은 분석이 가능해진다.
DeepMind 연구 과학자 Swarat Chaudhuri는 핵심 진전 중 하나로 사람과 AI의 협업 절차를 꼽았다. 에이전트가 거의 모든 단계에서 기여하고 스스로 오류를 고치되, 주요 지점에서는 사람의 입력과 검토를 받는 방식이다. Chaudhuri는 AI가 목표와 증명을 모두 만들고 스스로 쓴 테스트를 통과하는 상황은 원하지 않으며 "중간 지점이 있다"고 말했다. 그는 세계의 모든 소프트웨어로 확장하기까지는 갈 길이 멀다고도 했다.
Google Cloud 최고과학자이자 DeepMind 연구 부사장인 Pushmeet Kohli는 구현의 정확성을 검증할 수 있다면 안심할 수 있다고 말했다. 은행처럼 보증을 중시하고 버그를 우려하는 기업이 "이 성질들을 증명할 수 있다"고 말하게 될 수 있다는 것이다. WIRED는 AI 자동화 형식 검증이 실용적 비용으로 대규모로 확장될 수 있는지가 업계의 열린 질문이라고 짚었다.
출처
이 기사는 아래 자료를 바탕으로 정리했습니다. 제목을 누르면 원문이 새 창으로 열립니다.
푸시미트 콜리