Natural Language based Specification and Verification

기술 요약: 자연어 기반 명세 및 검증 (NLForge)

문제 제기
C 및 C++ 프로그램의 메모리 안전성 위반 (예: 잘못된 역참조, 사용 후 해제, 범위 초과 접근) 은 여전히 소프트웨어 취약점의 주요 원인입니다. 이러한 오류는 종종 할당, 해제, 초기화, 별칭 (aliasing) 과 관련된 복잡한 절차 간 상호작용에서 비롯되며, 전통적인 정적 분석 도구들은 대규모로 이를 검증하는 데 어려움을 겪습니다. 대규모 언어 모델 (LLM) 은 버그를 식별하는 데 뛰어난 능력을 입증해 왔지만, 형식 검증을 통해 새로운 취약점의 도입을 예방하는 데는 상당한 도전에 직면해 있습니다. 기존 검증 파이프라인은 일반적으로 루프 불변식, 전/후 조건과 같은 경직된 형식 언어로 명세를 요구하여 높은 주석 부담을 초래합니다. LLM 을 사용하여 이러한 형식 명세를 합성하려는 이전 시도들은 제한적인 성공만을 보였습니다. 또한 최근 벤치마크에 따르면, 단일 함수 검증에서 구성적 (compositional), 다중 함수 추론으로 전환될 때 LLM 의 성능이 급격히 저하되는데, 이는 주로 컨텍스트 창 제한과 전역 의미 일관성을 유지하는 어려움 때문입니다.

방법론: NLForge
저자들은 NLForge를 제안합니다. 이는 경직된 형식 산물 대신 자연어 명세를 생성하고 추론하는 데 LLM 을 활용하는 구성적 검증 프레임워크입니다.该系统은 프로그램 호출 그래프에 대해 하향식 (callee-first) 분석을 수행합니다.

1. 파이프라인 아키텍처:

   • 전처리: 시스템은 C/C++ 코드에서 함수 정의, 시그니처, 호출 지점을 추출하여 호출 그래프를 구성합니다. 해결되지 않은 호출은 외부 스텁 (stub) 을 통해 처리됩니다.
   • 하향식 분석: 프레임워크는 위상적 순서 (호출자를 호출하기 전에 피호출자를 처리) 로 호출 그래프에 대해 일련의 분석 패스를 수행합니다.
   • 자연어 요약: 형식 논리를 생성하는 대신, LLM 은 특정 속성에 대해 구조화된 자연어 요약 (자연어 설명이 포함된 타입 지정 JSON 으로 인코딩) 을 생성합니다.
     • 할당/해제/초기화: 힙 객체 생성, 해제 효과, 출력 매개변수 초기화를 요약합니다.
     • 메모리 안전성 계약: 전제 조건 (예: 비-null, 해제되지 않음, 버퍼 크기) 과 후제 조건을 추론합니다.
     • 누수 및 정수 요약: 해결되지 않은 의무 사항과 정수 오버플로 위험을 추적합니다.
   • 구성적 검사: 최종 검증 패스에서 LLM 은 자체적으로 추론된 전제 조건과 피호출자의 자연어 요약을 사용하여 함수를 분석합니다. 이 모델은 전체 피호출자 구현을 인라인 (inlining) 하지 않고 피호출자 계약에 대한 안전성 요구 사항을 확인하는 추론 에이전트 역할을 하며 잠재적 실행 상태를 유지합니다.

2. 설계 근거:
   이 접근법은 코드와 문서로 훈련된 LLM 이 경직된 형식 표기법보다 자연어 요약을 더 일관되게 생성, 해석, 정제할 수 있다는 관찰에서 영감을 받았습니다. 이 설계는 검증 문제를 재사용 가능한 의미 요약으로 분해하여, 모델이 매 호출자마다 원본 소스 코드를 재분석하는 대신 피호출자에 대한 명시적으로 명시된 가정 하에서 함수를 추론할 수 있도록 합니다.

주요 기여

