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

앤스로픽이 10월 22일 클로드로 오픈소스 라이브러리 123개의 보안 성질을 수학적으로 증명했다는 연구를 발표했다. 프런티어 레드팀 블로그에 실린 글에 따르면 클로드는 형식 검증 스타트업 테오렘(Theorem)과 함께 몇 주 만에 구글 OSS-Fuzz에 등록된 라이브러리 123개, 진입점 239개가 64MB 미만의 어떤 입력을 받아도 충돌하지 않는다는 증명을 완성했다. 증명 대상은 소스 코드가 아니라 RISC-V 명령어로 컴파일된 실행 파일이고, 검증을 통과한 증명은 증명 언어 Rocq로 약 1억 8,000만 줄이다. 연구진은 글에서 "우리가 아는 한 AI로 실제 운영 소프트웨어에 어셈블리 수준의 형식 검증을 적용한 첫 대규모 시도"라고 밝혔다.

형식 검증은 코드를 수학 모델로 옮긴 뒤, 정해 둔 규칙을 어떤 경우에도 어기지 않는다는 것을 증명하는 기법이다. 그동안 걸림돌은 비용이었다. 앤스로픽은 운영체제 커널 seL4를 만드는 데 2인년이 들었지만 형식 검증에는 20인년이 들었다는 사례를 들며, 이 기법이 에어버스 항공 전자 코드처럼 실패가 용납되지 않는 분야에서만 쓰여 왔다고 설명했다. 회사는 수십억 대 기기에 깔린 리눅스 커널에서도 최근 취약점 1,000건 넘게 공개됐다는 점을 짚었다. 언어 모델이 버그를 찾아 공격으로 엮는 능력이 커질수록 방어하는 쪽에는 남은 버그가 없다는 증거가 필요하다는 논리다.

연구진이 고른 출발점은 퍼즈 테스트다. 퍼저는 반쯤 무작위로 변형한 입력을 진입점에 쏟아부어 충돌을 찾는 도구인데, 오래 돌릴수록 버그를 더 찾지만 모든 실행 경로를 지났다는 보장은 끝내 주지 못한다. 앤스로픽은 개발자가 이미 써 둔 퍼즈 테스트를 '64MB 미만의 어떤 입력에도 이 테스트는 충돌하지 않는다'는 명세로 바꿨다. 테오렘이 만든 RISC-V 명령어와 리눅스 프로세스의 형식 의미론이 실행 파일을 수학 모델로 옮기고, 클로드가 증명을 쓰고, Rocq 커널이 그 증명이 명세를 만족하는지 검사한다. 증명이 통과한 진입점은 더 퍼징해도 찾을 버그가 없다는 뜻이다.

분량은 사람이 읽을 수 있는 수준을 한참 넘는다. 전형적인 증명 하나가 약 60만 줄이고, 대상 바이너리의 명령어 수 중앙값은 1만 8,000개다. 부록에 따르면 클로드가 이 프로젝트에서 쓴 Rocq 증명은 약 10억 줄이고, 그 가운데 1억 8,000만 줄이 검사를 통과한 증명에 들어갔다. cJSON의 391줄짜리 파서 진입점에는 63만 줄짜리 증명이 붙었고, 증명 하나를 검사하는 데 CPU 시간으로 30분에서 몇 시간이 걸린다. 그래도 사람이 증명을 한 줄씩 볼 필요는 없다는 것이 회사 설명이다. 개발자가 믿어야 할 것은 RISC-V와 리눅스 프로세스의 형식 모델, 증명한 정리 문장, Rocq 검사기 세 가지로 좁혀진다.

증명을 시도하는 과정 자체가 버그 탐지기 노릇을 했다. 증명이 막히는 자리마다 실제 결함이 있었고, 연구진은 클로드가 그 자리에서 코드를 고친 뒤 고친 코드로 다시 증명하게 했다. 이렇게 드러난 버그가 수백 건이다. 퍼저는 보통 1MB 이하 입력을 변형하는데, 한 라이브러리의 압축 해제기에서는 약 20MB짜리 특정 배치 입력에서만 카운터가 음수로 넘어가 범위 밖 쓰기가 일어났다. 한 이미지 디코더의 범위 밖 읽기는 64MB 입력과 2GB 넘는 메모리가 있어야 드러났고, XML 파서 libexpat에서는 알려진 취약점 CVE-2026-56132를 다시 찾아냈다. 충돌 없이 숨어 있던 논리 버그도 나왔다. 앱이 불러올 파일을 제한하는 기능이 항상 적용되지는 않는다는 결함이다. 클로드가 프로그램을 아무것도 하지 않는 코드로 바꿔 증명을 통과시키는 보상 해킹을 막으려고, 연구진은 패치에 감점을 주고 바뀐 입력이 얼마나 적은지 증명하면 가점을 줬으며 모든 패치를 기록해 감사했다.

퍼즈 테스트 밖의 실험도 공개했다. 클로드는 zlib 압축 형식을 정의한 RFC 1950의 형식 명세를 직접 쓰고, 리눅스 커널의 zlib 구현이 그 명세를 따른다는 것을 x86 바이너리 수준에서 증명했다. 이때 쓴 x86 명령어 의미론도 클로드가 만든 것이다. 러스트로 짠 파이썬 인터프리터를 검증 도구 Verus로 증명한 실험에서는 무작위로 만든 파이썬 프로그램 170만 개 이상을 돌려 CPython과 99.95% 같은 동작을 확인했다. 연구진이 일부러 심은 버그 7개 가운데 무작위 테스트는 5개를 놓쳤고 증명은 7개를 모두 잡았다. 널리 쓰이는 PDF 리더를 검증하려던 작업에서는 1주일 만에 보통 1년 동안 보고되는 만큼의 보안 버그가 나왔고, 다른 핵심 애플리케이션에서는 10년 넘게 숨어 있던 논리 버그가 드러났다.

