Anthropic의 LLM 정형 검증: Claude가 RISC-V 어셈블리 수준에서 123개 OSS-Fuzz 라이브러리의 비충돌 속성을 증명

Anthropic과 협력사 Theorem은 Claude가 123개의 실제 오픈소스 라이브러리에 대해 소스 코드가 아닌 컴파일된 RISC-V 어셈블리에서 직접 작업하여 비충돌 보안 속성을 자율적으로 증명했다고 보고합니다. Anthropic은 이를 어셈블리 코드 수준에서 프로덕션 소프트웨어에 AI 기반 정형 검증을 적용한 최초의 대규모 시도라고 부르며, 이 증명들이 수년간의 퍼징이 놓친 버그도 표면화했다고 말합니다.

발표 내용

핵심 주장은 LLM 지원 정형 검증이 실용성 임계값을 넘었다는 것입니다. 충돌을 확률적으로 탐색하는 퍼징에만 의존하는 대신, Claude는 정의된 범위 내에서 특정 컴파일된 프로그램이 어떤 입력에서도 충돌할 수 없다는 수학적 증명을 생성했습니다.

구체적으로, Anthropic은 Claude가 100개 이상의 실제 오픈소스 라이브러리에서 RISC-V 어셈블리 수준의 유용한 보안 속성을 증명했다고 보고합니다. 이 노력 전반에 걸쳐 Claude는 Google의 OSS-Fuzz 이니셔티브의 123개 라이브러리에 걸친 239개 진입점에 대한 증명을 완료했습니다. 이 작업은 기계 코드를 수학적 모델로 변환하는 데 사용된 RISC-V 명령어 및 Linux 프로세스 의미론을 제공한 Theorem과 협력하여 수행되었습니다.

Anthropic은 동기를 명확하게 제시합니다: 현존하는 가장 많이 테스트된 소프트웨어 중 하나인 Linux 커널은 최근 1,000개 이상의 취약점이 공개되었으며, 최첨단 모델은 점점 더 무해해 보이는 버그를 연결하여 심각한 익스플로잇으로 만들 수 있습니다. LLM이 대규모로 버그를 찾을 수 있다면, 방어자는 부재를 증명할 수 있는 기술이 필요하다는 논지입니다.

Claude를 사용하여 우리는 100개 이상의 실제 오픈소스 소프트웨어 라이브러리에서 어셈블리 코드 수준(RISC-V)의 보안 속성을 증명했습니다. 우리가 아는 한, 이는 프로덕션 소프트웨어에 어셈블리 코드 수준에서 AI를 사용하여 정형 검증을 적용한 최초의 대규모 시도입니다.

파이프라인이 퍼즈 테스트를 증명으로 전환하는 방법

파이프라인은 개발자가 이미 수행한 작업을 재사용합니다. OSS-Fuzz 프로젝트에는 속성이 위반될 때(예: 실패한 어서션 또는 AddressSanitizer가 감지한 부적절한 메모리 액세스) 프로그램을 충돌시키는 수천 개의 개발자 작성 진입점이 포함되어 있습니다. 해당 진입점과 기존 퍼즈 테스트는 RISC-V 실행 파일로 컴파일됩니다.

이 실행 파일은 Theorem의 RISC-V 및 Linux 의미론과 원하는 비충돌 속성과 결합되어 증명이 충족해야 하는 사양을 기계적으로 생성합니다. 그런 다음 Claude가 증명을 작성하고 Rocq 증명 검사기가 해당 사양에 대해 이를 검증합니다. 증명 시도가 실패하면 실패 지점이 실제 버그를 가리킵니다. Claude가 코드를 패치하고, 패치된 코드에서 사양이 재생성되며, 주기가 반복됩니다.

증명된 정확한 속성은 좁지만 의미가 있습니다: 이러한 프로그램은 64MB 미만의 모든 입력과 모델링된 모든 Linux OS 응답 및 메모리 레이아웃에 대해 메모리 안전 오류나 실패한 어서션을 트리거하지 않고 항상 정상적으로 종료됩니다.

증명은 명시된 가정 하에 유지됩니다: 프로그램이 Linux를 실행하는 RISC-V CPU에서 고정 메모리 예산으로 단일 스레드 정적 바이너리로 실행된다는 것입니다. Anthropic은 범위를 확장하려면 더 많은 어셈블리 아키텍처 및 기타 운영 체제 프로세스에 대한 의미론을 표준화하는 것이 포함될 것이라고 언급합니다.

증명 노력의 규모

