기술 요약: CONVER – 확장 가능한 형식 소프트웨어 검증을 위한 계약 및 루프 불변식 합성을 활용한 접근

문제 제기

대규모 C 프로그램의 형식적 검증은 현재 상태 공간 폭발 문제로 인해 방해받고 있습니다. ESBMC 및 CBMC와 같은 경계 모델 체킹 (BMC) 도구는 상태 공간을 SMT 수식으로 인코딩하기 위해 미리 정해진 경계까지 모든 중첩 구조 (루프 및 함수 호출) 를 풀어야 합니다. 프로그램 크기가 증가함에 따라 함수 수와 호출 깊이가 증가하여 SMT 인스턴스가 급격히 커지고, 이로 인해 검증이 처리 불가능해집니다. 함수 계약 (function contracts) 은 함수 내부 구현을 추상화하기 위한 표준 완화 기법이지만, 이러한 계약의 수동 작성은 전문가의 노력이 많이 필요하여 실제 현장에서는 거의 채택되지 않으며, 이로 인해 형식적 검증이 수백 줄 규모의 프로그램으로만 제한되고 있습니다.

방법론

CONVER는 대규모 언어 모델 (LLM) 을 활용하여 함수 계약과 루프 불변식을 자동 유도하도록 설계된 상향식 (top-down) 구성적 검증 도구입니다. 이는 ESBMC 를 기본 검증 엔진으로 활용하며 CEGAR-CEGIS(Counterexample-Guided Abstraction Refinement / Inductive Synthesis) 루프 내에서 작동합니다.

핵심 워크플로우

1. 상향식 분해: 개별 함수 명세부터 시작하는 대신, CONVER 는 main() 함수의 최상위 시스템 어설션으로 시작합니다. LLM 은 이 시스템 속성을 증명하기에 충분한 초기 함수 계약 (사전 조건, 사후 조건, 할당 절) 을 합성합니다.
2. 이중 수준 검증:
   • 시스템 수준: 함수 호출은 추상 계약 스텁으로 대체됩니다. ESBMC 는 함수 내부 구현을 탐색하지 않고 계약이 참이라고 가정할 때 시스템 속성이 성립하는지 검증합니다.
   • 함수 수준: 각 함수의 실제 구현은 해당 특정 계약에 대해 고립적으로 검증됩니다.
3. 정제 루프:
   • SMART ICE 를 활용한 CEGAR: 검증이 실패할 경우, 반례를 양수(반드시 포함해야 하는 상태), 음수(반드시 제외해야 하는 상태), 함의(귀납적 관계) 예제로 분류합니다. 이러한 구조화된 피드백은 LLM 이 계약을 정제하도록 안내합니다. 시스템 수준 실패는 더 강력한 계약을, 함수 수준 실패는 더 약한 (더 관대한) 계약을 유도합니다.
   • CEGIS 에스컬레이션: CEGAR 가 정체될 경우, 시스템은 제약 기반 합성 단계로 에스컬레이션합니다. 실패한 시도에서 수집된 예제를 누적하여 LLM 이 관찰된 모든 행동과 일관된 계약을 찾도록 유도합니다.
4. 사전 추상화 전략: 함수 수준에서도 상태 폭발을 유발하는 높은 구조적 복잡성 (예: 깊은 재귀, 경계가 없는 루프) 을 가진 함수의 경우, CONVER 는 사전 추상화 단계를 수행합니다. 이는 초기 검증을 가능하게 하는 "느슨하지만" 건전한 과대 근사 계약 (예: 널 안전성, 범위 경계) 을 생성하며, 시스템 속성이 성립하는 경우 나중에 정밀한 계약으로 대체됩니다.
5. ESBMC-LF: Lingua Franca (LF) 벤치마크를 검증 속성을 (MTL 수식) 유지한 채 단일 C 프로그램으로 변환하는 전용 전처리기입니다. 이를 통해 CONVER 는 원래 LF 로 작성된 복잡한 반응형 시스템을 검증할 수 있습니다.

주요 기여

