앤트로픽, 클로드로 오픈소스 123개 검증

앤트로픽은 22일(현지시간) 정리증명 전문 기업 시어럼(Theorem)과 협력해, 구글의 OSS-Fuzz에 등록된 오픈소스 라이브러리 123개의 보안 속성을 클로드로 검증했다고 밝혔습니다. 몇 주 만에 239개 테스트 진입점에서 64MB 미만의 모든 입력이 충돌 없이 종료되는지 증명했고, 기존 퍼즈 테스트가 찾지 못한 버그도 발견했습니다. 앤트로픽은 실제 운영 소프트웨어의 보안 속성을 어셈블리 코드 수준에서 AI로 대규모 검증한 첫 사례라고 설명했습니다.

형식 검증은 프로그램을 수학적 모델로 표현해 코드가 정해진 규칙을 항상 만족하는지 증명하는 기술입니다. 기존에는 시간과 전문 지식이 많이 들어 항공전자 시스템이나 운영체제 커널처럼 안전성이 중요한 일부 소프트웨어에 주로 쓰였습니다. 마이크로커널 seL4 구현에는 약 2인년, 형식 검증에는 약 20인년이 걸렸습니다. 앤트로픽은 AI 모델의 추론 능력 발전으로 검증 자동화와 적용 확대가 가능해졌다고 설명했습니다.

이번 실험은 OSS-Fuzz의 기존 퍼즈 테스트를 검증 기준으로 삼았습니다. 퍼즈 테스트는 변형한 입력을 반복해 넣어 충돌이나 오류를 찾지만, 모든 실행 경로를 확인할 수는 없습니다. 클로드는 테스트를 컴파일된 RISC-V 어셈블리 코드의 수학적 명제로 바꾸고, 64MB 미만 입력에서 정상 종료와 메모리 안전성 오류·단언문 실패 여부를 증명했습니다. 대상은 RISC-V 프로세서에서 실행되는 단일 스레드 정적 바이너리이며, 리눅스와 고정 메모리 예산 등 특정 조건을 전제로 합니다.

완성된 증명은 로크(Rocq) 형식으로 총 1억8000만 줄이며, 증명 하나는 중앙값 기준 RISC-V 명령어 1만8000개 규모의 바이너리를 대상으로 일반적으로 60만 줄의 증명 코드를 포함했습니다. 로크의 증명 검사기가 명세 충족 여부를 확인하므로 사람이 방대한 코드를 일일이 검토할 필요는 없습니다. 다만 신뢰성은 명령어와 리눅스 프로세스 동작 모델, 명세, 검사기의 정확성에 달려 있습니다.

클로드는 증명 과정에서 문제를 직접 수정하고 수정 코드도 다시 검증했으며, 수백 건의 버그를 찾았습니다. 압축 해제 프로그램에서는 약 2000만 바이트 입력과 특정 데이터 배치에서 카운터 언더플로가 발생해 메모리 범위 밖 쓰기로 이어질 수 있음을 확인했습니다. 이미지 디코더에서는 약 6400만 바이트 입력과 2GB가 넘는 메모리가 필요한 범위 밖 읽기를 찾았습니다. 두 핸들을 특정 순서로 호출해야 생기는 메모리 접근 오류와, 깊게 중첩된 입력에서 나타나는 libexpat의 CVE-2026-56132도 다시 발견했습니다. 충돌은 없어도 파일 로딩 제한이 항상 적용되지 않는 논리 오류도 확인했습니다.

앤트로픽은 별도 실험에서 리눅스 커널의 zlib 구현이 기술 명세를 따르는지 증명하고, 러스트로 작성한 파이썬 인터프리터가 CPython과 동일하게 동작하는지도 검증했습니다. 무작위 생성 파이썬 프로그램 170만개 이상을 실행해 99.95%에서 같은 동작을 확인했습니다. 널리 쓰이는 PDF 리더 검증에서는 일주일 만에 통상 1년 동안 보고되는 수준의 보안 버그를 발견했고, 일부 핵심 소프트웨어에서 10년 넘게 잠복한 논리 오류도 찾았습니다.

이번 증명이 모든 버그의 부재를 보장하지는 않습니다. 64MB 미만 입력과 특정 실행 환경에 한정되며, 검증하지 않은 진입점이나 다른 프로세서·운영체제에서의 문제는 보장하지 않습니다. 메모리 안전성 도구 ASan도 모든 메모리 오류를 잡아내지는 못합니다. 자체 실험에서 오퍼스 5.5는 36개 검증 과제 중 절반을 오퍼스 5보다 약 40% 적은 토큰으로 해결했고, 여러 AI 에이전트가 증명을 공유하면 개별 작업보다 토큰 사용량이 17% 감소했습니다. 앤트로픽은 증명 일부와 검증 모델을 공개했으며, 개발자는 이를 재사용하거나 자체 코드 검증에 활용할 수 있습니다. 시어럼도 다른 오픈소스 프로젝트에 같은 절차를 적용하도록 지원하고 있습니다.