숫자는 이것이 수작업 검증과 다른 체제임을 보여주는 헤드라인 증거입니다.

  • 123개 OSS-Fuzz 라이브러리에서 239개 진입점 증명
  • 총 약 1억 8천만 줄의 Rocq 증명 생성
  • 일반적인 증명은 약 600,000줄 실행
  • 증명으로 커버되는 중간 바이너리 크기: 약 18,000개의 RISC-V 명령어
  • 입력 범위: 64MB 미만의 모든 입력
  • 기간: 몇 주

Anthropic이 그리는 역사적 비교는 seL4 운영 체제 커널로, 구현에는 2인년이 걸렸지만 정형 검증에는 20인년이 걸렸습니다. 이 비율이 정형 검증이 Airbus의 항공 전자 코드와 같은 임무 중요 도메인에 국한된 이유입니다.

개발자가 여전히 신뢰해야 하는 것

1억 8천만 줄의 증명 코드 중 거의 대부분은 Rocq 증명 검사기가 검증하므로 수동 검토가 필요하지 않습니다. Anthropic은 개발자가 신뢰해야 하는 정확히 세 가지 산출물을 나열합니다:

  1. RISC-V 및 Linux 프로세스의 공식 모델
  2. 증명된 정확한 정리 명제
  3. Rocq 증명 검사기 자체

이것이 핵심 구조적 주장입니다. 신뢰할 수 있는 컴퓨팅 기반은 검증된 프로젝트 수에 따라 증가하지 않습니다. Anthropic은 이것이 라이브러리에 버그가 없다는 것을 의미하지 않는다고 명시적으로 경고합니다. 이는 남아 있는 버그가 해당 신뢰 산출물 내에 있거나 증명 범위 밖에 있다는 것을 의미합니다. Rocq, RISC-V 의미론 및 Linux 의미론을 강화하는 것은 실제 작업이지만 프로젝트별 부담이 아닌 제한된 작업입니다.

Claude가 증명을 작성하는 동안 찾은 버그

증명을 시도하는 것은 그 자체로 버그 찾기 프로세스로 판명되었습니다. Anthropic은 이 노력으로 수백 개의 버그를 발견했으며, 그 중 많은 버그는 퍼저가 발견할 가능성이 낮은 것들이라고 보고합니다. 그 이유는 기계적입니다: 퍼저는 일반적으로 1MB로 제한된 작은 입력을 변형하고 코드 커버리지에 의존하여 검색을 안내합니다.

Anthropic이 설명하는 구체적인 예:

  • 라이브러리의 압축 해제기 사본에서 카운터 언더플로로 인해 범위를 벗어난 쓰기가 발생했으며, 약 20MB 입력과 드물고 특정한 레이아웃에서만 도달 가능.
  • 이미지 디코더의 범위를 벗어난 읽기로 64MB 입력과 2GB 이상의 메모리가 필요.
  • 다른 라이브러리의 범위를 벗어난 읽기로 동일한 파일에 대한 두 핸들에 걸친 특정 호출 시퀀스가 필요.
  • 깊게 중첩된 입력이 필요한 libexpat의 CVE-2026-56132 재발견.
  • 충돌이 전혀 없는 순수 논리 버그: 한 라이브러리의 메모리 안전을 증명하는 동안 Claude는 응용 프로그램이 로드할 수 있는 파일을 제한하는 기능이 항상 적용되지 않는다는 것을 발견했습니다.

버그가 나타날 때마다 인간을 위해 멈추지 않기 위해 Anthropic은 Claude가 동일한 루프의 일부로 찾은 버그를 패치하도록 했습니다.

메모리 안전 이상 증명

퍼즈 테스트가 결코 충돌하지 않는다는 것을 증명하는 것은 실제 퍼즈 테스트가 메모리 검사뿐만 아니라 높은 수준의 속성을 인코딩하기 때문에 들리는 것보다 강력합니다. Anthropic은 인코딩-디코딩 왕복, 멱등성, 대수 법칙, 차등 테스트, 자기 일관성 및 참조 구현과의 동등성을 일반적인 예로 나열합니다. 예를 들어 LZO 압축 알고리즘에 대한 퍼즈 테스트는 입력을 압축한 다음 압축 해제하면 원본이 반환된다고 주장합니다. 실패하면 프로그램이 충돌하므로 테스트가 결코 충돌하지 않는다는 것을 증명하는 것은 속성 자체를 증명하는 것과 동일합니다.

