기술 요약: 에이전트 모델 체킹

문제 정의

대형 언어 모델 (LLM) 이 생성한 시스템 코드 검증은 기존 형식 검증의 어려움에 고유한 난제를 더해 복잡성을 증폭시킵니다. LLM 은 C 및 Rust 와 같은 언어로 운영체제, 컴파일러, 드라이버에 대한 방대한 코드 집합을 생성할 수 있지만, 결과물인 코드베이스는 종종 명시적인 형식 명세를 결여하고 있습니다. furthermore, LLM 생성 코드 내의 안전 계약은 함수 경계에서 강제되기보다 호출 지점 (call sites) 에서 암시적으로 인코딩되는 경우가 많습니다.

이러한 암시적 인코딩은 특정 실패 모드로 이어집니다. 예를 들어, 바이트 인덱싱 리더나 오프셋 산술 작성기와 같은 헬퍼 함수는 종종 경계 및 오버플로우 가드 (guard) 가 부재하며, 불변 조건을 유지하기 위해 주변 호출자 로직에 의존합니다. 결과적으로 코드는 잘 형성된 입력에서는 정상적으로 작동하지만, 적대적이거나 조작된 입력에서는 실패합니다. 전통적인 검증 도구는 여기서 어려움을 겪는데, 이는 문맥 없이 헬퍼 함수를 결함 있는 것으로 과도하게 보고하거나 (over-report), 현재 호출자가 이를 트리거하지 않아 버그를 놓치는 (under-report) 경향이 있기 때문입니다. 또한, 기존 LLM 기반 검증 접근법은 산술 및 메모리 안전성에 대한 건전성 (soundness) 이 부족한 경우가 많고, 전통적인 연역적 체커는 시스템 코드의 규모와 루프가 많은 특성에 대처하기 어렵고 구체적인 반례를 생성하는 능력이 부족합니다.

방법론: 에이전트 모델 체킹

저자들은 **"에이전트가 제안하고, 솔버가 검증한다"**는 원칙 하에 LLM 에이전트와 경계 모델 체킹 (BMC) 백엔드를 결합한 검증 패러다임인 **에이전트 모델 체킹 (Agentic Model Checking)**을 제안합니다.

BMC-Agent로 구체화된 이 시스템은 LLM 에이전트가 의미적 판단이 필요한 작업을 처리하고, 결정론적 BMC 백엔드 (C 의 경우 CBMC, Rust 의 경우 Kani) 가 건전성과 관련된 모든 결정을 처리하는 파이프라인을 통해 운영됩니다.

핵심 아키텍처 약속

1. 상향식 명세 추론 (Top-Down Specification Inference):

   • 에이전트는 호출자 문맥에서 상향식으로 함수별 전제조건과 사후조건을 추론합니다.
   • 명제는 백엔드의 네이티브 assume/assert 원시 명령어로 결정론적으로 변환되는 제한된 도메인 특정 언어 (DSL) 로 생성됩니다.
   • 시스템은 방어적 패닉 방지 검사 외에도 기능적 정확성 명세(예: 참조 동등성 표현, 대수적 항등식) 를 생성하여, 검증을 단순한 충돌 회피에서 행동의 충실성으로 확장합니다.

2. 구성적 검증 (Compositional Verification):

   • 검증은 함수 단위로 분해됩니다. 각 함수는 추론된 명세에 대해 격리된 상태에서 검사됩니다.
   • 호출된 함수 (callee) 는 그 사후조건으로 제약된 스텁 (stub) 으로 대체됩니다. 이는 callee 의 사후조건이 호출자의 가정 (assumption) 이 되는 가정 - 보증 (assume-guarantee) 규율을 구현합니다.
   • 이 접근법은 전체 프로그램 상태 폭발을 방지하여, 전체 프로그램이 아닌 단일 함수의 상태 공간 크기에 따라 검증이 확장되도록 합니다.

