Anthropic, Claude를 사용하여 RISC-V 어셈블리 수준에서 123개 OSS-Fuzz 라이브러리 공식 검증

Anthropic과 Theorem이 발표한 내용

Anthropic은 검증 회사 Theorem과 협력하여 Claude가 이전에는 비현실적이었던 규모로 공식 소프트웨어 증명을 작성할 수 있다고 발표했습니다. 팀은 Claude를 사용하여 100개 이상의 실제 오픈소스 라이브러리에서 컴파일된 RISC-V 어셈블리에 대한 보안 속성을 직접 증명했습니다. 구체적으로 123개의 OSS-Fuzz 라이브러리에서 239개의 퍼징 진입점을 증명했습니다. Anthropic은 결과를 다음과 같이 설명합니다: "우리가 아는 한, 이는 AI를 사용하여 어셈블리 코드 수준에서 프로덕션 소프트웨어에 공식 검증을 적용한 최초의 대규모 노력입니다."

증명된 속성은 "버그 없음"보다 좁은 범위이며, Anthropic은 이를 명확히 밝히고 있습니다. Claude는 각 대상 프로그램이 64MB 미만의 모든 입력과 모델링된 모든 Linux 운영 체제 응답 및 메모리 레이아웃에 대해 메모리 안전 오류를 트리거하거나 어설션 실패 없이 항상 정상적으로 종료된다는 것을 증명했습니다. 이러한 증명은 프로그램이 RISC-V CPU에서 Linux를 실행하는 단일 스레드 정적 바이너리로 고정 메모리 예산 하에 실행된다고 가정합니다.

OSS-Fuzz 검증 노력의 주요 수치

  • 123개의 서로 다른 OSS-Fuzz 라이브러리에서 239개의 퍼징 진입점이 증명됨.
  • 총 약 1억 8천만 줄의 Rocq 증명.
  • 일반적인 증명에 약 60만 줄, 중앙값 18,000개의 RISC-V 명령어를 포함하는 바이너리 대상.
  • 증명을 생성하는 데 몇 주의 작업.

공식 검증은 역사적으로 컴퓨팅보다 전문가 시간이 많이 드는 작업이었습니다. Anthropic은 검증된 운영 체제 커널인 seL4를 예로 들며, 구현에 2인년이 걸렸지만 공식 검증에 20인년이 걸렸다고 언급합니다. 이러한 비용 프로필 때문에 검증은 Airbus 항공 전자 장치와 같은 임무 중요 코드에 국한되었습니다. 이 작업의 주장은 LLM 생성 증명이 이러한 계산을 변화시킨다는 것입니다.

퍼즈 테스트를 공식 사양으로 변환하는 방법

핵심 방법론적 움직임은 사양을 수동으로 작성하는 것을 피하는 것입니다. 대부분의 프로그램에서 포괄적이고 모호하지 않은 사양이 어려운 부분입니다. Anthropic이 묻듯이, 텍스트 편집기나 웹 브라우저가 "올바르다"는 것은 무엇을 의미할까요? 대신 팀은 "이 기존 테스트 스위트가 항상 통과한다"는 규칙을 컴파일된 RISC-V 명령어에 대한 공식 사양으로 인코딩하고, Linux에서 RISC-V 컴파일 바이너리를 실행한다는 일반적인 모델을 사용합니다.

구체적으로 파이프라인은 4단계로 작동합니다:

  1. 라이브러리와 기존 퍼즈 테스트가 RISC-V 실행 파일로 컴파일됩니다. OSS-Fuzz는 C 및 C++ 프로그램에 AddressSanitizer(ASan)를 자동으로 계측하여 잘못된 메모리 액세스를 충돌시킵니다.
  2. Theorem의 공식 RISC-V 명령어 및 Linux 프로세스 의미론은 기계 코드를 수학적 모델로 변환합니다.
  3. Claude는 생성된 사양이 유지된다는 Rocq 증명을 작성합니다.
  4. Rocq 증명 검사기가 사양에 대해 증명을 기계적으로 검증합니다.

사양은 퍼즈 테스트가 64MB 미만의 모든 입력에 대해 충돌하지 않는다고 명시합니다. 증명이 유지되면 해당 진입점을 퍼징해도 더 이상 아무것도 찾을 수 없습니다. ASan이 링크된 상태에서 "충돌 없음"을 증명하는 것은 범위를 벗어난 액세스를 충돌로 변환하므로 포함된 경로에 대한 메모리 안전도 설정합니다.

개발자가 실제로 신뢰해야 하는 것

Anthropic은 생성된 증명 코드 중 사실상 아무것도 인간 검토가 필요하지 않다고 주장합니다. Rocq 증명 검사기가 사양에 대한 증명의 정확성을 강제하기 때문입니다. 남아 있는 신뢰할 수 있는 아티팩트는 작고 열거 가능합니다:

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

