ConVer: 확장 가능한 형식 소프트웨어 검증을 위한 계약 및 루프 불변량 합성 활용

대규모 C 프로그램의 형식 검증 (Formal verification)은 상태 공간 폭발 (state-space explosion) 문제로 인해 방해를 받습니다. 경계 모델 검사 (Bounded Model Checking, BMC) 도구들은 모든 중첩 구조를 언롤링 (unrolling)하여 미리 정해진 경계까지 전체 상태 공간을 인코딩해야 합니다. 우리는 하향식 구성적 검증 (top-down compositional verification) 도구인 ConVer를 제시합니다. 최상위 어설션 (top-level assertion)이 포함된 C 프로그램이 주어지면, ConVer는 검증을 하향식으로 분해합니다. 즉, 대규모 언어 모델 (Large Language Model, LLM)을 사용하여 시스템 속성으로부터 함수 계약 (function contracts)을 합성한 다음, CEGAR-CEGIS 루프 내에서 시스템 수준과 함수 수준의 검사를 교대로 수행하며, 검사가 실패할 때마다 SMART ICE 학습을 통해 계약을 정교화합니다. 우리는 점진적으로 난이도가 높아지는 4개의 벤치마크 제품군과 다른 최첨단 (State-of-the-art, SOTA) 도구들을 대상으로 ConVer를 평가합니다. 45개의 단순 C 프로그램으로 구성된 Frama-C 벤치마크에서 ConVer는 세 가지 LLM 백엔드에 걸쳐 82-96%의 검증 성공률을 달성하였으며, 수렴된 프로그램의 93-95%는 단 한 번의 CEGAR-CEGIS 반복만을 필요로 했습니다. X.509 파서 벤치마크 (6개 프로그램) 및 LF2C-Simple 제품군 (17개 프로그램)에서 ConVer는 각각 33-50% 및 82-88%의 성공률을 달성했습니다. 재귀 및 루프 집약적인 11개 프로그램으로 구성된 VerifyThis 제품군에서 Pre-Abstraction 전략은 55-64%의 성공률을 달성했습니다. 또한, 우리는 LF 모델을 속성을 보존하면서 C로 변환하여 ConVer가 이를 검증할 수 있게 해주는 전처리기 도구인 ESBMC-LF를 제시합니다. 우리는 ESBMC-LF를 사용하여 LF Verifier Benchmarks를 C로 트랜스파일 (transpile)하였으며, 이를 LF-Hard라고 명명합니다. 우리는 ConVer가 전체 LF-Hard 벤치마크의 67%를 성공적으로 검증함을 보여줍니다.