LLM으로 대규모 소프트웨어 정형 검증이 현실에 가까워지고 있습니다

AI 요약

Anthropic과 Theorem은 Claude로 오픈소스 라이브러리의 퍼즈 테스트를 기계어 수준의 정형 명세로 바꾸고, 테스트가 충돌을 일으키지 않는다는 명제를 증명했습니다. 정형 검증은 코드가 명시된 규칙을 항상 지키는지 수학적으로 확인하는 방법입니다. 연구팀은 Google OSS-Fuzz에서 123개 라이브러리의 239개 진입점을 대상으로 작업했고, 수 주 동안 RISC-V 실행 파일의 증명 약 1억 8천만 줄을 생성했습니다.

퍼즈 테스트를 증명으로 바꾸기

연구팀은 개발자가 작성한 퍼즈 테스트의 규칙, 즉 어떤 입력에서도 테스트가 충돌하지 않는다는 조건을 명세로 삼았습니다. Claude는 컴파일된 RISC-V 명령어에 대해 입력이 64MB 미만일 때 테스트가 정상 종료하는지 증명했습니다. 테스트에는 AddressSanitizer(ASan)가 포함되어 메모리 접근 오류와 assertion 실패도 충돌로 처리합니다. 이 방식은 퍼저가 무작위 입력을 시도하는 것과 달리 명시된 입력 공간 전체를 다룹니다. 다만 모든 입력이 아니라 크기 상한 아래의 입력만 대상으로 합니다.

증명은 단일 스레드 정적 바이너리, 고정 메모리 예산, RISC-V CPU, Linux 환경을 전제로 합니다. Theorem의 RISC-V 명령어와 Linux 프로세스 의미론을 사용해 바이너리를 수학적 모델로 옮겼습니다. 증명 검사는 Rocq가 맡습니다. 연구팀은 검증을 위해 신뢰해야 하는 요소로 RISC-V와 Linux의 형식 모델, 증명한 정리의 정확한 문장, Rocq 검사기를 꼽습니다. 증명 코드 자체는 자동 검사하지만, 모델과 정리가 실제 시스템 및 기대한 보안 속성을 제대로 나타내는지는 별도의 문제입니다.

증명 과정에서 발견한 결함

Claude는 증명에 실패한 사례에서 반례를 찾아 코드를 수정한 뒤, 수정된 바이너리에 맞춰 다시 증명했습니다. 발견 사례에는 약 20MB 입력의 드문 배치에서 발생하는 압축 해제 코드의 카운터 언더플로와 범위 밖 쓰기, 64MB 입력과 2GB가 넘는 메모리가 필요한 이미지 디코더의 범위 밖 읽기가 있습니다. 같은 파일을 가리키는 두 핸들에서 특정 순서로 호출해야 나타나는 오류도 찾았습니다. 중첩이 깊은 입력이 필요한 libexpat의 CVE-2026-56132도 다시 발견했습니다. 메모리 안전성 증명 중에는 특정 파일을 제한하는 기능이 항상 적용되지 않는 논리 오류도 확인했습니다.

연구팀은 다른 검증 사례도 제시합니다. Claude가 RFC 1950에 맞춰 zlib 형식 명세를 작성하고 Linux 커널의 zlib 구현이 이를 따르는지 바이너리 수준에서 증명했습니다. Python의 큰 하위 집합을 Rust 인터프리터로 구현한 뒤 Verus로 CPython 의미론을 따르는지 증명했고, 무작위 Python 프로그램 170만 개 이상을 실행해 99.95%에서 CPython과 같은 동작을 확인했습니다. PDF 뷰어 검증에서는 일주일 동안 통상 1년간 보고되는 수준의 보안 버그를 찾았다고 밝혔습니다.

범위와 비용

이 결과는 라이브러리 전체가 버그 없이 동작한다는 보증이 아닙니다. 검증하지 않은 진입점과 죽은 코드가 남을 수 있고, ASan이 모든 메모리 안전성 문제를 잡아내지도 않습니다. 실제 배포 환경의 x86·ARM, 동적 링크와 glibc도 이번 RISC-V·정적 바이너리·musl 모델과 다릅니다. 호출자가 라이브러리를 잘못 사용하는 경우도 현재 증명 범위에 들어가지 않습니다. 명세가 현실의 요구를 제대로 표현하는지도 증명 검사기만으로 판단할 수 없습니다.

증명 생성에는 수억 토큰이 들 수 있지만, 연구팀은 작은 검증 과제 36개에서 Opus 5.5가 Opus 5보다 절반의 과제를 약 40% 적은 토큰으로 증명했다고 보고했습니다. 에이전트가 서로 증명을 공유했을 때는 혼자 작업할 때보다 토큰을 17% 덜 사용했습니다. 연구팀은 공통 라이브러리의 증명 재사용과 더 많은 CPU·운영체제 모델을 향후 과제로 제시합니다.