3. 다단계 반례 검증 (Multi-Stage Counterexample Validation):

   • BMC 반례는 즉각적인 버그 보고서로 취급되지 않습니다. 활성 트리 내 충돌과 잠재적 실패 또는 모델링 산물을 구별하기 위해 엄격한 검증 파이프라인을 통과합니다.
     • 입력 도달성: 호출자 그래프를 따라 증거 입력을 전파하여 호출자가 해당 값을 제공할 수 있는지 판단합니다.
     • Callee 실현 가능성: 실제 callee 본체를 사용하여 BMC 를 다시 실행하여 증거가 실제 구현을 통해 도달 가능한지 확인합니다.
     • 동적 재생: 호스트 시스템에서 증거를 실행하기 위해 하네스 (harness) 를 컴파일하고 신호 (SIGSEGV, SIGABRT 등) 를 포착하여 동적 충돌을 확인합니다.
     • 현실성 감사: LLM 에이전트가 전체 문맥 (명세, 하네스, 증거 상태) 을 검토하여 발견 사항을 현실적이거나 비현실적으로 분류하고, 프레임워크 불변 산물 (예: 초기화되지 않은 전역 변수, 불가능한 하드웨어 상태) 을 필터링합니다.

4. 적응형 정제 루프 (명세 수준의 CEGAR):

   • 반례가 허위 (예: 루프 언와인딩 산물) 로 분류될 때, 시스템은 단순히 이를 억제하지 않습니다. 대신 LLM 이 전제조건을 강화하거나, callee 계약을 강화하거나, 솔버 매개변수를 조정하는 정제를 제안합니다.
   • 건전성 가드는 이러한 정제가 실제 버그를 가리지 않도록 보장합니다.
   • 승인된 정제는 지식베이스 (명세 저장소 및 패턴 라이브러리) 에 영구 저장되고 모든 호출자에게 전파되어, CEGAR 을 술어 추상화에서 구성적 전파를 갖춘 명세 수준으로 확장합니다.

주요 기여

논문은 다음과 같은 여섯 가지 주요 기여를 제시합니다:

1. 에이전트 모델 체킹 패러다임: LLM 에이전트가 명세 추론, 검사 선택, 분류와 같은 의미적 작업을 관리하고 BMC 백엔드가 건전성을 보장하여, 명세 없는 LLM 생성 C 및 Rust 코드 검증을 가능하게 하는 프레임워크.
2. 상향식 명세 계층: DSL 을 통해 CBMC/Kani 로 변환되는 함수별 전/사후조건을 추론하고 산술 오버플로우, 포인터 검사 등 의미적으로 정당화된 산술 검사를 선택하는 메커니즘.
3. 구성적 검증 아키텍처: 가정 - 보증 계약 하에서 격리된 함수 검사를 통해 확장 가능한 접근 방식으로, 호출 그래프 계층을 가로질러 병렬화합니다.
4. 검증 파이프라인: 도달성, 실현 가능성, 동적 재생, 현실성 감사의 4 단계 프로세스로 발견 사항을 "확인된 동적", "확인된 시스템 진입"과 같은 증거 등급으로 분류합니다.
5. 다단계 정제 루프: 허위 반례를 활용하여 구성적 정제를 유도하고 실행 간에 지속되도록 하여 명세 수준으로 CEGAR 을 확장하는 시스템.
6. BMC-Agent 구현 및 평가: 다양한 코퍼스에서 평가된 작동 도구로, 실제 결함을 확인하고, 퍼즈된 라이브러리에 대해 경계된 깨끗한 검증을 생성하며, 기능적 동등성을 증명하는 능력을 입증합니다.

평가 결과

저자들은 C 와 Rust 로 구성된 네 가지 코퍼스에 대해 BMC-Agent 를 평가했습니다:

• VibeOS (C): 15,000 줄 규모의 LLM 생성 ARM64 커널. BMC-Agent 는 12 개 모듈에 걸쳐 34 개의 현실적인 버그를 확인했습니다. 이 중 16 개는 동적으로 재현 (SIGSEGV/SIGABRT) 되었고, 14 개는 시스템 진입점으로 확인되었으며, 4 개는 형식 모델 위반이었습니다.
• 성숙한 오픈소스 라이브러리 (C): jq, OpenSSL, libcurl, libxml2, protobuf upb를 평가했습니다. 도구는 jq에서 2 개의 정의되지 않은 동작 (undefined-behavior) 결함을 공개 (GHSA 에 신고) 했으며, 심하게 퍼즈된 파서 표면에서 경계된 깨끗한 검증을 산출했습니다 (예: OpenSSL ASN.1 의 24 개 리프 함수 중 15 개가 깨끗하게 검증됨).
• Realtek r8125 드라이버 (C): rtl8125 도구 ioctl 에서 CAP_NET_ADMIN 게이트가 걸린 MMIO 경계 검사 우회를 발견했으며, 이는 플래그 선택기를 통해 특정 오버플로우 검사를 활성화함으로써 트리거되었습니다.
• claudes-c-compiler (Rust): 50,000 줄 규모의 LLM 생성 C 컴파일러. BMC-Agent 는 25 개의 실제 버그를 확인했는데, 주로 공개 API 바이트 헬퍼 (슬라이스 OOB, 정수 오버플로우) 에서의 패닉 클래스 결함과 하나의 기능적 정확성 위반이었습니다. 또한 ELF 해시 및 헤더 작성 헬퍼에 대해 경계된 기능적 동등성을 확립했습니다.

결과에서 도출된 주요 관찰 사항:

• 도구의 정밀도는 프레임워크 산물을 필터링하는 현실성 단계 감지기, 표준 구성에서 기본적으로 꺼져 있는 검사를 활성화하는 함수별 플래그 선택, 그리고 반복되는 패턴을 영구 불변 조건으로 변환하는 피드백 루프에 기인합니다.
• Rust 컴파일러 사례에서 버그는 특정 반패턴을 따랐습니다: LLM 이 경계 검사 없이 헬퍼 함수를 작성하고 호출자가 불변 조건을 유지하도록 의존했습니다. 이는 잘 형성된 입력에서는 작동하지만 적대적 입력에서는 실패하는 코드로 이어졌으며, 이는 일반적인 인간 작성 컴파일러 논리 오류와 구별되는 프로파일입니다.

중요성과 주장

이 논문은 에이전트 모델 체킹이 계약 추론을 자동화하고 이를 건전하고 경계된 모델 체킹과 결합함으로써 LLM 생성 시스템 코드의 "명세 격차"를 해결한다고 주장합니다.

• 건전성 vs 확장성: 건전성을 BMC 에 위임하고 에이전트를 의미적 판단에 활용함으로써, 순수 LLM 추론의 비건전성을 피하면서도 전체 프로그램 검증의 확장성 한계를 극복합니다.
• 실행 가능한 검증: 다단계 검증 파이프라인은 보고된 버그가 단순한 이론적 반례가 아니라 도달성과 동적 영향에 따라 분류되도록 보장하여, 활성 충돌과 잠재적 강화 작업 사이를 구분합니다.
• 구성적 전파: 시스템을 통해 명세를 정제하고 이를 호출 그래프 전반에 전파할 수 있는 능력은 허위 반례로부터 학습하여 수동 개입 없이 시간이 지남에 따라 검증 품질을 향상시킵니다.

저자들은 향후 작업에 대해 겸손하게 언급하며, 광범위한 정량적 평가 (규모에 따른 정밀도/재현율), 명세 정확성 가정의 심층 분석, 토큰 최적화를 통한 비용 절감이 필요한 다음 단계라고 강조합니다. 그들은 현재 결과가 결함 확인 및 깨끗한 표면 검증을 위한 파이프라인의 능력을 입증하지만, 제한 없이 모든 LLM 생성 코드 검증이라는 일반적 문제를 해결했다고 주장하지는 않는다고 강조합니다.