Anthropic은 결과를 명확히 설명합니다: "이것은 이러한 라이브러리에 버그가 없다는 것을 의미하지 않습니다." 남아 있는 버그는 신뢰할 수 있는 구성 요소 내에 있거나 증명 범위 밖에 있습니다. 이러한 구성 요소를 강화하는 것은 사소하지 않지만, Anthropic은 증명으로 덮인 모든 줄을 감사하는 것보다 훨씬 더 다루기 쉽다고 주장합니다. 그리고 코드와 달리 신뢰 기반은 더 많은 프로젝트가 검증됨에 따라 증가하지 않습니다.

수년간의 퍼징이 놓친 버그 발견

증명을 시도하는 과정에서 수백 개의 버그가 표면화되었고, Claude는 자율적으로 패치할 수 있었습니다: 코드를 수정하고, 패치된 코드에서 사양을 재생성한 다음, Claude가 새 사양을 증명했습니다. 이는 많은 버그가 일반적으로 약 1MB로 제한된 작은 입력을 변형하고 커버리지 안내에 의존하는 기존 퍼징의 도달 범위를 벗어났기 때문에 중요했습니다.

Anthropic이 보고한 구체적인 예:

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

Anthropic은 이 점을 요약합니다: 궁극적인 목표인 완성된 무충돌 증명에 도달하지 못하더라도 시도 자체가 수정해야 할 실제 버그를 산출합니다.

메모리 안전을 넘어선 속성 증명

퍼즈 테스트가 절대 충돌하지 않는다는 것을 증명하는 것은 실제로 퍼즈 테스트가 종종 고급 속성을 인코딩하기 때문에 생각보다 강력합니다: 인코딩-디코딩 왕복, 멱등성, 대수 법칙, 차등 테스트, 자기 일관성 또는 참조 구현과의 동등성. 예를 들어 LZO 압축 알고리즘에 대한 퍼즈 테스트는 입력을 압축한 다음 압축 해제하면 원본이 반환된다고 주장합니다. 속성이 실패하면 프로그램이 충돌하므로 테스트가 절대 충돌하지 않는다는 것을 증명하는 것은 속성 자체를 증명하는 것과 동일합니다.

속성은 개발자가 명시하지 않아도 증명 중에 필요해질 수 있습니다. cpp-httplib에 대한 OSS-Fuzz 증명을 완료하기 위해 Claude는 std::set 소멸자의 과도한 재귀로 인한 스택 오버플로를 배제해야 했습니다. 재귀 깊이는 트리의 최대 깊이로 제한되므로 Claude는 libc++의 레드-블랙 트리 재균형 알고리즘이 트리 깊이를 로그로 제한한다는 것을 기계 코드에서 증명해야 했습니다.

같은 보고서의 다른 공식 검증 사례 연구

Anthropic은 OSS-Fuzz 파이프라인 외에 세 가지 추가 실험을 설명합니다.

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

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

중요 응용 프로그램의 보안 속성. 널리 사용되는 소프트웨어의 간단한 보안 속성을 검증하면 직접 문제가 표면화되었습니다: 한 응용 프로그램에서는 10년 이상 잠복해 있던 이전에 알려지지 않은 논리 버그가, 널리 사용되는 PDF 리더에서는 1년에 일반적으로 보고되는 만큼의 보안 버그가 1주일 만에 발견되었습니다.

비용, 토큰 효율성 및 증명 재사용

Anthropic은 비용을 현재 주요 제한 사항으로 지목합니다: 증명을 생성하는 데 수억 개의 토큰이 소요될 수 있습니다. 개선을 기대할 수 있는 두 가지 추세가 제시됩니다.

첫째, 최신 모델은 더 적은 토큰이 필요합니다. 실제 OSS-Fuzz 코드로 구축된 36개의 작은 검증 작업에서 Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 절반을 증명합니다. 각 작업은 5M 토큰 예산으로 3번의 독립적인 단일 에이전트 시도를 받았으며 첫 번째 시도가 완료되면 증명된 것으로 간주되었습니다. Anthropic은 모델이 긴 검증 작업에 대해 훈련됨에 따라 추세가 계속될 것으로 기대합니다.

둘째, 증명은 재사용할 수 있습니다. 증명은 소프트웨어와 마찬가지로 더 작은 증명에서 재귀적으로 구축되며 더 작은 증명은 재사용 가능성이 더 높습니다. 에이전트가 공유 작업 공간에서 작업하고 서로의 증명을 복사했을 때 단독 작업 에이전트보다 17% 더 적은 토큰이 필요했으며 일부 에이전트는 이전에 단독으로 실패한 후 성공했습니다. 36개 작업 실험 전반에 걸쳐 공유 작업 공간 비용은 34개의 완료된 증명 중 30개에서 단독 평균보다 낮았으며 단독 작업 에이전트는 그중 2개를 완료할 수 없었습니다.

