구글, AI로 암호 약점 발견 이어 시그널 보안 검증…650만줄 증명

AI 요약

구글 딥마인드는 10일(현지시간) 공식 블로그에서 다중 AI 에이전트 기반 정형 검증 시스템 알파프루프 코드(AlphaProof Code)로 시그널의 핵심 암호화 라이브러리 립시그널(libsignal)이 핵심 보안 조건을 실제 컴파일된 기계어 코드에서도 만족한다는 사실을 수학적으로 검증했다고 발표했습니다. AI 에이전트들은 4주 동안 650만줄 이상의 린(Lean) 증명 코드를 작성했고, 연구진이 승인한 수학적 명세를 바탕으로 PQXDH 핸드셰이크와 트리플 래칫의 기밀성·인증·순방향 비밀성·사후 침해 보안 등을 증명했으며 사람이 추가로 검토해야 하는 코드 영역을 전체의 약 1%로 좁혔다고 설명했습니다. 연구진은 과거 수정된 시그널 버그 2개를 코드에 다시 삽입해 알파프루프 코드가 두 사례 모두 보안 조건 미충족을 수학적으로 증명했고, 구글은 관련 수학적 명세와 증명 자료를 깃허브에 오픈소스로 공개했다고 밝혔습니다.