AI
LLM으로 대규모 정형 소프트웨어 검증의 실용화
LLMs are making formal software verification feasible at a much larger scale
두줄요약
Claude가 123개 OSS-Fuzz 라이브러리의 RISC-V 바이너리 보안 속성을 정형 증명했습니다. 기존 퍼즈 테스트를 모든 입력에 대한 no-crash 명세로 확장했습니다.
핵심 발표
- Claude를 활용한 123개 오픈소스 라이브러리, 239개 OSS-Fuzz 엔트리 포인트의 RISC-V 실행 바이너리 보안 속성 정형 증명
- 프로덕션 소프트웨어의 어셈블리 코드 수준 정형 검증에 AI를 대규모 적용한 첫 시도라는 설명
연구 방법·결과
- 기존 컴파일 가능 퍼즈 테스트를 ‘64MB 미만 모든 입력에서 테스트가 항상 통과’하는 명세로 변환
- AddressSanitizer로 탐지되는 메모리 안전성 오류와 실패한 assertion 없이 정상 종료하는 no-crash 속성 증명
- Claude의 버그 발견·패치 후 Rocq 커널 검증, 약 1억 8천만 줄의 Rocq 증명 생성
개발자 영향
- 수조 회의 테스트 실행에서도 발견되지 않았던 버그 탐지
- 퍼즈 테스트의 입력 탐색 한계를 모든 입력에 대한 정형 증명으로 보완
사용 방법·가용성
- 증명 일부와 RISC-V·OS 시맨틱스 공개
- Theorem의 다른 오픈소스 프로젝트 대상 동일 파이프라인 제공 및 Claude skill 공개
한계·주의점
- 단일 스레드 정적 바이너리, 고정 메모리 예산, RISC-V CPU, Linux OS 가정
- 증명 범위는 특정 보안 규칙 위반 버그이며 모든 가능한 버그 해결과는 거리 존재