Anthropic, Claude가 123개 라이브러리의 보안 속성을 증명했다고 밝혀

Anthropic은 2026년 10월 22일, Theorem과 협력해 Claude가 123개의 오픈소스 라이브러리에서 퍼즈 테스트 진입점 239개의 RISC-V 어셈블리 코드 수준 보안 속성을 기계 검증 가능한 형식 증명으로 입증했다고 보고하는 연구 결과를 발표했다.

Anthropic에 따르면 Claude는 발견한 버그를 수정한 뒤, 64MB 미만의 모든 입력과 모델링된 모든 Linux 운영체제 응답 및 메모리 배치에서 프로그램이 메모리 안전성 오류나 어설션 실패를 일으키지 않고 항상 정상적으로 종료된다는 점을 증명했다. 이 증명은 프로그램이 Linux를 사용하는 RISC-V CPU에서 고정된 메모리 예산을 바탕으로 단일 스레드 정적 바이너리로 실행된다고 가정한다. Anthropic은 증명에 Rocq 코드 약 1억 8,000만 줄이 포함되며, 일반적인 증명은 중앙값이 RISC-V 명령어 1만 8,000개인 바이너리를 다루기 위해 약 60만 줄에 달한다고 밝혔다. 회사는 자사가 아는 한, 어셈블리 코드 수준의 프로덕션 소프트웨어에 형식 검증을 적용하는 데 AI를 활용한 첫 대규모 시도라고 말했다.

증명의 일부와 그 기반이 된 RISC-V 및 운영체제 의미론이 GitHub에 공개되고 있다. Anthropic은 프로젝트를 위해 구축했지만 아직 공개되지 않은 신뢰 기반 구성 요소, 패치가 필요하지 않았던 퍼즈 테스트의 완전한 증명, 그리고 증명에 실패한 퍼즈 테스트의 명세도 공개한다고 밝혔다. 다만 수정되지 않은 버그가 드러날 수 있는 증명은 공개하지 않는다.

퍼즈 테스트를 형식 증명으로 전환

이 접근법은 각 라이브러리에 이미 존재하는 컴파일 가능한 퍼즈 테스트를 형식 명세로 변환한다. 이 명세에는 64MB 미만의 모든 입력에서 테스트가 절대 충돌하지 않는다는 규칙 하나를 담는다. 명세는 Theorem이 정의한 RISC-V 명령어 집합 및 Linux 프로세스의 형식 의미론을 사용해 컴파일된 RISC-V 명령어를 대상으로 작성하며, Rocq 증명 검사기는 완성된 각 증명을 명세에 비추어 검증한다. Anthropic은 이로써 개발자가 신뢰해야 할 구성 요소가 세 가지로 한정된다고 설명한다. RISC-V와 Linux 프로세스의 형식 모델, 정확한 정리 진술, 그리고 Rocq 검사기 자체다.

Anthropic은 Google의 OSS-Fuzz 이니셔티브에 참여한 수백 개 프로젝트에 이 절차를 적용했다고 밝혔다. OSS-Fuzz는 자격 요건을 충족하는 오픈소스 프로젝트에 지속적인 퍼즈 테스트를 제공하고, 메모리에 부적절하게 접근할 때마다 프로그램을 충돌시키는 도구인 AddressSanitizer를 C 및 C++ 프로그램에 자동으로 삽입한다. 2026년 10월 22일자 부록에는 증명한 정리의 전체 내용이 명시되어 있다. 즉, 64MiB 미만의 모든 입력과 모든 메모리 배치에서 ASan이 삽입된 바이너리와 일반 바이너리 모두 오류를 일으키거나 중단되지 않고 모델링되지 않은 동작도 보이지 않으며, 읽기 및 쓰기 추적, 종료 동작, 최종 파일 시스템 상태가 서로 동일하다.

부록에 따르면 Claude는 이 작업을 수행하는 동안 Rocq 코드 약 10억 줄을 작성했으며, 그중 약 1억 8,000만 줄이 증명 검사기를 통과했다. cJSON의 391줄짜리 파서 진입점에는 63만 줄의 증명이 작성됐고, 링크된 코드가 5만 1,000줄인 fftw3에는 48만 줄의 증명이 작성됐다. Claude가 증명을 완료하기 전에 코드를 수정할 수 있었으므로 Anthropic은 패치에 불이익을 주고, 패치로 달라진 입력을 증명할 경우 추가 점수를 제공했으며, 보상 체계 악용을 막기 위해 패치를 기록하고 감사했다고 밝혔다.

증명 시도 중 발견된 버그

Anthropic은 증명을 시도하는 과정에서 수백 개의 버그가 드러났으며, 그중 다수는 퍼저가 찾아내기 어려웠을 버그라고 보고했다. 한 라이브러리의 진입점을 증명하던 중 Claude는 압축 해제기에서 카운터 언더플로를 발견했다. 이로 인해 범위를 벗어난 쓰기가 발생했지만, 약 20MB 크기의 입력과 드물고 특정한 메모리 배치가 함께 있을 때만 나타났다. 그 밖에도 입력이 64MB이고 메모리가 2GB를 초과해야 하는 이미지 디코더의 범위 초과 읽기, 동일한 파일을 가리키는 두 핸들에서 특정한 호출 순서를 거쳐야 발생하는 범위 초과 읽기, 그리고 깊게 중첩된 입력이 필요한 libexpat의 CVE-2026-56132 재발견 등이 있었다.

