Agentic Separation Logic Specification Synthesis

Motivation

• Known: LLM 기반 코드 명세(contract) 합성이 유망함이 이전 연구들(Wen et al., 2024; Ma et al., 2025 등)에서 보여졌고, separation logic은 infer 같은 verifier에서 힙 조작 코드를 다루는 핵심 논리로 사용되어 왔으며, coverage-guided fuzzing(libFuzzer 등)은 코드 경로 탐색과 취약점 탐지에 널리 쓰여왔다.
• Gap: 기존 LLM 기반 접근법들은 수백만 라인 규모의 대형 C++ 저장소로 스케일링, dynamic memory/heap-allocated data structure 같은 systems code 특성을 표현할 수 있는 명세의 표현력, 그리고 잘못된 후보를 걸러내는 체계적 검증이라는 세 요구사항을 동시에 만족시키지 못했다.
• Why: 정확성 보장 없는 LLM 기반 자동 프로그래밍이 확산되는 상황에서, 코드 명세(contract)는 리팩토링, 트랜스파일레이션, 최적화, 검증 등 다양한 응용의 기반이 되므로 대규모 실전 systems software에 대해 표현력 있고 검증된 명세를 자동 합성하는 것은 소프트웨어 신뢰성 확보에 중요하다.
• Approach: Spec-Agent는 separation logic을 통한 힙 인지적(resource-aware) 명세 표현과, 기존 유닛 테스트를 fuzz harness로 일반화하여 이를 pseudo-oracle로 활용하는 counterexample-guided refinement를 결합한 agentic 파이프라인을 제안한다.

Achievement

1. 대규모 스케일 검증: 4백만 라인 이상의 오픈소스 C++ 코드베이스에서 함수의 85%에 대해 유효한 명세를 합성함.
2. False positive 없는 검증: fuzzing과 전문가 검증 하에서 관찰된 false positive가 없음을 입증함.
3. 비용 효율성: Claude Code Opus 4.6 대비 10배 낮은 token cost로 더 우수한 성능을 달성함.
4. 적응형 명세 언어 선택기: propositional, first-order, propositional separation, first-order separation logic의 4단계 표현력 사다리(ladder)를 통해 조건 분기, 반복 루프, 힙 구조를 하나의 파이프라인에서 모두 다룸.

How

• 각 함수에 대해 정적 분석(static analysis)과 런타임 힙 추적(runtime heap tracing)을 사용해 목표 명세 언어를 propositional, first-order, propositional separation, first-order separation logic 중에서 선택
• 프로젝트의 기존 functional test를 fuzz harness로 일반화하여 fuzzing 커버리지를 유닛 테스트보다 훨씬 넓게 확보
• LLM이 생성한 후보 명세를 fuzzing으로 stress-test하고, 명세를 위반하는 입력을 counterexample로 LLM에 피드백하여 반복적으로 정제(refine)
• Prop, FOL, Prop SL, FOSL 네 가지 문법(Figure 3)에 기반한 order-theoretic lattice(Figure 5)로 명세의 표현력 단계를 관리

Originality

• Fuzz testing을 버그 탐지 도구가 아니라 명세 추론을 위한 강력한 pseudo-oracle로 재해석하여 사용한 최초의 시도
• Separation logic 기반 표현력과 fuzzing 기반 검증을 명세 합성(specification synthesis)에서 결합한 최초의 시스템
• Propositional부터 first-order separation logic까지 표현력이 증가하는 네 단계의 명세 언어를 정적/동적 분석으로 적응적으로 선택하는 메커니즘 제안
• 수백만 라인 규모의 실제 C++ 오픈소스 저장소에 대해 명세 합성을 최초로 적용

Limitation & Further Study

• 논문 발췌본에는 실험 세부사항(BDE 벤치마크 특성, 함수 선정 기준, 전문가 검증 절차의 엄밀성 등)이 충분히 제시되지 않아 85%라는 수치의 일반화 가능성 평가가 제한적임
• Fuzzing이 pseudo-oracle로 사용되지만 fuzzing이 도달하지 못하는 코드 경로에 대해서는 여전히 false negative(과도하게 강한/틀린 명세를 못 잡아내는 경우) 위험이 남아있을 수 있음
• 완전한 program verifier와의 통합이나 실제 검증 파이프라인으로의 연결에 대한 논의가 부족해 보이며, 후속 연구로 Frama-C나 infer 같은 verifier와의 end-to-end 결합 검증이 필요함
• C++ 이외 언어(Rust, Java 등)로의 일반화 가능성에 대한 논의가 미흡함

Evaluation

총평: Separation logic 표현력과 fuzz testing 기반 counterexample-guided refinement를 결합해 대규모 실전 C++ 코드베이스에서 실용적 수준의 명세 합성을 달성한 참신하고 의미 있는 연구로, 시스템 소프트웨어 검증 및 자동 프로그래밍 신뢰성 확보에 기여할 잠재력이 크다.