1. 상향식 계약 유도: 시스템 수준 어설션에서 직접 함수 계약을 유도하는 방법론으로, 시스템 증명을 위해 필요한 속성에만 초점을 맞춤으로써 수동 명세 노력을 최소화합니다.
2. SMART ICE 학습을 활용한 CEGAR: ESBMC 반례를 양수, 음수, 함의 예제로 분류하여 표적화된 LLM 재합성을 안내하는 반복적 정제 루프로, 표준 CEGAR 보다 수렴성을 개선합니다.
3. 루프 불변식 합성: 경계 검사가 불충분한 함수를 위해 CEGIS 루프에 통합된 온-디맨드 (on-demand) 귀납적 불변식 생성 단계입니다.
4. 종단 간 평가: 알고리즘적, 재귀적, 포인터 중심, 그리고 반응형 시스템 등 다양한 구조를 다루는 네 가지 벤치마크 스위트에 걸친 포괄적인 실증 연구입니다.
5. ESBMC-LF 전처리기: LF 벤치마크를 검증 구조를 유지한 채 C 로 변환하여 검증을 가능하게 하는 도구로, "LF-Hard" 스위트의 검증을 용이하게 합니다.

실험 결과

저자들은 세 가지 LLM 백엔드 (Qwen3.5-Plus, Claude Haiku 4.5, GPT-OSS 120b) 를 사용하여 네 가지 벤치마크 스위트에 포함된 79 개 C 프로그램에서 CONVER 를 평가했습니다.

• Frama-C 벤치마크 (45 개 프로그램): CONVER 는 **8296%**의 검증 성공률을 달성했습니다. 특히, 수렴된 프로그램의 **9395%**는 단일 CEGAR 반복만 필요했습니다. GPT-OSS 120b 가 96% 로 가장 우수한 성능을 보였습니다.
• LF2C-Simple (17 개 프로그램): **82~88%**의 성공률을 달성하여, 주요 벤치마크를 넘어 파이프라인의 일반화 능력을 입증했습니다.
• X.509 파서 (6 개 프로그램): **33~50%**의 성공률을 달성했습니다. 낮은 성공률은 현재 LLM 들이 저수준 메모리 연동에 대한 건전한 포인터 계약을 합성하는 데 어려움을 겪고 있음을 보여줍니다.
• VerifyThis (11 개 프로그램): 사전 추상화 전략을 사용하여 CONVER 는 **55~64%**의 성공률을 달성했습니다. Claude Haiku 4.5 는 전문가 참조 결과 (11 개 중 7 개) 와 일치했습니다.
• LF-Hard (24 개 프로그램): 이들은 LF 벤치마크의 복잡한 단일 C 번역본들입니다. 직접 ESBMC 검증은 42%(24 개 중 10 개) 에서만 성공했습니다. CONVER 의 사전 추상화 전략을 사용하면 성공률이 **46~62%**로 향상되었으며, GPT-OSS 120b 가 62% 로 가장 높았습니다.

Ablation Study (RQ2): 연구 결과, SMART ICE 학습은 "능력 증폭기" 역할을 하는 것으로 나타났습니다. 이는 고성능 모델의 결과를 크게 향상시켰습니다 (GPT-OSS 120b: +5%, Qwen: +2%). 반면, 반례 데이터베이스에 구문적 노이즈가 누적되어 더 작은 모델의 성능은 저하되었습니다 (Claude Haiku 4.5: -2%).

중요성 및 주장

본 논문은 CONVER 가 가장 노동 집약적인 요소인 계약 명세를 자동화함으로써 형식적 검증의 확장성 장벽을 해결한다고 주장합니다. 상향식 분해와 LLM 기반 합성 및 구조화된 반례 피드백을 결합함으로써, CONVER 는 단일 블록 BMC 도구로는 처리 불가능한 프로그램의 검증을 가능하게 합니다.

저자들은 검증 결정이 LLM 이 아닌 모델 체커 (ESBMC) 에 위임되며, LLM 은 후보 주석을 제안만 한다는 점에서 이 접근 방식이 **건전 (sound)**하다고 강조합니다. 결과는 잘 구조화된 프로그램의 경우 CEGAR+ICE 루프가 대체로 모델에 무관하지만, 복잡하거나 포인터가 많거나 재귀적인 프로그램의 경우 LLM 백엔드의 품질이 결정적 제약 요인이 된다는 것을 시사합니다. 또한, ESBMC-LF 와 같은 도구를 통해 도메인 특화 언어 (예: LF) 를 C 로 변환하면 표준 C 검증기가 복잡한 반응형 시스템 벤치마크를 처리할 수 있음을 보여줍니다.

논문은 결론적으로, 이 접근 방식이 단일 어설션 프로그램에는 효과적이지만, 다중 속성 프로그램을 처리하고 하이브리드 모델 선택 전략을 조사하기 위해서는 향후 연구가 필요하다고 겸손하게 언급합니다. 또한, 포인터 역참조 대상에 대한 프레임 조건을 기계적으로 검증할 수 없는 ESBMC 의 현재 한계를 인정합니다.