때로는 필요한 의무가 개발자가 의도한 것보다 더 나아갑니다. cpp-httplib에 대한 OSS-Fuzz 증명을 완료하려면 Claude는 std::set 소멸자의 과도한 재귀로 인한 스택 오버플로를 배제해야 했습니다. 해당 재귀 깊이는 트리의 최대 깊이로 제한되므로 Claude는 libc++의 레드-블랙 트리 재균형 알고리즘이 트리 깊이를 로그적으로 제한된 상태로 유지한다는 것을 기계 코드 수준에서 증명해야 했습니다.

기타 정형 검증 사례 연구

Anthropic은 OSS-Fuzz 퍼즈 테스트-투-증명 파이프라인 외에 몇 가지 추가 실험을 설명합니다.

zlib 및 RFC 1950. Claude는 zlib 압축 파일 형식을 정의하는 문서인 RFC 1950의 공식 사양을 작성한 다음 Linux 커널의 zlib 구현이 해당 사양을 올바르게 구현한다는 것을 증명했습니다. RISC-V 작업과 달리 이 증명은 Claude가 생성하고 광범위하게 테스트한 x86 ISA의 공식 의미론을 사용하여 x86 컴파일 바이너리에서 직접 수행되었습니다. 이 프로세스는 다른 널리 사용되는 라이브러리 6개에 대해 반복되었으며 업스트림에 제출되는 과정에 있는 코너 케이스에서 사소하고 악용할 수 없는 버그를 발견했습니다. Anthropic은 두 가지 결론을 도출합니다: 이러한 매우 잘 테스트된 코드베이스는 이미 거의 완전히 정확하며, 실제 기존 코드베이스에 대해 종단 간 정확성 속성을 증명할 수 있습니다.

Rust로 작성된 Python 인터프리터. Claude는 Rust로 Python의 큰 하위 집합에 대한 인터프리터를 개발하고 Verus 검증 도구를 사용하여 학술 논문에 설명된 CPython 의미론을 준수함을 증명했습니다. 170만 개 이상의 무작위 생성 Python 프로그램에 대한 경험적 테스트에서 99.95%의 테스트에서 CPython과 동일한 동작을 발견했으며 나머지 차이는 놀랍지 않은 알려진 코너 케이스였습니다.

중요 응용 프로그램. 간단한 보안 속성에 대한 정형 검증 시도는 널리 사용되는 여러 중요 응용 프로그램에서 문제를 표면화했습니다. 한 경우 Claude는 10년 이상 잠복해 있던 이전에 알려지지 않은 논리 버그를 발견했습니다. 널리 사용되는 PDF 리더를 검증하는 동안 Anthropic은 1주일 만에 일반적으로 1년에 보고되는 만큼의 보안 버그를 발견했다고 보고합니다.

비용: 토큰 사용량 및 왜 감소해야 하는지

Anthropic은 토큰 비용을 핵심 제한 사항으로 식별합니다. 증명을 생성하는 데 수억 개의 토큰이 소요될 수 있으며, 이러한 방법이 전체 소프트웨어 생태계에 도달하려면 비용 효율성이 중요합니다. 두 가지 측정된 추세는 비용이 하락할 것임을 시사합니다.

첫 번째는 모델 개선입니다. Anthropic은 실제 OSS-Fuzz 코드에서 36개의 작은 검증 작업을 구축했습니다. Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 절반을 증명합니다. 각 작업은 5M 토큰 예산으로 3번의 독립적인 단일 에이전트 시도를 받았으며 첫 번째 시도가 완료되면 증명된 것으로 간주됩니다.

두 번째는 증명 재사용입니다. 에이전트가 서로의 증명을 복사할 수 있는 공유 작업 공간을 받았을 때 혼자 작업할 때보다 17% 적은 토큰이 필요했으며 일부 에이전트는 단독 시도가 이전에 실패했던 작업에서 성공했습니다.

동일한 효과가 OSS-Fuzz 노력에서 대규모로 나타났습니다. 증명의 대부분은 모든 프로그램에 포함된 코드, 특히 C 런타임 및 AddressSanitizer 초기화에 관한 것이므로 매우 다른 프로그램도 상당히 겹치는 증명으로 끝납니다. 에이전트 팀은 다른 팀의 완성된 증명을 복사하여 적용했습니다. libcups, freerdp 및 libzmq의 게시된 비교에서 각 증명은 동일하게 유지된 부분, 약간 편집된 부분, 더 많이 편집된 부분 또는 새로 작성된 부분으로 분류되며 공유 부분은 거의 새 코드를 얻지 못했습니다. 36개의 공유 작업 공간 증명 중 34개가 완료되었으며 그중 30개는 평균 단독 에이전트 시도보다 비용이 적게 들었습니다.