Hacker News 반응

• @jaykru — 에이전트가 쓴 증명도 같은 정리를 증명한다는 점에서는 다른 증명만큼 유효합니다. 하지만 장황한 증명 방식으로 더 복잡한 프로그램까지 확장할 수 있을지는 아직 알 수 없습니다. MachCSL 같은 에이전트 검증 프로젝트에서는 복잡도 한계에 부딪혔고, 확장하려면 더 나은 모듈 추상화와 추론 원리가 필요했습니다. 에이전트가 그런 추상화를 찾아내게 하려면 전문가의 개입이 필요한지, 공통 원리를 뽑아낼 수 있는지가 궁금합니다.
  • @nextaccountic — 증명 작성은 특수한 언어로 코드를 쓰는 일입니다. 모듈화된 증명과 추상화는 모듈화된 코드와 추상화를 쓰는 일입니다. 에이전트는 전반적으로 더 나은 프로그래밍을 배워야 합니다. 증명 학습이 Haskell이나 Rust 코드를 더 잘 쓰는 능력으로 이어질 수도 있습니다.
  • @jasongross — 수학에서는 볼록 껍질 가설이 인간 능력을 넘기 어려운 이유가 분포 밖 일반화에 있습니다. 소프트웨어 검증은 병목이 규모에 있으므로, 그 가설이 맞더라도 존재하는 거의 모든 소프트웨어를 검증할 수 있습니다.
• @mjorgers — 명제를 증명하려면 명제가 코드의 현실을 제대로 모델링해야 하는 것 아닌가요? 정형 검증에서 대상 소프트웨어를 올바르게 모델링했는지 어떻게 확신하나요? 실제 프로그램이 아닌 것을 증명했을 수도 있지 않나요?
  • @gizmo686 — 프로그래밍 언어 모델이 있으면 소스 코드 자체를 증명할 수 있지만, 그때는 컴파일러 모델을 신뢰해야 합니다. 명령어 집합과 아키텍처를 모델링해 최종 바이너리를 증명하면 컴파일러 버그 문제는 피할 수 있고, 물리 하드웨어가 모델과 일치한다는 가정이 남습니다.
• @pinevale — 모든 의도된 입력과 의도되지 않은 입력, 이해관계자와 사용자 행동을 포함하는 완전한 명세를 무엇과 대조해 검증하나요? 결국 일반 퍼저로 충돌을 찾아 수정한 뒤, 수정됐다는 증명을 쓴 것처럼 보이는데 별 의미가 있나요?
  • @gr_norm — 글은 인코딩과 디코딩의 왕복 일치, 멱등성, 대수 법칙, 참조 구현과의 일치처럼 의미 있는 속성을 검사하는 퍼즈 테스트도 있다고 설명합니다. 다만 프로그램의 의도를 온전히 담은 명세에 대한 정확성 증명과는 다릅니다.
  • @btilly — 일반 퍼저가 충돌을 일으킬 수 있는 입력 공간에서 무작위 표본을 뽑는다면, 여기서는 그 공간의 어떤 입력도 충돌을 내지 않는다고 증명했습니다. 퍼저가 제공하는 결과보다 강합니다.
• @woggy — LLM이 형식 명세가 실제 원하는 동작을 담도록 돕더라도, LLM이 증명한 내용이 정말 원하는 것인지 어떻게 확인하나요?
• @j16sdiz — OpenAI의 Lean 수학 증명 사례에서는 검증을 통과하는 Lean 코드와 그 코드에 맞지 않는 수학 논문이 나왔습니다. 프로그램을 Rocq 증명으로 옮길 때도 같은 문제가 생길 수 있습니다. 버그를 찾는 데는 도움이 되겠지만, 이것만으로 충분한 증명이라고 보기는 어렵습니다.
• @malisper — Rust로 PostgreSQL을 다시 구현하면서 Rust와 C 코드를 Lean으로 옮기는 컴파일러를 만들고, 두 함수가 같은 동작을 하는지 LLM으로 증명했습니다. 현재 단일 스레드 실행에서 코드의 약 12%, C 코드 약 7만 줄의 동작이 같다는 점을 증명했습니다. 플랫폼별 부동소수점 연산 차이 같은 작은 동작 차이도 찾았고, 확장을 막는 근본적 한계는 보이지 않는다고 했습니다.
• @sestep — 직장에서 에이전트가 SIMD나 CUDA로 함수를 빠르게 바꾸는 실험을 PR로 올리고, Rocq 증명으로 기존 구현과 동등함을 보이면 자신 있게 병합하는 방식으로 사용하고 있습니다.
  • @mattr03 — 정리가 실제 코드에 적용된다는 점은 어떻게 확신하나요?

원문: Anthropic / 번역·요약: Trawling