구글 딥마인드, Signal 암호화 코드를 AI로 수학 검증

한눈에 보기

구글 딥마인드가 AI 에이전트를 써서 메신저 Signal의 암호화 기술이 실제 실행 코드에서도 약속한 보안 성질을 지키는지 수학적으로 증명했어요. 형식 검증(코드가 정해진 대로 동작함을 수학으로 확인하는 방법)을 설계뿐 아니라 컴파일된 실제 코드까지 적용한 첫 사례라고 해요. 검증은 4주가 걸렸어요.

핵심만 콕콕

1. 1

   검증 대상은 Signal이 쓰는 암호화 라이브러리 libsignal의 컴파일된 코드예요.

2. 2

   사람 전문가가 보안 목표를 수학 명세로 옮기고, AI 에이전트가 600만 줄 넘는 증명 코드를 만들었어요.

3. 3

   증명이 맞는지는 Lean(증명을 자동으로 검사하는 도구)이 확인했어요.

4. 4

   사람이 다시 봐야 할 부분은 전체 코드의 1%였어요.

왜 중요할까요?

Signal은 수십억 건의 대화를 보호하는 기술이라, 구현까지 수학으로 확인하면 프라이버시 보장을 더 믿을 수 있어요. AI가 이런 검증 작업을 크게 줄일 수 있다는 점도 보여 줘요.

같은 소식을 전한 다른 곳

• WIREDA New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure
• Ars TechnicaSignal’s encryption just passed an AI-powered mathematical checkup
• Google DeepMind blogIntroducing AlphaProof Code: a breakthrough in verifying complex software at depth
• 뉴스N연합구글 딥마인드 '알파프루프 코드', 시그널 암호화 프로토콜 기계어 수준 정식 검증 성공…보안 인증 시장 재편 압력 가시화
• Unite.AIGoogle DeepMind, AI 에이전트로 Signal의 핵심 기계어 코드 검증
• knpp.co.kr구글 딥마인드 '알파프루프 코드', 시그널 암호화 프로토콜 기계어 수준 정식 검증 성공…보안 인증 시장 재편 압력 가시화
• VOI.ID구글 딥마인드, 신호 및 WhatsApp 암호화 프로토콜의 보안을 입증
• AI 매터스구글 딥마인드 ‘알파프루프 코드’, 시그널 암호 코드 4주 만에 검증