형식 검증이 버그 없음을 뜻하진 않는다…공개 증명은 25개
앤트로픽이 클로드로 오픈소스 라이브러리 123개의 크래시 부재를 수주 만에 형식 증명했다고 22일(현지시간) 밝혔다.
같은 날 공동연구 상대인 Theorem은 자격 있는 오픈소스에 동일 파이프라인을 무료로 돌리는 OSS Verify를 열었다. 앤트로픽이 밝힌 239개 진입점 중 GitHub에 공개된 증명은 60개뿐이다.
클로드, 239개 진입점 크래시 부재 증명
앤트로픽 프론티어 레드팀 연구에 따르면 클로드는 구글 OSS-Fuzz의 퍼즈 테스트를 사양으로 바꿔 RISC-V 바이너리에서 증명했다. 대상은 123개 라이브러리의 239개 진입점이다. 입력 64MB 미만에서 메모리 안전 오류나 단언 실패 없이 정상 종료함을 보였다.
파이프라인은 라이브러리와 퍼즈 테스트를 RISC-V로 컴파일한 뒤, Theorem의 RISC-V·리눅스 프로세스 의미론과 ‘크래시 없음’ 속성을 묶어 사양을 만든다. 클로드가 증명을 쓰고 Rocq 커널이 사양 충족 여부를 검사한다.
증명은 수주에 걸쳐 쌓였다. Rocq로 쓴 증명 코드는 약 1억 8000만 줄이고, 전형적 증명은 약 60만 줄이다. 중앙값 1만 8000개 RISC-V 명령어짜리 바이너리를 다룬다.
연구 부록은 시도 과정에서 쓴 증명 초안이 약 10억 줄에 이른다고 적었다. 그중 약 1억 8000만 줄이 검사기를 통과했다. cJSON의 391줄 파서 진입점은 63만 줄 증명을 받았다.
증명 과정서 수년간 놓친 버그 발견
증명이 실패하면 버그가 드러난다. 클로드는 패치를 넣고 사양을 다시 만든 뒤 증명을 이어갔다. 프론티어 레드팀은 이 과정에서 수백 건의 버그를 찾았다고 적었다.
한 압축 해제기의 카운터 언더플로는 약 20MB 입력과 드문 배치에서만 범위 밖 쓰기를 일으켰다. 이미지 디코더의 범위 밖 읽기는 64MB 입력과 2GB 넘는 메모리가 필요했다. libexpat에서는 CVE-2026-56132를 다시 확인했다.
퍼저는 보통 입력을 1MB 안팎으로 두고 커버리지로 탐색한다. 위 사례들은 그 범위를 넘는 입력에서 터졌다. 패치에는 패널티를 두고 바뀐 입력이 얼마나 적은지 증명하면 가점을 줬으며, 패치 로그를 감사했다.
검증됨이 버그 없음을 뜻하지는 않아
“형식적으로 검증됐다”는 말은 “버그가 없다”는 뜻이 아니다.
— 앤트로픽 프론티어 레드팀, 연구 게시물 10월 22일 · ""Formally verified” does not mean “bug-free.""
증명은 단일 스레드 정적 RISC-V 바이너리, musl, 고정 메모리 예산, 리눅스라는 가정 아래서만 성립한다. 대부분의 배포본은 x86이나 ARM에서 glibc와 동적 링크한다.
AddressSanitizer가 잡지 않는 메모리 오류는 범위 밖이다. 라이브러리의 모든 진입점을 검증한 것도 아니다. 개발자가 믿어야 할 대상은 RISC-V·리눅스 프로세스 형식 모델, 증명한 정리 문장, Rocq 검사기다.
Theorem이 OSS Verify 연다
Theorem의 OSS Verify는 OSS-Fuzz처럼 pull request로 등록한다. project.yaml, Dockerfile, build.sh를 넣고, 자격 있는 오픈소스는 비용이 없다. 우선순위는 널리 쓰이는 핵심 인프라다.
발견과 패치는 AI 모델이 생성하며, 보내기 전에 사람이 검토한다고 약속하지 않는다.
— Theorem, OSS Verify 10월 22일 · “Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them.”
공개 증명 저장소는 openssl, zstd, mbedtls, simdjson 등 25개 라이브러리의 60개 진입점을 담는다. Rocq 9.2.0으로 검사하며, 이번 공개분의 증명된 진술은 138개다. 프로그램이 끝나지 않는 실행을 배제하는 ‘halts’ 정리는 없다.
x86·ARM·glibc로 가정 범위를 넓히는 일정은 발표문에 없다.