Anthropic은 AI를 활용하여 기존 소프트웨어의 형식적 검증을 위한 기술을 개발하고 있습니다.

Anthropic은 AI 모델을 사용하여 기존 프로젝트의 신뢰성과 보안성을 형식적으로 검증하는 실험 결과를 발표했습니다. 이 실험에서 AI 모델은 OSS Fuzz 인프라에서 테스트된 123개의 오픈 소스 라이브러리에 대해 메모리 오류가 없음을 수학적으로 증명하는 데 사용되었습니다.

검증은 RISC-V 아키텍처의 컴파일된 어셈블리 코드 수준에서 수행되었습니다. 생성된 증명의 총량은 Rocq Prover 검증 시스템의 코드 약 1억 8천만 줄(18,000개의 RISC-V 명령어를 포함하는 바이너리 파일당 약 60만 줄)에 달했습니다. 증명은 기존 퍼징 테스트를 형식 명세로 자동 변환하여 생성되었으며, 이후 Claude AI 모델이 최대 64MB의 모든 입력 데이터에 대해 프로그램에 오류가 없음을 증명했습니다.

검증 과정에서 AI 모델은 퍼즈 테스트로는 발견되지 않았던 수백 개의 버그를 식별하고 수정 사항을 준비할 수 있었습니다. 여기에는 특정 입력 데이터를 처리할 때 발생하는 버퍼 오버플로 취약점(예: libexpat의 CVE-2026-56132)과 논리적 오류가 포함됩니다. 또한, AI 모델은 커널의 zlib 알고리즘 구현의 적합성을 입증하는 데 사용되었습니다. Linux RFC 1950 규격.

파이썬의 일부 기능에 대한 러스트(Rust) 인터프리터도 개발되었으며, Verus 툴킷을 사용하여 CPython 의미론과의 적합성을 입증하는 형식적 증명을 준비했습니다. CPython과의 동작 비교를 위해 1.7만 개 이상의 무작위로 생성된 파이썬 프로그램을 실행했습니다. 99.95%의 경우에서 새로운 구현과 CPython에서 실행한 결과가 일치했으며, 발견된 모든 불일치는 알려진 예외적인 경우였습니다.

형식 검증은 명세 준수를 보장하지만, 멀티스레딩 문제, 동적 링크, 실제 하드웨어에서의 비정상적인 동작으로 인한 위험이 형식화되지 않아 보안 문제를 완전히 해결하지는 못합니다. 제안된 접근 방식의 핵심 장점은 바이너리 파일에서 직접 작동하므로 기존 코드를 형식 검증 가능한 언어로 다시 작성할 필요가 없다는 것입니다.

출처 : opennet.ru