시그널 암호 코드 검증…AI가 650만줄 증명 코드 생성
제목 연관성·주요 수치·시장 영향·향후 전망을 기준으로 핵심 문장을 선별한 요약 브리핑입니다.
핵심 포인트
- 구글 딥마인드는 4주간 시그널 프로토콜의 일대일 대화용 코드에서 핵심 보안 성질을 검증했다.
- 구글 딥마인드가 AI 에이전트를 활용해 시그널 암호화 프로토콜의 일대일 대화용 코드에서 핵심 보안 성질을 수학적으로 검증했다.
- 분석은 4주간 진행됐으며, 그룹 대화나 시그널 앱 전체를 검증한 결과는 아니다.
본문
구글 딥마인드는 4주간 시그널 프로토콜의 일대일 대화용 코드에서 핵심 보안 성질을 검증했다. 구글 딥마인드가 AI 에이전트를 활용해 시그널 암호화 프로토콜의 일대일 대화용 코드에서 핵심 보안 성질을 수학적으로 검증했다. 분석은 4주간 진행됐으며, 그룹 대화나 시그널 앱 전체를 검증한 결과는 아니다. 구글 딥마인드(Google DeepMind)는 10일 공식 블로그와 기술 논문 및 증명 자료에서 ‘AlphaProof Code’를 이용한 연구 결과를 공개했다. AlphaProof Code는 사람이 정한 보안 조건을 바탕으로 AI 에이전트가 실제 코드의 증명을 작성하는 형식 검증 프레임워크다. 검증 대상은 libsignal 0.105.4와 SPQR 1.6.0으로 만든 일대일 대화용 실행 파일이다.
논문은 과거 메시지가 이후 키 유출로 드러나지 않게 하는 전방향 비밀성, 키가 노출된 뒤 보호를 회복하는 침해 후 보안, 상대 인증과 초기 연결의 비밀성을 증명 대상으로 들었다.
기호 모델은 양자 공격자가 디피-헬먼 키 교환을 깨는 경우에도 초기 연결의 비밀성을 다뤘지만, 계산 모델은 양자 공격자를 대상으로 하지 않았고 SPQR의 양자 공격 대응 복구 성질도 증명 범위에서 빠졌다. 다만 증명 대상은 시그널 앱 실행 파일이 아니라 연구진이 만든 명령줄 실행 파일이다. 암호 연산과 일부 라이브러리 기능은 계약된 조건대로 작동한다고 가정했으며, Lean 검사기와 AArch64 의미 모델도 신뢰 기반에 포함됐다. 연구팀은 다섯 명이 4주 동안 병렬로 작업해 약 650만줄의 Lean 증명 코드를 만들었다. 구글은 분석 비용과 상용 검증 제품·서비스 출시 계획을 공개하지 않았다.