앤트로픽, Claude로 오픈소스 코드 "충돌 없음" 증명
앤트로픽이 Claude에게 오픈소스 코드가 충돌하지 않는다는 것을 수학적으로 증명하게 해, 구글 OSS-Fuzz에 등록된 라이브러리 123개의 진입점 239곳에서 증명을 마쳤다. 증명하는 과정에서 수조 번의 테스트에도 드러나지 않던 버그를 찾아 고쳤지만, 보장 범위는 RISC-V 프로세서용으로 만든 실행 파일로 한정된다.
이 에게 오픈소스 라이브러리의 보안 성질을 수학적으로 증명하게 해, 라이브러리 123개의 진입점 239곳에서 증명을 마쳤다. 증명하는 과정에서 수조 번의 테스트에도 드러나지 않던 버그도 찾아냈다.
앤트로픽은 AI가 버그를 쉽게 찾아 악용하는 지금은 기존 방어만으로 부족하고, 코드에 버그가 없다는 것을 증명할 방법이 필요하다고 연구 취지를 밝혔다. 회사는 앞서 오픈소스 취약점을 찾아 주는 OSS Scanner도 공개했다.
앤트로픽 프런티어 레드팀은 10월 22일 협력사 Theorem과 함께한 이 연구를 공개했다. Theorem은 RISC-V 프로세서와 Linux 프로세스의 수학 모델을 제공했다. (형식 검증)은 코드를 수학 모델로 옮긴 뒤, 코드가 정해진 규칙을 언제나 지킨다는 것을 증명하는 방법이다. 지금까지는 전문가가 몇 년을 들여야 해 항공기 소프트웨어처럼 꼭 필요한 곳에만 쓰였다. 앤트로픽은 seL4 운영체제 커널을 만드는 데 2인년, 검증하는 데 20인년이 들었다는 예를 들었다.
이번에는 OSS-Fuzz에 등록된 (퍼즈 테스트)를 명세로 바꿨고, Claude가 그 명세를 증명했다. 퍼즈 테스트는 개발자가 열어 둔 진입점(entry point)에 무작위로 만든 입력을 대량으로 넣어 프로그램이 충돌하는지 보는 시험인데, 입력을 아무리 많이 넣어도 모든 경우를 다 볼 수는 없다. Claude는 찾은 버그를 고친 뒤, 64MB보다 작은 어떤 입력에도 프로그램이 충돌하지 않는다는 것을 진입점 239곳에서 증명했다. 증명은 증명 검사 도구 Rocq로 작성됐고 분량은 약 1억 8,000만 줄이다.
찾은 버그 중에는 퍼즈 테스트로는 찾기 어려운 것이 많았다. 한 압축 해제 코드에서는 약 20MB 크기의 특정 입력에서만 메모리 범위를 벗어나 쓰는 버그가 나왔다. 앤트로픽은 퍼저가 보통 1MB 이하의 입력을 다룬다고 설명했다.
다만 증명은 RISC-V 프로세서와 Linux에서 단일 스레드로 실행되고, 메모리 한도가 정해져 있으며, musl 라이브러리를 정적으로 묶은 실행 파일을 기준으로 한다. 대부분의 사용자는 이 라이브러리를 x86·ARM 환경에서 glibc와 함께 쓰기 때문에 그 환경까지 보장하지는 않는다. 라이브러리마다 모든 진입점을 증명한 것도 아니고, 진입점을 다 증명해도 라이브러리 전체가 보장되지는 않는다고 앤트로픽은 설명했다. 앤트로픽은 형식 검증을 거쳤다고 버그가 없는 것은 아니라고 적었다.
비용도 과제로 꼽았다. 증명을 만드는 데 이 수억 개 들 수 있다. 앤트로픽이 만든 작은 검증 과제 36개에서 Claude Opus 5.5는 절반을 증명하는 데 Opus 5보다 토큰을 약 40% 덜 썼다. 앤트로픽은 증명 일부를 공개했고, Theorem은 다른 오픈소스 프로젝트에도 같은 방식을 적용해 주겠다며 개발자용 Claude 을 공개했다.
