Anthropic: Claude, 오픈소스 라이브러리에 대한 대규모 형식적 검증 완료

10월 22일, 인공지능 기업 Anthropic 산하 프론티어 레드 팀(Frontier Red Team)은 대규모 언어 모델이 현재 형식적 증명을 보다 광범위하게 자동 생성할 수 있는 능력을 갖추게 되었다는 연구 결과를 발표했다. 이 팀은 Theorem과 협력하여 Claude 모델을 기반으로 RISC-V 어셈블리 레벨에서 100개 이상의 실제 오픈소스 라이브러리에 대해 보안 속성의 형식적 검증을 수행했는데, 이는 지금까지 AI 시스템이 어셈블리 레벨에서 프로덕션급 소프트웨어를 대상으로 실시한 최초의 대규모 형식적 검증이다. 증명 구축 과정에서 팀은 예기치 않게 오랫동안 발견되지 않았던 여러 개의 보안 취약점을 밝혀냈다. 실험 방법은 Google OSS-Fuzz에 이미 존재하는 컴파일 가능한 퍼징 테스트 케이스를 형식적 사양으로 변환한 후, 단일 스레드 정적 바이너리, 고정 메모리 예산, RISC-V CPU 아키텍처 및 Linux 실행 환경 등 제약 조건 하에서 크기가 최대 64MB인 임의의 입력에 대해 검증을 수행하는 방식이다.