구글 딥마인드, AI로 시그널 프로토콜 보안을 형식 검증했다

와이어드에 따르면 구글 딥마인드 연구진은 AlphaProof Code라는 에이전트형 AI 프레임워크를 사용해 시그널 프로토콜의 핵심 암호학적 보장 여러 가지를 수학적으로 증명했다. 4주 만에 끝낸 개념 증명 작업인 이번 연구는 형식 검증에 해당한다. 형식 검증은 일부 사례만 시험하는 대신 수학을 이용해 소프트웨어가 의도대로 동작하는지 확인하는 방법이다.

시그널 프로토콜은 시그널 앱 뒤에 있는 암호화 방식이며, 와이어드가 지적하듯 구글 메시지와 왓츠앱의 통신도 보호한다. 따라서 이번 분석은 방대한 양의 메시지를 지키는 암호 기술에 대한 추가적인 독립 검증으로 소개된다. 와이어드는 암호학과 AI 자체에 이정표가 될 만한 성과라고 평가하면서도 범위가 제한적이라는 점을 강조한다.

딥마인드는 정확히 무엇을 증명했나

연구팀이 증명한 것은 프로토콜의 핵심 보장 중 "여러 가지"이며 전부가 아니다. 와이어드는 시그널 모바일 앱 전체를 형식 검증한 것은 아니라고 분명히 밝히고, 연구진도 이번 결과를 더 큰 과정의 한 이정표라고 설명한다. 딥마인드 연구 과학자 스와랏 차우두리는 와이어드에 "이 결과에 매우 들떠 있지만, 이를 세상의 모든 소프트웨어로 확장하기까지는 먼 길이 남아 있고 우리는 그렇게 하고 싶다"고 말했다.

같은 기사에 따르면 이번 분석은 검토한 프로토콜 부분에서 새로운 취약점을 찾지 못했다. 연구진은 오래전에 수정된 알려진 취약점이 들어 있는 시그널 구버전에도 AlphaProof Code를 적용했다. 도구는 이를 정확히 찾아냈고 그 버전들이 형식 검증을 통과할 수 없음을 보여 주었다. 결함이 없을 때 성공할 뿐 아니라 결함이 있을 때 실패할 수 있는 방법이라는 점을 보여 주기 때문에 이 시험은 의미가 있다.

• 도구: 구글 딥마인드의 새 에이전트형 AI 프레임워크 AlphaProof Code.
• 기간: 개념 증명 프로젝트로 4주.
• 결과: 핵심 암호학적 보장 증명, 분석한 부분에서 새 취약점은 없음.
• 구버전: 알려졌고 오래전에 수정된 결함을 탐지했으며 프로토콜이 검증 불가능함을 확인.
• 공개: 다른 형식 검증 작업을 돕기 위해 명세와 증명을 공개.
• 비용: 비공개, 연구 프로젝트로 무료 진행.

AI와 사람은 일을 어떻게 나눴나

AI 시대 이전에는 사람이 증명하려는 성질을 기술하고, 이를 수식으로 바꾼 다음, 증명을 만들어야 했다. 와이어드는 에이전트형 AI가 마지막 단계에 드는 시간을 크게 줄일 수 있으며, 그 덕분에 시그널 평가를 4주 만에 끝낼 수 있었다고 설명한다. 딥마인드 연구진은 시그널 재단이 이미 코드의 더 작은 부분에 대해 형식 검증을 해 두었기 때문에 출발이 유리했다고 덧붙인다.

시그널의 최고기술책임자 에렌 크레트는 와이어드가 인용한 성명에서 "이전의 형식 검증은 코드의 더 작은 부분에 집중했지만, 구글 딥마인드의 접근은 상당한 확장을 가능하게 한다"고 밝혔다. 그는 AI 기반 보안 위협이 커지는 만큼, 구현을 엄밀히 검증하면 코드의 프라이버시 보장에 대해 더 큰 확신을 얻는다고도 말했다.

딥마인드는 핵심 진전으로 "인간과 AI의 협업 과정"을 꼽는다. 에이전트는 거의 모든 단계에서 기여하고 스스로 오류를 고치며, 사람은 핵심 지점에서 검토한다. 차우두리는 "AI가 목표도 만들고 증명도 만드는 세상은 원하지 않는다"고 말했다. 형식 증명은 글로 적은 성질만 보장하므로 명세에 대한 사람의 검토가 계속 핵심이다.

시그널을 둘러싼 별도의 노력

딥마인드의 작업이 시그널 암호를 증명하려는 유일한 시도는 아니다. 비니피셜 AI 재단(Beneficial AI Foundation)은 시그널의 롤프 슈미트, Lean FRO와 함께 증명 보조 도구 Lean으로 프로토콜과 Rust 구현을 검증하는 공개 프로젝트 "Signal Shot"을 시작했다. 도구 Aeneas로 시그널의 Rust 코드를 Lean으로 변환할 계획이며, 검증 대상 구성 요소로 양자 내성 키 교환 PQXDH, 더블 래칫, SPQR/트리플 래칫 등을 꼽는다. 와이어드는 이 이니셔티브를 딥마인드의 작업과 연결하지 않으며, 두 노력은 서로 별개다.

아직 불확실한 점은 무엇인가

와이어드는 AI로 자동화한 형식 검증이 감당할 만한 비용으로 확장될 수 있는지가 열린 질문이라고 짚는다. 구글은 시그널 분석 비용 공개를 거부했고, 형식 검증 상용 제품이나 서비스를 계획하는지에 대해서도 언급하지 않았다. 구글 클라우드 최고 과학자이자 딥마인드 연구 부사장인 푸슈밋 콜리는 버그를 걱정하는 은행 등 기업이 자사 소프트웨어의 특정 성질을 증명할 수 있다고 말하게 되는 미래를 상상한다. 이는 구상일 뿐 발표된 제공 계획이 아니다.

기업에는 무엇이 달라지나

메신저 도구를 고르거나 시그널 프로토콜 위에 서비스를 만드는 기업에게 이번 결과는 프로토콜 설계에 대한 안심할 만한 신호이지만, 이를 쓰는 모든 앱에 대한 인증서는 아니다. 시그널 앱 전체는 검증되지 않았고, 제품의 배포 방식과 서버, 설정은 증명 범위 밖에 있다. 공개된 명세와 증명은 보안팀이 연구하고 재사용할 자료를 제공한다. 비용과 상용 서비스 여부를 알 수 없으므로 자사 코드를 이런 방식으로 형식 검증하는 일을 아직 기대할 수는 없지만, 핵심 소프트웨어 공급업체에 어떤 성질이 명세되고 증명되었는지 지금부터 물어볼 수 있다.