Verification Modulo Tested Library Contracts

이 논문은 **"테스트된 라이브러리 계약 (Tested Library Contracts) 을 통한 검증 (Verification Modulo Tested Library Contracts, VMTLC)"**이라는 새로운 문제를 제시하고, 이를 해결하기 위한 자동화 프레임워크를 제안합니다. 대규모 라이브러리를 사용하는 클라이언트 프로그램의 형식적 검증을 자동화하는 데 있어 발생하는 난제를 우회하기 위해, 라이브러리의 완전한 형식적 검증 대신 광범위한 테스트를 기반으로 한 계약을 합성하는 접근법을 취합니다.

다음은 논문의 주요 내용을 기술적으로 요약한 것입니다.

---

1. 문제 정의 (Problem Statement)

대규모 소프트웨어 시스템에서 클라이언트 프로그램의 형식적 검증을 자동화하는 것은 여전히 어렵습니다. 기존 접근법은 라이브러리에 강력한 계약 (Contracts) 을 수동으로 주석하거나 자동 합성해야 하며, 이를 통해 클라이언트와 라이브러리 모두를 검증해야 합니다. 그러나 복잡한 라이브러리에 대한 완전한 자동 검증은 현실적으로 불가능에 가깝습니다.

저자들은 다음과 같은 VMTLC 문제를 정의합니다:

• 입력: 라이브러리 $L$을 사용하는 클라이언트 프로그램 $C$.
• 목표: 라이브러리 메서드에 대한 형식적 계약 $\Pi$를 합성하여 다음 두 조건을 만족하는 것:
  1. 클라이언트 검증: 계약 $\Pi$를 가정할 때, 클라이언트 $C$가 정확함 (Assertions) 을 논리 엔진을 통해 증명.
  2. 라이브러리 테스트: 주어진 테스트 생성기 (Test Generator) 가 제한된 자원으로 라이브러리 메서드를 테스트했을 때, 합성된 계약 $\Pi$를 위반하는 테스트 케이스를 찾지 못함.

즉, 라이브러리 자체를 형식적으로 증명하는 대신, 합성된 계약이 테스트를 통과하는지 확인함으로써 클라이언트의 검증을 수행합니다.

2. 핵심 방법론 (Methodology)

이 논문은 반대 예제 유도 학습 (Counterexample-Guided Learning) 프레임워크를 기반으로 한 자동화 솔루션을 제안합니다.

2.1. 컨텍스트 계약 (Contextual Contracts)

기존의 모듈러 계약 (Modular Contracts) 은 모든 가능한 상태와 입력에서 라이브러리 메서드가 계약에 부합해야 하지만, 컨텍스트 계약은 클라이언트 프로그램이 실제로 호출하는 특정 상태와 입력 범위 내에서만 유효하면 됩니다.

• 장점: 클라이언트가 라이브러리를 사용하는 특정 맥락 (예: 양수만 삽입하는 경우) 을 반영하므로, 더 간단하고 추론하기 쉬운 계약을 합성할 수 있습니다.
• 검증 방식: 모듈러 계약은 라이브러리만 독립적으로 테스트하지만, 컨텍스트 계약은 클라이언트와 라이브러리가 결합된 전체 프로그램을 테스트합니다.

2.2. 학습 프레임워크 (Learning Framework)

VMTLC 문제를 해결하기 위해 ICE (Implication, Counterexample, Example) 학습 알고리즘을 활용합니다.

1. CHC (Constrained Horn Clauses) 생성: 클라이언트 프로그램의 검증 조건을 CHC 형태로 변환합니다. 여기에는 클라이언트의 루프 불변식 (Loop Invariants) 과 라이브러리 메서드 계약에 대한 미해결 변수 (Predicates) 가 포함됩니다.
2. 일반화 CHC 솔버 (Generalizing CHC Solver):
   • 단순한 CHC 솔버는 주어진 양의 예제 (Positive Examples) 에만 맞춰 과적합 (Overfitting) 될 수 있어 테스트에서 실패할 수 있습니다.
   • 따라서 일반화 (Generalization) 능력을 갖춘 솔버 (예: ICE 학습기) 를 사용하여, 테스트에서 발견된 위반 사례를 포함하면서도 더 넓은 범위를 커버하는 계약을 학습합니다.
3. 반복적 검증 및 테스트 루프:
   • 합성 단계: CHC 솔버가 클라이언트 불변식과 라이브러리 계약을 합성합니다.
   • 테스트 단계: 합성된 계약을 테스트 생성기 (AFL++ 등) 에 입력하여 위반 사례를 찾습니다.
   • 피드백: 테스트가 실패하면 위반 사례를 '양의 예제 (Positive Examples)'로 변환하여 학습기에 전달하고, 다음 iteration 에서 계약을 수정하여 다시 학습합니다.
   • 이 과정이 모든 테스트를 통과하고 클라이언트가 검증될 때까지 반복됩니다.