• 구성적 프레임워크: LLM 을 사용하여 메모리 안전성 속성을 추론하고 검증하는 C/C++ 을 위한 하향식 절차 간 검증 프레임워크.
• 자연어 중간 표현: 외부 심볼릭 체커를 위한 형식 명세 생성에 초점을 맞춘 기존 작업과 대조적으로, 검증을 위한 중간 표현으로 자연어 의미 요약을 도입함.
• 단계적 분석 파이프라인: 메모리 안전성 추론을 재사용 가능한 요약 (할당, 해제, 초기화, 호출자 측 의무) 으로 분해하여 후속 단계에서 LLM 에 다시 피드백하는 방식.
• 실증 평가: SV-COMP 2026 벤치마크에서 구성적 추론과 비구성적 전체 프로그램 프롬핑트 (whole-program prompting) 베이스라인을 비교한 연구.

결과
저자들은 SV-COMP 2026 메모리 안전성 벤치마크의 일부에 대해 NLForge 를 평가했으며, 네 가지 LLM 백본 (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite, Qwen3.5-27B-UD-Q4) 을 사용했고 전통적인 검증기 (CPAchecker, Symbiotic, Ultimate Automizer) 와 비교했습니다.

• RQ1 (검증기로서의 LLM): LLM 기반 분석은 높은 재현율 (recall) 과 커버리지를 보여주어 대부분의 참 양성 (true positives) 을 식별했습니다 (예: Sonnet-4.6 은 valid-memsafety 에서 99.8% 의 재현율을 달성). 그러나 전통적인 도구보다 훨씬 많은 거짓 양성 (false positives) 을 생성하며, 아직은 독립적인 정합성 (sound) 검증기로 사용될 수 없습니다. 전통적인 도구는 거짓 양성을 피하기 위해 어려운 경우에 종종 "알 수 없음 (Unknown, UNK)"을 반환하는 반면, LLM 은 더 높은 오류율로 확정적인 답변을 제공합니다.
• RQ2 (구성적 검증): 구성적 접근법은 복잡한 실제 제어 흐름 및 데이터 구조 벤치마크에서 특히 비구성적 베이스라인보다 크게 우월한 성능을 보였습니다.
  • 모든 모델에서 구성적 실행은 참 양성을 3,390 개에서 3,476 개로 늘렸고, 거짓 음성을 301 개에서 216 개로 줄였습니다.
  • 개선 효과는 작은 모델에서 가장 두드러졌습니다 (예: Qwen3.5-27B-Q4 는 거짓 음성이 218 개에서 97 개로 감소) 및 강력한 절차 간 추론이 필요한 벤치마크에서 두드러졌습니다.
  • 합성적이고 국소화된 Juliet 테스트에서는 개선이 덜 일관적이었는데, 이는 비구성적 모델이 로컬 패턴을 직접 활용할 수 있었기 때문입니다.

의의 및 주장
이 논문은 검증에서 LLM 을 활용하는 방식의 전환을 주장합니다. 외부 엔진을 위한 형식 산물의 생성자로만 취급하는 것에서 벗어나, 구조화되고 재사용 가능한 자연어 요약을 기반으로 추론하는 에이전트로 사용하는 것입니다.

• 실용성: 자연어는 전체 프로그램 프롬프팅이 모델의 추론 예산이나 컨텍스트 창을 초과하는 작업에 특히 유용한 구성적 검증을 가능하게 하는 실용적인 중간 명세 계층으로 작용합니다.
• 한계: 저자들은 자연어의 비형식성이 보정 문제 (높은 거짓 양성) 로 이어지며, 이 접근법은 생성된 요약의 품질에 민감하다고 인정합니다. 요약의 오류는 전파되어 증폭될 수 있습니다.
• 미래 전망: 이 연구는 LLM 이 아직 정합적인 형식 검증을 대체할 수는 없지만, 확장 가능한 버그 찾기 검증에 대한 유망한 방향을 제시한다고 제안합니다. 향후 연구는 보정 개선, 요약과 심볼릭 검사의 결합, 간접 호출 및 힙 불변식과 같은 복잡한 기능을 더 견고하게 처리하는 데 초점을 맞춰야 합니다.

이 연구는 LLM 이 메모리 안전성을 검증할 수 있는지가 아니라, 어떤 표현과 분해를 통해 더 신뢰할 수 있게 되는지가 핵심 질문이라고 결론지으며, 자연어가 모듈식 프로그램 구조와 LLM 추론 능력 사이의 간극을 효과적으로 연결할 수 있음을 강조합니다.