앤트로픽은 22일(현지시간) 정리증명 전문 기업 시어럼(Theorem)과 협력해, 구글의 OSS-Fuzz에 등록된 오픈소스 라이브러리 123개의 보안 속성을 클로드로 검증했다고 밝혔습니다. 몇 주 만에 239개 테스트 진입점에서 64MB 미만의 모든 입력이 충돌 없이 종료되는지 증명했고, 기존 퍼즈 테스트가 찾지 못한 버그도 발견했습니다. 앤트로픽은 실제 운영 소프트웨어의 보안 속성을 어셈블리 코드 수준에서 AI로 대규모 검증한 첫 사례라고 설명했습니다.

형식 검증은 프로그램을 수학적 모델로 표현해 코드가 정해진 규칙을 항상 만족하는지 증명하는 기술입니다. 기존에는 시간과 전문 지식이 많이 들어 항공전자 시스템이나 운영체제 커널처럼 안전성이 중요한 일부 소프트웨어에 주로 쓰였습니다. 마이크로커널 seL4 구현에는 약 2인년, 형식 검증에는 약 20인년이 걸렸습니다. 앤트로픽은 AI 모델의 추론 능력 발전으로 검증 자동화와 적용 확대가 가능해졌다고 설명했습니다.

이번 실험은 OSS-Fuzz의 기존 퍼즈 테스트를 검증 기준으로 삼았습니다. 퍼즈 테스트는 변형한 입력을 반복해 넣어 충돌이나 오류를 찾지만, 모든 실행 경로를 확인할 수는 없습니다. 클로드는 테스트를 컴파일된 RISC-V 어셈블리 코드의 수학적 명제로 바꾸고, 64MB 미만 입력에서 정상 종료와 메모리 안전성 오류·단언문 실패 여부를 증명했습니다. 대상은 RISC-V 프로세서에서 실행되는 단일 스레드 정적 바이너리이며, 리눅스와 고정 메모리 예산 등 특정 조건을 전제로 합니다.

완성된 증명은 로크(Rocq) 형식으로 총 1억8000만 줄이며, 증명 하나는 중앙값 기준 RISC-V 명령어 1만8000개 규모의 바이너리를 대상으로 일반적으로 60만 줄의 증명 코드를 포함했습니다. 로크의 증명 검사기가 명세 충족 여부를 확인하므로 사람이 방대한 코드를 일일이 검토할 필요는 없습니다. 다만 신뢰성은 명령어와 리눅스 프로세스 동작 모델, 명세, 검사기의 정확성에 달려 있습니다.

클로드는 증명 과정에서 문제를 직접 수정하고 수정 코드도 다시 검증했으며, 수백 건의 버그를 찾았습니다. 압축 해제 프로그램에서는 약 2000만 바이트 입력과 특정 데이터 배치에서 카운터 언더플로가 발생해 메모리 범위 밖 쓰기로 이어질 수 있음을 확인했습니다. 이미지 디코더에서는 약 6400만 바이트 입력과 2GB가 넘는 메모리가 필요한 범위 밖 읽기를 찾았습니다. 두 핸들을 특정 순서로 호출해야 생기는 메모리 접근 오류와, 깊게 중첩된 입력에서 나타나는 libexpat의 CVE-2026-56132도 다시 발견했습니다. 충돌은 없어도 파일 로딩 제한이 항상 적용되지 않는 논리 오류도 확인했습니다.

앤트로픽은 별도 실험에서 리눅스 커널의 zlib 구현이 기술 명세를 따르는지 증명하고, 러스트로 작성한 파이썬 인터프리터가 CPython과 동일하게 동작하는지도 검증했습니다. 무작위 생성 파이썬 프로그램 170만개 이상을 실행해 99.95%에서 같은 동작을 확인했습니다. 널리 쓰이는 PDF 리더 검증에서는 일주일 만에 통상 1년 동안 보고되는 수준의 보안 버그를 발견했고, 일부 핵심 소프트웨어에서 10년 넘게 잠복한 논리 오류도 찾았습니다.

이번 증명이 모든 버그의 부재를 보장하지는 않습니다. 64MB 미만 입력과 특정 실행 환경에 한정되며, 검증하지 않은 진입점이나 다른 프로세서·운영체제에서의 문제는 보장하지 않습니다. 메모리 안전성 도구 ASan도 모든 메모리 오류를 잡아내지는 못합니다. 자체 실험에서 오퍼스 5.5는 36개 검증 과제 중 절반을 오퍼스 5보다 약 40% 적은 토큰으로 해결했고, 여러 AI 에이전트가 증명을 공유하면 개별 작업보다 토큰 사용량이 17% 감소했습니다. 앤트로픽은 증명 일부와 검증 모델을 공개했으며, 개발자는 이를 재사용하거나 자체 코드 검증에 활용할 수 있습니다. 시어럼도 다른 오픈소스 프로젝트에 같은 절차를 적용하도록 지원하고 있습니다.