2.3. 학습 알고리즘의 다양성

프레임워크는 다양한 학습 엔진을 지원하며, 실험에서는 다음 세 가지 방식을 비교했습니다:

• HornICE: 결정 트리 (Decision Tree) 를 기반으로 한 전통적인 기호적 학습 알고리즘.
• LLM (Large Language Models): Gemini v2.5 Pro 등을 사용하여 자연어 설명과 코드 맥락에서 계약을 제안하고, 검증 실패 시 수정을 요청하는 방식.
• Hybrid (HornICE + LLM): LLM 이 제안한 원자적 술어 (Atomic Predicates) 를 템플릿으로 사용하여 HornICE 가 결정 트리를 학습하는 방식.

3. 주요 기여 (Key Contributions)

1. VMTLC 문제의 공식화: 라이브러리 검증을 형식적 증명 대신 테스트 기반으로 대체하여 클라이언트 검증을 자동화하는 새로운 문제 정의를 제시했습니다.
2. 컨텍스트 계약의 도입: 클라이언트의 사용 맥락에 의존하는 더 간단하고 합성하기 쉬운 계약 개념을 제안하고, 이를 검증하는 프레임워크를 설계했습니다.
3. Dualis 도구 구현: 위의 프레임워크를 구현한 도구 Dualis를 개발했습니다. 이는 CHC 솔버, 테스트 생성기, ICE 학습기 (HornICE, LLM, Hybrid) 를 통합합니다.
4. 광범위한 벤치마크 평가: 오픈소스 데이터 구조 라이브러리 (Folly, Abseil 등) 를 사용하는 43 개의 C++ 클라이언트 프로그램에 대해 실험을 수행했습니다.

4. 실험 결과 (Evaluation Results)

• 성능: Dualis 는 기존 자동화 도구 (SeaHorn 등) 가 검증에 실패하거나 시간 초과를 한 대부분의 벤치마크 (43 개 중 38~41 개) 를 성공적으로 해결했습니다.
• 학습 방식 비교:
  • LLM 기반 접근: 가장 높은 성공률을 보였으며 (모듈러 38/43, 컨텍스트 41/43), 복잡한 논리 구조를 잘 추론했습니다.
  • HornICE: 템플릿의 한계로 인해 일부 복잡한 벤치마크에서 실패했습니다.
  • Hybrid: LLM 의 표현력과 HornICE 의 일반화 능력을 결합하여 좋은 성능을 보였습니다.
• 모듈러 vs 컨텍스트: 컨텍스트 계약이 모듈러 계약보다 더 적은 시간에 더 많은 벤치마크를 성공적으로 합성했습니다. 이는 컨텍스트 계약이 더 단순하고 합성하기 쉽기 때문입니다.
• 정확성: 합성된 모든 계약은 수동 검증 및 추가 테스트를 통해 논리적으로 유효함이 확인되었습니다.
• 위험성 분석 (Mutant Study): 의도적으로 버그를 주입한 프로그램 (테스트로 발견하기 어려운 희귀 경로 포함) 에 대해, 컨텍스트 계약은 일부 잘못된 프로그램을 '검증된' 것으로 오인할 수 있음을 보여주었습니다 (모듈러 계약은 이를 더 잘 차단함). 이는 컨텍스트 계약의 한계를 보여줍니다.

5. 의의 및 결론 (Significance & Conclusion)

이 논문은 대규모 코드베이스의 자동화된 형식적 검증을 위한 새로운 패러다임을 제시합니다.

• 확장성 (Scalability): 라이브러리의 완전한 형식적 검증이라는 비현실적인 요구를 완화하고, 테스트 기반의 검증을 통해 자동화 가능성을 크게 높였습니다.
• 실용성: 현재 자동화 도구로는 검증이 불가능한 복잡한 라이브러리를 사용하는 클라이언트 프로그램에 대해 검증 가능한 솔루션을 제공합니다.
• LLM 의 활용: LLM 을 ICE 학습기의 일부로 통합하여, 전통적인 기호적 방법만으로는 도달하기 어려운 합성 공간을 탐색할 수 있음을 입증했습니다.

결론적으로, Dualis와 VMTLC 프레임워크는 "검증 (Verification)"과 "테스팅 (Testing)"의 경계를 넘나드는 하이브리드 접근법이 대규모 소프트웨어 시스템의 신뢰성 보장에 있어 매우 유망한 방향임을 보여줍니다. 특히 컨텍스트 계약은 클라이언트 검증의 난이도를 획기적으로 낮추는 핵심 요소로 작용합니다.