앤스로픽, 클로드로 오픈소스 123개 보안성 형식 검증

앤스로픽이 10월 22일 클로드를 활용해 구글의 오픈소스 소프트웨어 테스트 프로젝트 OSS-Fuzz에 등록된 오픈소스 라이브러리 123개의 보안 속성을 형식 검증했다고 발표했다. 형식 증명 전문 기업 시어럼과 공동으로 진행한 작업이다.

클로드는 이들 라이브러리의 테스트 진입점 239개에 대한 증명을 완성했다. 64MB 미만의 모든 입력에 대해 테스트가 중단 없이 종료되며 메모리 안전 오류나 단언 실패가 발생하지 않는다는 내용이다. 생성된 증명은 증명 보조 도구 로크(Rocq) 형식으로 총 1억 8천만 줄에 달했고, 증명 하나의 중앙값은 약 1만 8천 개의 RISC-V 명령어로 구성된 바이너리를 대상으로 했다.

증명 과정에서 클로드는 수백 건의 버그를 찾아냈다. 압축 해제기의 카운터 언더플로와 이미지 디코더의 범위 초과 읽기 등이 사례로 제시됐다. 클로드는 해당 코드를 수정한 뒤 수정된 코드를 다시 증명했다. 또 XML 파서 라이브러리 libexpat에서 CVE-2026-56132를 재발견했다.

앤스로픽은 이번 작업이 프로덕션 소프트웨어의 보안 속성을 어셈블리 코드 수준에서 대규모로 AI가 검증한 첫 사례라고 밝혔다. 회사는 생성된 증명 일부와 검증에 사용한 모델을 공개했으며, 시어럼은 다른 오픈소스 프로젝트에도 같은 방식을 적용할 수 있도록 지원한다.

별도 실험에서는 토큰 효율 개선

앤스로픽은 별도 실험에서 최신 모델 Opus 5.5가 36개의 검증 과제 가운데 절반을 해결했으며, 이때 Opus 5보다 약 40% 적은 토큰을 사용했다고 밝혔다. 에이전트 간 협업을 적용하면 토큰 사용량이 17% 줄었다. 이번 소식은 aitimes.com이 전했다.