앤트로픽, 클로드로 오픈소스 123개 라이브러리 검증...수십 년 버그도 발견

AI타임스 기사를 바탕으로 정리했어요. 발표는 22일(현지시간)이에요.

무엇을 했나요

앤트로픽은 정리증명 전문 기업 시어럼(Theorem)과 함께 구글의 오픈소스 테스트 프로젝트 OSS-Fuzz에 등록된 라이브러리를 대상으로 대규모 형식 검증을 했어요. 실제 운영 소프트웨어의 보안 속성을 어셈블리 코드 수준에서 AI로 대규모 검증한 첫 사례라고 설명했어요.

형식 검증이란

프로그램을 수학적 모델로 표현하고, 코드가 미리 정한 규칙을 항상 만족하는지 증명하는 기술이에요. 시간과 전문성이 많이 들어 항공전자나 OS 커널 같은 일부에만 쓰였어요. 예를 들어 마이크로커널 seL4는 구현에 약 2인년, 형식 검증에 약 20인년이 걸렸대요. AI 추론 능력이 좋아지면서 이걸 자동화하고 범위를 넓힐 수 있게 됐다는 거예요.

어떻게 했나요

• 기존 퍼즈 테스트를 검증 기준으로 썼어요. 퍼징은 무작위 입력을 반복해 넣어 충돌을 찾지만 모든 실행 경로를 볼 수는 없어요.
• 클로드가 이 테스트를 컴파일된 RISC-V 어셈블리 수준의 수학적 명제로 바꾸고, 64MB 미만의 모든 입력에서 메모리 안전성 오류나 단언문 실패 없이 정상 종료됨을 증명했어요.
• 결과: 123개 라이브러리, 239개 진입점 증명 완료. 대상은 RISC-V에서 도는 단일 스레드 정적 바이너리이고, 리눅스와 고정 메모리 예산을 전제로 해요.
• 증명은 정리 증명 도구 Rocq 형식으로 1억 8,000만 줄이에요. 증명 하나는 중앙값 1만 8,000개 명령어 바이너리에 보통 60만 줄이래요. 사람이 다 읽을 필요는 없고 Rocq 검사기가 확인하지만, 신뢰성은 RISC-V·리눅스 동작 모델, 명세, 검사기의 정확성에 달려 있어요.

찾아낸 버그

클로드는 증명 중 발견한 문제를 고치고 다시 증명했어요. 그 과정에서 수백 건의 버그가 나왔고, 일부는 퍼징으로 찾기 어려운 유형이었어요.

• 한 압축 해제 프로그램: 약 2,000만 바이트 입력과 특정 배치가 있어야 생기는 카운터 언더플로 → 범위 밖 쓰기 가능
• 한 이미지 디코더: 약 6,400만 바이트 입력과 2GB 넘는 메모리가 필요한 범위 밖 읽기
• 같은 파일의 두 핸들을 특정 순서로 호출해야 생기는 메모리 접근 오류
• XML 파서 libexpat에서 깊게 중첩된 입력이 필요한 CVE-2026-56132를 재발견
• 충돌은 없지만 파일 로딩 제한이 항상 적용되지 않는 논리 오류

다른 실험과 한계

• 리눅스 커널의 zlib 구현이 명세를 지키는지 바이너리 수준에서 증명했고, Rust로 쓴 Python 인터프리터를 무작위 프로그램 170만 개 이상으로 돌려 99.95%가 CPython과 같게 동작함을 확인했어요.
• 널리 쓰이는 PDF 리더에서는 일주일 만에 보통 1년치 수준의 보안 버그를 찾았고, 10년 넘게 숨어 있던 논리 오류도 나왔대요.
• 다만 이 증명이 모든 버그가 없다는 뜻은 아니에요. 64MB 미만 입력과 특정 환경이 전제이고, 검증하지 않은 진입점이나 다른 CPU·OS는 보장하지 않아요.
• 비용도 줄이고 있어요. 오퍼스 5.5는 36개 과제 중 절반을 오퍼스 5보다 약 40% 적은 토큰으로 풀었고, 에이전트끼리 증명을 공유하면 토큰이 17% 줄었대요. 증명 일부와 검증 모델은 공개됐어요.