기술 요약: HarnessLLM

문제 정의

Rust의 소유권 및 타입 시스템은 강력한 메모리 안전 보장을 제공하지만, unsafe 코드의 사용과 잠재적인 런타임 패닉(예: 오버플로 또는 범위를 벗어난 접근)은 여전히 상당한 위험을 초래합니다. Kani와 같은 도구를 통한 경계 모델 검사(Bounded Model Checking, BMC)를 포함한 형식 검증(Formal Verification)은 메모리 안전성을 보장하는 데 필수적입니다. 그러나 BMC를 적용하려면 대상 API를 비결정론적 입력으로 호출하는 특수 테스트 함수인 **검증 하네스(verification harnesses)**를 수동으로 구축해야 합니다.

이러한 하네스를 만드는 것은 지루하고 수동적인 작업입니다. 기존의 자동화된 접근 방식은 세 가지 주요 한계에 직책합니다:

1. 컨텍스트 제한: 전통적인 도구들은 컨텍스트 윈도우 제약이나 복잡한 Rust 기능(제네릭, 클로저)을 처리하는 능력의 부재로 인해 대규모 코드베이스에서 완전한 호출 시나리오를 포착하는 데 어려움을 겪습니다.
2. 비결정론적 인자 생성: 복잡한 사용자 정의 타입을 위한 유효한 비결정론적(nondet) 인자를 합성하는 것은 어렵습니다. Kani의 Autoharness와 같은 기존 도구는 kani::Arbitrary 트레이트를 구현하는 타입만을 지원하여, 커스텀 타입에서는 실패합니다.
3. 환각(Hallucination) 및 조작(Fabrication): LLM을 직접 사용할 경우, LLM은 컴파일 에러를 피하기 위해 타입 정의나 함수 구현을 조작하거나, 반복적인 수정 과정에서 올바른 코드를 의도치 않게 변경하여 효율성을 떨어뜨리는 경우가 많습니다.

방법론: HarnessLLM

HarnessLLM은 기존 테스트 스위트로부터 Rust 코드를 직접 사용하여 검증 하네스를 생성하기 위해 LLM을 활용하는 자동화된 워크플로우입니다. 이 시스템은 네 가지 단계로 작동합니다:

1. 코드 분석

시스템은 Rust 코드베이스에 대해 경량 정적 분석을 수행하여 다음을 식별합니다:

• unsafe 블록 또는 잠재적 런타임 패닉( unwrap 호출 및 컴파일러 어설션(assertion)을 통해 감지됨)을 포함하는 대상 함수를 식별합니다.
• 대상과 연관된 기존 테스트 케이스를 찾습니다.
• 의존성 맵을 구축하기 위해 타입 정의, 트레이트, 공개 생성자(public constructors)를 추출합니다.

2. 호출 시나리오 추출

완전한 시나리오를 포착하는 과제(C1)를 해결하기 위해, HarnessLLM은 기존 테스트에서 특정 호출 시나리오를 추출합니다:

• 시나리오 분리 테스트 함수: 시스템은 개별 assert 문과 그에 종속된 코드 시퀀스를 격리하여 별도의 함수로 캡슐화합니다.
• 시나리오 함수: 이 시퀀스 내의 상수는 함수의 파라미터로 승격됩니다. 시스템은 LLM을 사용하여 코드를 리팩토링하며, 의미론을 유지하면서 어설션을 제거하고 상수를 파라미터로 승격시킵니다.
• 검증: 추출된 시나리오가 원래의 동작을 정확히 반영하는지 확인하기 위해, 시스템은 코드를 계측(instrumentation)하고, 원래의 상수로 시나리오를 재현하여 실행 트레이스(execution trace)를 비교합니다. 일치하는 트레이스를 가진 시나리오만 유지됩니다.

3. 하네스 합성

이 단계는 복잡한 타입에 대한 nondet 인자 구축(C2)에 집중하여 실제 검증 하네스를 생성합니다:

• 의존성 그래프 구축: 시스템은 노드가 타입 생성자를 나타내고 에지가 파라미터 타입의 생성자를 가리키는 그래프를 구축합니다.
• 단계별 사고(Chain-of-Thought, CoT) 지침: 의존성 그래프를 기반으로 CoT 지침을 생성합니다. 이 지침은 LLM이 기본 타입부터 시작하여 복잡한 사용자 정의 타입으로 이동하며 점진적으로 ndodet 데이터를 구축하도록 유도합니다.
• 외부 지식: 프롬프트에는 일반적인 Kani 사용 패턴(예: nondet 정수, 열거형, 구조체 생성)에 대한 미리 구현된 구문적으로 올바른 코드 예시가 포함되어 환각을 줄입니다.
• 합성: LLM은 생성된 시나리오 함수, 생성된 nondet 파라미터 코드, 그리고 Kani 하네스 호출을 하나의 모듈로 결합합니다.