동일한 효과가 OSS-Fuzz 노력에서 대규모로 나타났습니다. 모든 증명의 많은 부분은 모든 프로그램에 포함된 코드, 특히 C 런타임 및 AddressSanitizer 초기화에 관한 것이므로 관련 없는 프로그램은 크게 겹치는 증명을 갖게 됩니다. 에이전트 팀은 완성된 증명을 복사하여 자신의 프로그램에 적용했습니다. libcups, freerdp 및 libzmq에 대한 공개 비교에서 공유 부분은 거의 새 코드를 얻지 못했습니다.

Anthropic은 이를 Lean의 공식 수학 공유 라이브러리인 Mathlib에 비유합니다. Mathlib는 각각의 새 증명이 기존 작업을 기반으로 구축되기 때문에 700명 이상이 기여한 거의 300,000개의 정리로 성장했습니다. 회사는 OSS-Fuzz 증명의 하위 집합을 공개했으며 패치되지 않은 버그를 드러낼 수 있는 증명은 보류했습니다.

공개된 아티팩트 및 작업 재현 방법

  • 증명: 하위 집합이 github.com/theorem-labs/oss-verify-proofs에 게시되어 있으며, 패치가 필요하지 않은 퍼즈 테스트에 대한 완전한 Rocq 증명과 증명할 수 없는 퍼즈 테스트에 대한 사양이 포함되어 있습니다.
  • 의미론: 신뢰할 수 있는 모델로 사용된 RISC-V 및 Linux 프로세스 의미론이 github.com/theorem-labs/rocq-linux-process-semantics에 게시되어 있습니다.
  • 도구: Theorem은 개발자가 자신의 코드를 온보딩하는 데 도움이 되는 Claude 스킬을 게시했으며 다른 오픈소스 프로젝트에 대해 동일한 파이프라인을 실행할 것을 제안하고 있습니다.
  • 전체 부록: 더 긴 PDF 부록에는 추가 사례 연구와 외부 전문가의 증명 평가가 포함되어 있습니다.

LLM 지원 공식 검증의 명시된 한계

Anthropic은 "공식 검증"이 "버그 없음"과 동일하지 않은 이유에 대한 섹션을 할애하고 세 가지 뚜렷한 격차를 식별합니다.

실제 기계는 모델이 설명하지 않는 작업을 수행합니다. 증명은 musl libc에 링크된 단일 스레드 정적 RISC-V 바이너리에 관한 것이지만 대부분의 사용자는 x86 또는 ARM에서 이러한 라이브러리를 실행하고 glibc에 동적으로 링크합니다. 이 격차를 해소하려면 배포된 시스템과 더 유사한 시스템 모델(예: x86에 대한 정확한 의미론)이 필요합니다.

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

사양이 현실과 일치하지 않을 수 있습니다. 증명 검사기는 사양이 실제 세계와 일치하는지 여부를 알려줄 수 없습니다. Anthropic은 다음과 같이 씁니다: "Claude는 컴파일된 프로그램의 동작이 공식 사양의 요구 사항을 충족한다는 증명을 작성할 수 있습니다(외부 증명 검사기로 검증됨). 그러나 증명 검사기는 사양이 현실과 일치하는지 여부를 알려줄 수 없습니다." 검증된 코드에서 버그가 나타나면 사양이나 가정된 기계 의미론이 현실과 다르기 때문입니다. 이는 적어도 어디를 봐야 하는지 알려줍니다.

Hacker News 토론이 추가한 내용

토론에서 가장 많이 재인쇄된 비판은 검증이 사양만큼만 좋다는 것이었습니다. 한 댓글 작성자는 비전, 청사진, 검사를 사다리로 요약했습니다: "이 연구는 검사를 완벽에 가깝게 만듭니다. 그러나 검사는 청사진만 확인할 뿐 비전은 확인하지 않으므로 잘못된 청사진으로 지은 집은 완벽한 검사를 통과할 수 있습니다." 관련 댓글은 모델이 검증되는 프로그램을 충실히 나타내는지 어떻게 확신할 수 있는지 물었습니다. "실제로 프로그램이 아닌 것을 증명했을 가능성이 매우 높지 않나요?" 그리고 다른 댓글은 더 직설적으로 말했습니다: "현실에 대한 공식 사양을 상상해 보세요!"