Claude는 충돌을 일으키지 않는 논리 버그도 발견했다. 여기에는 애플리케이션이 불러올 수 있는 파일을 제한하는 규칙이 항상 적용되지는 않는 문제가 포함된다. Anthropic은 널리 사용되는 여러 핵심 애플리케이션을 검증하는 과정에서 10년 넘게 잠복해 있던 미지의 논리 버그를 발견했다고 밝혔다. 또한 널리 사용되는 PDF 리더를 검증하는 작업을 진행하는 동안, 보통 1년간 보고되는 것과 같은 수의 보안 버그를 한 주 만에 찾아냈다고 말했다.

추가 실험 및 효율성 관련 결과

OSS-Fuzz 외에도 Anthropic은 Claude에 zlib 압축 형식을 정의하는 기술 문서인 RFC 1950의 형식 명세를 작성한 뒤, Linux 커널의 zlib 구현이 이를 올바르게 구현하는지 증명하도록 했다. Claude는 Claude가 생성한 x86 명령어 집합의 형식 의미론을 사용해 x86으로 컴파일된 바이너리를 직접 증명했다. Anthropic은 널리 사용되는 다른 라이브러리 여섯 개에도 이 절차를 반복했으며, 악용할 수 없는 사소한 예외 사례 버그를 발견해 각 프로젝트에 보고하고 있다고 밝혔다. 회사는 x86 의미론을 생성하는 과정에서 공식 참조 문서의 오류 수백 건과 하드웨어 자체의 버그 몇 건도 확인했다고 보고했다. 또한 의미론을 한 단계씩 실행하면 Linux 커널에서 Ubuntu 사용자 공간을 부팅할 수 있다고 밝혔다.

또 다른 실험에서 Claude는 Rust로 Python의 상당 부분을 구현하는 인터프리터를 만들고, Verus 검증 도구를 사용해 이 인터프리터가 학술 논문에 설명된 CPython 의미론을 준수한다는 점을 증명했다. 기술 부록에 따르면 인터프리터의 17개 계층 모두를 증명했으며, 정리는 “인터프리터가 결과를 반환할 때마다 그 결과는 형식 의미론이 규정하는 결과다”라는 내용을 담고 있다. Anthropic은 무작위로 생성한 Python 프로그램 170만 개를 대상으로 실증 테스트를 실시한 결과 테스트의 99.95%에서 CPython과 동일하게 동작했다고 밝혔다. 의도적으로 주입한 버그 7개 가운데 5개는 무작위 테스트에서 발견되지 않았지만, 7개 모두 증명을 깨뜨렸다.

효율을 측정하기 위해 Anthropic은 실제 OSS-Fuzz 진입점을 축소해 소규모 검증 작업 36개를 만들었다. 이렇게 만든 프로그램은 명령어 수가 283~2,491개였고, 입력 크기는 64바이트로 제한했으며, AddressSanitizer는 약 100개 명령어로 구성된 “mini-ASan” 런타임으로 대체했다. Anthropic에 따르면 Opus 5.5는 Opus 5보다 토큰을 약 40% 적게 사용해 작업의 절반을 증명한다. 또한 Anthropic은 공유 작업 공간에서 에이전트들이 서로의 증명을 복사할 수 있도록 했을 때, 각자 작업한 경우보다 토큰을 17% 적게 사용했다고 밝혔다. 일부 에이전트는 혼자 작업할 때 실패했던 증명에 성공했고, 혼자 작업한 에이전트들은 증명 2개를 완료하지 못했다. 회사는 OSS-Fuzz 작업을 대규모로 진행할 때도 같은 재사용 효과가 나타났다고 밝혔다. 에이전트 팀은 완성된 증명을 복사해 수정했는데, 각 증명의 상당 부분이 공통 C 런타임과 AddressSanitizer 초기화 코드를 다루기 때문이었다.

명시된 한계와 OSS Verify 프로그램

Anthropic은 이 증명이 라이브러리에 버그가 없다는 뜻은 아니라고 밝혔다. 남아 있는 버그는 신뢰하는 구성 요소 안에 있거나 증명 범위 밖에 있을 수 있다. 이 증명은 musl libc에 연결된 단일 스레드 정적 RISC-V 바이너리를 대상으로 하지만, 대부분의 사용자는 이 라이브러리를 x86 또는 ARM에서 실행하고 glibc에 동적으로 연결한다. 또한 AddressSanitizer가 모든 메모리 안전성 버그를 탐지하는 것은 아니다. 회사는 모델이 개선되면 이러한 한계를 해결할 수 있을 것으로 본다고 밝혔다.

Theorem은 OSS Verify 프로그램을 통해 자격을 갖춘 오픈소스 프로젝트에 동일한 파이프라인을 무료로 제공하고 있다. 프로그램의 저장소에 project.yaml, Dockerfile, build.sh 파일을 추가하는 풀 리퀘스트를 제출하면 등록할 수 있다. Theorem은 널리 사용되는 핵심 인프라를 우선시하며 OSS-Fuzz와 비슷한 기준으로 프로젝트를 검토한다고 밝혔다. Theorem에 따르면 프로젝트 관리자는 각 퍼즈 테스트 대상이 최대 64 MiB 크기의 어떤 입력에도 충돌하지 않는다는 Rocq 증명을 받으며, 이 증명은 Rocq 커널이 검증한다. 증명 과정에서 발견된 버그는 공개 기한 없이 이메일을 통해 프로젝트 관리자에게 비공개로 알리며, 증명을 만드는 데는 며칠이 걸릴 수 있다. Theorem의 로드맵은 glibc, OpenSSL, cURL과 같은 핵심 인프라를 포함해 Nix 생태계 전체를 검증하는 것을 목표로 한다.