실시간 업데이트
구글 딥마인드, AI로 '시그널' 암호 코드 안전성 증명…증명 600만줄 쓰고 사람은 1%만 봤다
X 첫 글 17시간 전@GoogleDeepMind ♥ 1,033조회 6
구글 딥마인드가 인공지능(AI) 에이전트로 메신저 '시그널(Signal)'의 암호 프로토콜이 실제 코드 수준까지 안전하다는 것을 수학적으로 증명했다. 널리 쓰이는 암호 프로토콜의 구현 코드를 형식 검증한 것은 AI를 쓰든 안 쓰든 이번이 처음이라고 회사는 밝혔다.
10일(현지시간) 구글 딥마인드 공식 블로그에 따르면 새 에이전트 프레임워크 '알파프루프 코드(AlphaProof Code)'에서 제미나이 4 카본 기반 에이전트들이 증명 언어 '린(Lean)'으로 600만줄이 넘는 증명을 썼다. 사람 전문가가 다시 들여다본 부분은 전체의 1%였고, 보통 전문가 팀이 몇 년씩 걸리던 작업이 4주 만에 끝났다. 검증 범위도 설계 단계를 넘어 기기에서 실제로 도는 컴파일된 코드까지 넓혔다. 이미 고친 실제 버그 두 개를 일부러 되살려 넣자 시스템은 두 번 모두 '안전하지 않다'는 증명을 내놨다.
에런 크렛 시그널 최고기술책임자(CTO)는 "AI 에이전트로 실제 코드를 유효한 린 정리로 옮긴 것은 큰 돌파구"라며 "AI를 앞세운 보안 위협이 커지는 가운데 코드의 프라이버시 보장에 더 확신을 갖게 됐다"고 말했다. 이 프로토콜은 시그널과 구글 메시지 등에서 수십억건의 대화를 보호한다. X 발표 글은 두 시간여 만에 '좋아요' 1000개를 넘겼고, 답글에는 "실제로 설치하는 앱까지 검증한 건지, 참조 구현만인지"를 묻는 질문도 달렸다. 딥마인드는 검증 산출물을 오픈소스로 공개하고 다음 대상으로 의료기기 펌웨어와 전력망 소프트웨어를 꼽았다.
“For the first time, AI has mathematically proven @signalapp ’s protocol is secure down to the code level.”