두 번째 주제는 표준 검증 대 검증(validation) 구분이 여전히 적용된다는 것이었습니다. 한 댓글 작성자는 IEEE 용어로 설명했습니다: 검증은 "제품을 올바르게 만들고 있는가?"를 묻는 반면 검증은 "올바른 제품을 만들고 있는가?"를 묻습니다. "수학적으로 완벽한 코드를 작성하여 잘못된 문제를 매우 효율적으로 해결할 수 있습니다."

세 번째 주제는 예측된 능력 벽이었습니다. 한 댓글 작성자는 보고서 자체의 부록을 인용했는데, 에이전트가 장황한 증명 스타일을 더 복잡한 프로그램으로 확장할 수 있는지 묻고 "MachCSL과 같은 다른 에이전트 기반 검증 프로젝트의 경험에 따르면 답은 '아니오'일 수 있습니다: 에이전트는 장황한 증명 스타일로 복잡성 벽에 부딪혔습니다." 같은 댓글 작성자는 공식 검증이 LLM 추론에 대한 유용한 리트머스 테스트라고 주장했습니다. 이러한 시스템이 반드시 모델의 분포에 있는 것은 아니기 때문에 LLM이 인간이 만든 수학의 경계 바로 너머에서 정체될 것이라는 "볼록 껍질" 가설에 신빙성을 부여합니다.

스레드의 실무자들은 자신의 성공을 보고했습니다. 한 사람은 Rust와 C를 모두 Lean으로 변환하는 컴파일러를 구축하고 LLM이 동작 동등성을 증명하도록 했으며 단일 스레드 실행에 대해 코드의 약 12%(약 70,000줄의 C)를 다루었고 플랫폼 간 부동 소수점 동작과 같은 매우 사소한 차이를 발견했습니다. 다른 사람은 SIMD 또는 CUDA로 함수를 가속화하는 PR을 여는 에이전트를 설명하고 "PR에 원래 구현과 동작적으로 동등하다는 Rocq 증명이 있기 때문에" 자신 있게 병합했습니다. 세 번째 사람은 Codex를 사용하여 권한 부여 시스템의 Alloy 모델을 구축한 다음 서버를 몇 시간 동안 레드팀하여 권한 상승을 생성하지 못했다고 보고했습니다.

회의론은 기술적 한계보다 조직적 인센티브에 초점을 맞추기도 했습니다. 한 댓글 작성자는 채택이 따를지 의심했습니다: "소프트웨어에서 LLM을 채택한 것은 지금까지 모범 사례를 버리는 것이었기 때문에 검증 확장으로 이어질지 회의적입니다." 이는 경영진이 더 짧은 주 5일 근무를 예측하는 것에 비유했습니다. 다른 사람은 게으름이 실제 위험이라고 경고했습니다. 코드 검토를 건너뛰고 분위기 코딩으로 공식 검증을 하는 것은 여전히 문제를 일으킬 것이며 "완벽은 좋은 것의 적입니다."

여러 댓글 작성자가 노동 영향에 대해 직접 언급했고 한 사람은 보고서 작성자가 증명이 공식 아티팩트와 일치하지 않는 그럴듯한 논문이라는 Lean 비유와 일치한다는 점을 고려했는지 물었습니다. 이는 이전 OpenAI Lean 작업을 언급한 것입니다. 다른 사람들은 코드에서 증명으로의 워크플로에 대한 더 많은 세부 정보를 요청했으며 적어도 한 명은 Claude가 지시하지 않는 한 공식 검증을 사용하지 않는다고 언급했습니다.

이것이 소프트웨어 구축 방식에 중요한 이유

Anthropic의 결론은 완성된 제품 주장이 아니라 궤적 주장입니다: 공식 검증은 역사적으로 가장 안전에 중요한 코드에서 맞춤형 전문가 제작 보증에만 실용적이었지만, 퍼징이 오늘날 그런 것처럼 대부분의 프로덕션 소프트웨어에 실용적이 될 것이며 언어 설계 및 개발 워크플로 변경과 함께 볼트온에서 내장형으로 이동할 것입니다. 회사는 덜 강력한 모델로 공식 검증을 시도했지만 작동하지 않는다는 것을 발견한 개발자에게 다시 시도할 것을 명시적으로 권장합니다.

보고서는 또한 기존 소프트웨어 기반에 대한 전략을 설명합니다: 코드베이스가 다른 언어로 다시 작성할 필요가 없도록 일반 사양으로 바이너리 수준에서 검증하고 패키지 세분성에서 증명을 재사용하여 각 종속성이 한 번 검증되도록 합니다. 종속성은 멱법칙을 따르므로 소수의 공유 라이브러리 집합(Nix 생태계 내에서 Theorem의 로드맵은 glibc, OpenSSL 및 cURL을 명명)을 증명하면 소프트웨어의 많은 부분을 검증 가능하게 만들 수 있습니다.

Sources

관련