시그널 암호 코드 검증…AI가 650만줄 증명 코드 생성

구글 딥마인드가 AI 에이전트를 활용해 시그널 암호화 프로토콜의 일대일 대화용 코드에서 핵심 보안 성질을 수학적으로 검증했다. 분석은 4주간 진행됐으며, 그룹 대화나 시그널 앱 전체를 검증한 결과는 아니다.

구글 딥마인드(Google DeepMind)는 10일 공식 블로그와 기술 논문 및 증명 자료에서 ‘AlphaProof Code’를 이용한 연구 결과를 공개했다. AlphaProof Code는 사람이 정한 보안 조건을 바탕으로 AI 에이전트가 실제 코드의 증명을 작성하는 형식 검증 프레임워크다.

형식 검증은 일부 입력을 넣어 오류를 찾는 시험과 다르다. 코드가 지켜야 할 조건을 수학적으로 표현하고, 실행 결과가 그 조건을 충족하는지 증명한다.

연구진은 사람이 어떤 보안 성질을 증명할지 정하고 명세를 작성·검토하도록 했다. AI 에이전트가 만든 증명은 Lean의 검사기를 통과해야 인정되며, 에이전트의 판단만으로 결론을 내리지 않는다.

검증 대상은 libsignal 0.105.4와 SPQR 1.6.0으로 만든 일대일 대화용 실행 파일이다. 연구진은 수정하지 않은 라이브러리를 명령줄 도구로 감싼 뒤 AArch64 기계어로 컴파일해 분석했다.

검증한 기능은 대화를 시작할 때 암호화 키를 합의하는 PQXDH와 메시지마다 키를 갱신하는 트리플 래칫이다. 시그널 프로토콜 계열은 시그널 앱 외에도 구글 메시지와 왓츠앱, 메타 메신저에서 쓰인다.

논문은 과거 메시지가 이후 키 유출로 드러나지 않게 하는 전방향 비밀성, 키가 노출된 뒤 보호를 회복하는 침해 후 보안, 상대 인증과 초기 연결의 비밀성을 증명 대상으로 들었다. 메시지 기밀성과 진위 확인도 검증 항목에 포함됐다.

연구진은 기호 모델과 계산 모델에서 각각 결과를 제시했다. 기호 모델은 암호 연산을 이상적인 대상으로 취급하고, 계산 모델은 계산 능력이 제한된 공격자를 가정해 보안 성질을 분석한다.

두 모델의 보장 범위는 같지 않다. 기호 모델은 양자 공격자가 디피-헬먼 키 교환을 깨는 경우에도 초기 연결의 비밀성을 다뤘지만, 계산 모델은 양자 공격자를 대상으로 하지 않았고 SPQR의 양자 공격 대응 복구 성질도 증명 범위에서 빠졌다.

이번 연구는 프로토콜 설계 문서에 그치지 않고 컴파일된 실행 파일의 동작을 명세와 대조했다. 다만 증명 대상은 시그널 앱 실행 파일이 아니라 연구진이 만든 명령줄 실행 파일이다.

결과에는 전제가 따른다. 암호 연산과 일부 라이브러리 기능은 계약된 조건대로 작동한다고 가정했으며, Lean 검사기와 AArch64 의미 모델도 신뢰 기반에 포함됐다.

검증 범위는 두 이용자 사이의 대화로 한정됐다. 그룹 메시징과 여러 기기의 상태, 시그널 앱 자체는 포함되지 않았고, 연구진은 논문에서 이 점을 범위의 한계로 명시했다.

연구진은 검증 방법이 결함을 가려낼 수 있는지 확인하기 위해 이미 발견돼 수정된 버그 두 개를 격리된 코드에 다시 넣었다. 두 경우 모두 보안 명제가 성립하지 않는다는 기계 검증 결과를 얻었으며, 새 취약점을 찾아낸 것은 아니다.

연구팀은 다섯 명이 4주 동안 병렬로 작업해 약 650만줄의 Lean 증명 코드를 만들었다. 논문은 증명에 필요한 신뢰 명세와 AArch64 의미 모델이 약 2만6000줄이라고 밝혔다.

에런 크렛(Ehren Kret) 시그널 최고기술책임자(CTO)는 “기존 형식 검증은 코드의 작은 부분에 집중했지만, 구글 딥마인드의 접근은 범위를 크게 넓힌다”고 말했다. 크렛은 프로토콜 구현을 더 넓은 범위에서 검증한 점을 평가했다.

와이어드(WIRED)는 이번 연구가 AI 보조 형식 검증의 실제 확장성과 비용 문제까지 해결했는지는 분명하지 않다고 짚었다. 구글은 분석 비용과 상용 검증 제품·서비스 출시 계획을 공개하지 않았다.

논문은 그룹 메시징과 발신자 비공개 기능, 서버 측 프로토콜을 후속 검증 범위로 제시했다. 구글 딥마인드는 명세와 증명 자료를 공개했다.