Anthropic은 이 역학을 Lean의 공식 수학 공유 라이브러리인 Mathlib에 비유합니다. Mathlib는 각각의 새 증명이 기존 작업을 기반으로 구축되기 때문에 700명 이상의 기여자가 제출한 거의 300,000개의 정리로 성장했습니다.

Anthropic이 인정하는 한계

게시물은 정형 검증이 사람들이 가정하는 보장을 제공하지 않는다는 점을 명시적으로 밝힙니다.

"정형 검증됨"이 "버그 없음"을 의미하지는 않습니다. 증명 검사기는 프로그램이 사양을 충족한다는 것을 보여줄 수 있지만 사양이 현실과 일치하는지 여부는 알 수 없습니다. 검증된 코드에 버그가 나타나면 사양 또는 가정된 기계 의미론이 현실과 다릅니다. Anthropic은 이것이 여전히 유용하다고 주장합니다. 남아 있는 버그를 찾을 위치를 알려주기 때문입니다.

실제 기계는 모델이 설명하지 않는 작업을 수행합니다. 증명은 musl libc에 연결된 단일 스레드 정적 RISC-V 바이너리를 다룹니다. 대부분의 사람들은 glibc에 대한 동적 연결로 x86 또는 ARM에서 이러한 라이브러리를 실행합니다. 이 격차를 해소하려면 예를 들어 x86에 대한 정확한 의미론을 생성하는 등 배포된 시스템과 더 유사한 시스템 모델이 필요합니다.

주장이 우리가 관심을 갖는 모든 것을 다루지 않을 수 있습니다. ASan은 모든 메모리 안전 버그를 감지하지 않으며 각 라이브러리의 모든 진입점이 검증된 것은 아닙니다. 모든 진입점을 검증한다고 해서 특히 죽은 코드가 존재하는 경우 전체 라이브러리를 다루지는 않습니다. 실제 프로그램은 호출자의 메모리를 손상시키는 방식으로 라이브러리를 오용할 수도 있습니다. 이 격차를 해소하려면 각 공용 함수에 대해 호출자가 수행해야 하는 작업을 지정하고 호출자가 이를 엄격히 준수해야 합니다.

공개된 내용

Anthropic과 Theorem은 게시물과 함께 여러 산출물을 게시했습니다:

  • github.com/theorem-labs/oss-verify-proofs의 증명 하위 집합. 패치가 필요하지 않은 퍼즈 테스트에 대한 Claude의 완전한 Rocq 증명과 증명할 수 없는 퍼즈 테스트에 대한 사양이 포함됩니다.
  • github.com/theorem-labs/rocq-linux-process-semantics의 RISC-V 및 OS 의미론.
  • 개발자가 자신의 코드 검증을 시작하는 데 도움이 되는 github.com/theorem-labs/oss-verify의 Claude 스킬.
  • 다른 오픈소스 프로젝트에 대해 동일한 파이프라인을 실행하겠다는 Theorem의 제안.

Anthropic은 오픈소스 소프트웨어에서 패치되지 않은 버그를 드러낼 수 있는 증명을 의도적으로 보류했으며 게시된 내용에 대한 독립적 검증을 초대합니다.

이것이 왜 중요한가

전략적 주장은 LLM이 취약점을 찾고 연결하는 데 더 능숙해짐에 따라 테스트만으로는 충분한 방어가 될 수 없다는 것입니다. 정형 검증은 확률이 아닌 보장을 제공하며 역사적 장애물은 가치가 아니라 증명 작성 비용이었습니다.

Anthropic은 또한 단위 경제성이 프로그램보다 패키지에 유리하다고 주장합니다. 증명 재사용은 패키지 수준 세분화에서 작동하므로 각 종속성은 한 번만 검증하면 되며 종속성은 멱법칙을 따릅니다: 소수의 공유 라이브러리를 증명하면 방대한 다운스트림 소프트웨어를 증명할 수 있게 됩니다. glibc, OpenSSL 및 cURL과 같은 중요 인프라를 포함하는 전체 Nix 생태계를 검증하기 위한 Theorem의 로드맵은 즉각적인 대규모 응용 프로그램으로 제시됩니다.

마지막 예측은 역사적으로 가장 안전에 중요한 코드에서 맞춤형 전문가 제작 보장에만 실용적이었던 정형 검증이 오늘날 퍼징이 거의 모든 프로덕션 소프트웨어에 실용적인 것처럼 실용적이 되어 애드온에서 내장으로 이동할 것이라는 것입니다. Anthropic은 이전에 덜 강력한 모델로 정형 검증을 시도했지만 작동하지 않는다는 것을 발견한 개발자에게 다시 시도할 것을 명시적으로 권장합니다.

Sources