4. 하네스 컴파일 및 반복적 개선

생성된 하네스는 Kani를 사용하여 컴파일됩니다. 오류가 발생하면 시스템은 반복적 개선 루프(C3)에 진입합니다:

• 대상 수정: LLM은 검증된 시나리오 함수와 외부 지식 코드를 명시적으로 보존하면서, 영향을 받은 섹션만 수정하도록 지시받습니다.
• 조작 탐지: 경량 AST 체커가 LLM의 출력을 검사하여 기존 타입이나 함수를 재정의했는지(환각) 탐지합니다. 환각이 감지되면 시스템은 이를 LLM에 보고하고 새로운 타입을 도입하지 않고 수정을 요청합니다.
• 이 과정은 하네스가 성공적으로 컴파일되거나 사전 정의된 반복 제한(10회)에 도달할 때까지 반복됩니다.

주요 기여

1. 최초의 Rust 기반 LLM 하네스 생성기: HarnessLLM은 실제 Rust 프로젝트의 메모리 안전성 검증을 목표로 검증 하네스 생성을 위해 LLM을 활용한 최초의 연구입니다.
2. 새로운 워크플로우 설계: 본 논문은 하네스 생성을 코드 분석, 시나리오 추출, 합성, 컴파일로 분해하고, 신뢰할 수 있는 출력을 생성하도록 유도하기 위해 의존성 그래프 기반의 CoT 지침과 같은 특정 프롬프팅 전략을 설계했습니다.
3. 환각에 대한 견고성: 오류 수정 단계에서 AST 체킹과 엄격한 보존 제약을 통합함으로써, 유형을 조작하거나 올바른 코드를 변경하는 LLM의 위험을 완화합니다.

평가 결과

저자들은 crates.io의 9개 실제 Rust 라이브러리(494개의 테스트 케이스 및 6,651줄의 코드 포함)를 대상으로 HarnessLLM을 평가했습니다.

• 시나리오 추출: HarnessLLM은 294개의 호출 시나리오를 추출했으며, 94.66%의 정밀도(원래의 실행 트레이스를 정확하게 보존하는 시나리오)를 기록했습니다.
• 하네스 생성: 시스템은 하네스당 평균 145초 내에 294개의 구문적으로 올바른 하네스를 성공적으로 생성했습니다 (100% 성공률).
• Autoharness와의 비교: 동일한 데이터셋에서 Kani의 Autoharness는 주로 kani::Arbitrary를 구현하지 않은 사용자 정의 타입에서 실패하여 **41%**의 시나리오에서만 성공했습니다. HarnessLLM은 100%의 커버리지를 달ach했습니다.
• 버그 발견: 생성된 하네스를 사용하여 저자들은 pdf-rs 라이브러리에서 6개의 실제 메모리 안전 버그를 발견했습니다(그 중 5개는 개발자에 의해 수정됨). 하나의 버그는 UTF-16 변환 함수에서의 범위를 벗어난 접근(out-of-bounds access)이었습니다.
• 절제 연구(Ablation Studies): CoT 지침을 제거하면 초기 성공률이 23.1% 감소했으며, (조작 체크가 없는) 단순한 오류 수정 프롬프트를 사용하면 생성 시도가 23.9% 증가했습니다.
• 모델 성능: GPT-4.1이 주요 모델로 사용되었으나, 다른 모델들(DeepSeek-R1, Claude-4, DeepSeek-V3)에 대한 실험에서도 모든 모델이 비용과 생성 시간은 다르지만 10회 이내에 100% 성공률을 달성할 수 있음을 보여주었습니다.

의의 및 주장

본 논문은 HarnessLLM이 Rust의 형식 검증 작업에 LLM을 사용하는 것의 실용적 유용성을 입증한다고 주장합니다. 기존 테스트에서 호출 시나리오를 자동 추출하고 복잡한 nondet 인자를 합성함으로써, 기존의 자동화된 도구들이 가진 수동 작업의 병목 현상과 한계를 극려합니다. 저자들은 이 접근 방식이 높은 자동화 수준으로 실제 코드베이스에서 메모리 안전 위반 및 런타임 패닉을 점검할 수 있도록 BMC를 가능하게 하며, Autoharness와 같은 기존의 최첨단 도구들을 크게 능가한다고 강조합니다. 저자들의 지식 범위 내에서, 이는 Rust의 메모리 안전 검증을 위해 하네스 생성을 목적으로 LLM을 적용한 첫 번째 사례입니다.