비용 곡선은 빠르게 내려오고 있다. 증명 하나에 토큰 수억 개가 드는 것이 지금의 부담인데, 앤스로픽이 실제 OSS-Fuzz 코드로 만든 소형 검증 과제 36개에서 Opus 5.5는 절반을 Opus 5보다 약 40% 적은 토큰으로 풀었다. 에이전트들이 서로의 증명을 베껴 쓸 수 있게 공유 작업 공간을 열자 토큰 사용량은 17% 줄었다. 테오렘이 따로 잰 수치는 더 가파르다. 테오렘에 따르면 5월부터 9월 사이 앤스로픽과 오픈AI 모델 7종의 검증 속도는 약 두 달마다 두 배가 됐고, 시간당 검증한 기계어는 Opus 4.8의 약 0.12KB에서 9월 모델들의 0.6~0.9KB로 올랐다.

테오렘은 이 추세를 리눅스 배포판 패키지 모음 nixpkgs 전체에 대입했다. 라지슈리 아그라왈, 제이슨 그로스 등 테오렘 연구진 6명이 쓴 글은 "AI 시스템은 이제 형식 검증에 충분히 유능해져, 모든 소프트웨어가 검증되는 미래를 진지하게 그려 볼 수 있다"고 적었다. 이들의 추산으로는 nixpkgs의 기계어 약 150GB 가운데 3분의 2가 9MB 남짓한 공유 라이브러리에 의존하고, 암호 라이브러리 OpenSSL 하나가 패키지 1만 6,000개가량의 실행 의존성에 들어 있다. 연 1억 달러를 쓰면 2027년 말까지 기계어의 95%를 검증할 수 있고 총비용은 약 1억 3,400만 달러라는 계산이다. 한 번 증명한 라이브러리를 그 위에서 도는 패키지가 재사용한다는 전제가 이 숫자를 만든다.

메탈이 확인한 6쪽 분량 부록 PDF에는 형식 검증 전문가가 클로드의 증명을 읽은 평가가 실려 있다. 에이전트들은 요구받은 것보다 짧고 의미 있는 명세를 스스로 세웠는데, 새니타이저 증명의 명세 길이 중앙값은 약 110줄로 대상 프로그램 코드 중앙값 86KB에 비해 훨씬 짧았다. 반면 증명 본문은 장황했다. CPU 레지스터 내용, 정수 변환, 주소끼리 겹치지 않는다는 사실을 매번 풀어 적었고, 평가자는 사람 증명 엔지니어라면 호출 규약이나 메모리 할당기 같은 추상화를 곧바로 도입했을 것이라고 썼다. 이 장황한 방식이 더 복잡한 프로그램까지 그대로 커질 수 있는지는 아직 답이 없는 질문으로 남았다.

증명이 보장하는 범위도 글에 구체적으로 적혀 있다. 대상은 musl libc에 정적으로 연결된 단일 스레드 RISC-V 바이너리인데, 실제 사용자 대부분은 같은 라이브러리를 x86이나 ARM에서 glibc에 동적으로 연결해 돌린다. 충돌 감지에 쓴 AddressSanitizer가 모든 메모리 오류를 잡지는 못하고, 라이브러리마다 모든 진입점을 검증한 것도 아니다. 앤스로픽은 "'형식 검증됨'은 '버그 없음'을 뜻하지 않는다"고 적고, 남은 버그가 있다면 명세와 기계 모델이 현실과 어긋난 자리에 있으니 어디를 봐야 할지는 안다고 덧붙였다.

결과물은 밖으로 열었다. 앤스로픽은 패치가 필요 없었던 퍼즈 테스트의 Rocq 증명 전체와 RISC-V·리눅스 의미론을 깃허브에 공개했고, 아직 고쳐지지 않은 버그를 드러낼 수 있는 증명은 공개하지 않았다. 테오렘은 OSS-Fuzz와 같은 방식으로 저장소에 풀 리퀘스트를 열어 등록하는 무료 프로그램 OSS Verify를 시작했고, 개발자용 클로드 스킬도 내놨다. 증명 중에 찾은 버그는 메인테이너에게 비공개 이메일로만 알리고 공개 기한을 두지 않는다고 테오렘은 밝혔다.

메탈은 8월 클로드 시큐리티가 Mythos 5로 코드 스캔을 시작했다고 보도한 바 있으며, 이번 연구는 같은 회사의 방향이 버그를 찾는 일에서 버그가 없음을 증명하는 일로 넘어가고 있음을 보여 준다. 엔지니어링 조직의 관점에서 계산은 단순해진다. 퍼징은 돌린 시간만큼 확률을 사는 지출이지만, 증명은 한 번 통과하면 그 진입점에서 다시 돈을 쓸 이유를 지운다. 의존성은 소수의 공유 라이브러리에 몰려 있고 그 증명은 위층 패키지가 그대로 물려받는다. 증명 비용이 두 달마다 절반씩 줄어드는 동안, 핵심 라이브러리를 누가 먼저 증명된 상태로 만드느냐가 소프트웨어 공급망 보안의 다음 경쟁이 된다.