Claude가 RISC-V 어셈블리 수준에서 123개 라이브러리 보안을 증명했다

앤트로픽이 협력사인 시어럼(Theorem)과 함께 Claude로 실제 프로덕션 소프트웨어의 보안 속성을 형식 검증(formal verification)한 결과를 공개했다. 검증 대상은 123개의 오픈소스 라이브러리이며, 증명은 소스 코드가 아니라 컴파일된 RISC-V 어셈블리 수준에서 이뤄졌다. 앤트로픽은 이 규모의 어셈블리 레벨 형식 검증을 AI로 수행한 사례가 처음이라고 설명한다.

증명된 명제는 꽤 구체적이다. 대상 프로그램이 단일 스레드 정적 바이너리로 고정된 메모리 예산 안에서 RISC-V CPU와 리눅스 위에서 실행된다는 전제 아래, 64MB 미만의 모든 입력과 모델링된 모든 운영체제 응답·메모리 배치에 대해 프로그램이 메모리 안전성 오류나 단언(assertion) 실패 없이 정상 종료한다는 것이다. 즉 무한히 많은 입력을 전수 조사하지 않고도 특정 조건에서는 크래시가 발생하지 않는다는 보장을 얻은 셈이다.

출발점은 퍼징(fuzzing)이었다. 개발자가 진입점을 만들어 두면 퍼저가 준무작위 입력을 쏟아부어 크래시를 찾는 방식인데, 입력 공간이 무한하므로 아무리 오래 돌려도 모든 경로를 훑었다는 보장이 없다. 연구진은 이 퍼즈 테스트를 '이 테스트 스위트는 항상 통과한다'는 명세로 자동 변환하고, 그 명세를 RISC-V 명령어 위에서 증명하는 쪽을 택했다. 증명에 성공하면 해당 진입점에 대한 퍼징은 사실상 불필요해진다. 대상은 구글의 OSS-Fuzz 이니셔티브에 참여하는 수백 개 프로젝트의 진입점들이었다.

배경에는 형식 검증의 오랜 비용 문제가 있다. seL4 운영체제 커널은 구현에 2인년이 들었지만 형식 검증에는 20인년이 투입됐다. 증명 코드가 원본 코드보다 몇 배 길어지기 일쑤이고, 다루는 기술도 극도로 좁은 전문 영역이다. 그래서 형식 검증은 에어버스 항공전자 코드처럼 실패가 곧 재앙인 곳에서만 쓰여 왔다. 반면 요즘 소프트웨어의 현실은 반대다. 전 세계 수십억 기기에 깔린 리눅스 커널에서도 최근 1,000건이 넘는 취약점이 공개됐고, 최신 모델은 사소해 보이는 버그를 연쇄해 치명적 익스플로잇으로 엮어내는 데 능해지고 있다.

주목할 부수 효과도 있다. 증명을 작성하는 과정에서 Claude가 수년간, 그것도 조 단위의 테스트 실행으로도 잡히지 않았던 버그를 찾아냈다. 증명 시도가 실패하는 지점이 곧 버그의 위치를 알려주는 단서로 작동하기 때문이다. 형식 검증이 '보장 도구'이자 '버그 탐지 도구'로 동시에 기능한다는 점을 보여주는 대목이다.

앤트로픽은 증명 결과의 일부를 공개해 누구나 검증하고 재사용할 수 있게 했고, RISC-V와 운영체제 시맨틱스도 함께 내놨다. 시어럼은 다른 오픈소스 프로젝트에도 같은 파이프라인을 돌려주겠다고 제안했으며, 개발자가 자기 코드 검증을 시작할 수 있도록 Claude 스킬도 배포한다.

형식 검증만 실험한 것은 아니다. zlib 압축 알고리즘의 보안성 평가, 러스트로 작성된 파이썬 인터프리터의 동작 동등성 증명, 오래된 크리티컬 소프트웨어의 잠복 버그 색출 같은 다른 방법론 탐색도 함께 진행됐다.

개발자 입장에서 달라지는 것은 검증의 진입 장벽이다. 모델이 똑똑해질수록 증명 작성 비용은 내려가고, 코드가 더 많이 형식화될수록 증명을 다른 코드베이스에 재사용하거나 변형하기 쉬워져 비용이 분산된다. 보안이 중요한 모듈을 다루면서 형식 검증을 '우리 규모에서는 무리'라고 접어뒀던 팀이라면, 더 성능이 낮은 모델로 시도했다가 실패한 경우를 포함해 다시 평가해 볼 시점이라는 것이 앤트로픽의 권고다.

한계는 분명하다. 이번 증명은 단일 스레드 정적 바이너리, 고정 메모리 예산, 특정 CPU와 OS라는 전제 위에 서 있다. 모든 종류의 버그를 없앤다는 목표와는 여전히 거리가 있고, 명세 자체를 어떻게 정의할 것인가라는 근본 문제도 남는다. 텍스트 편집기나 웹 브라우저가 '올바르다'는 것이 무엇인지 명확히 규정하기 어렵듯, 검증의 출발점인 명세 작성은 여전히 사람의 몫이다.