기술 요약: CNnotator: LLM 기반 메모리 안전성 어노테이션 합성

문제 정의

메모리 안전성 오류는 C 및 C++ 시스템에서 보안 취약점의 상당 부분을 차지합니다. Rust나 Java와 같은 현대적인 메모리 안전 언어와 달리, C는 인간이 추출하고 검증하기 어려운 암시적인 메모리 사용 패턴에 의존합니다. 공식적 방법론(formal methods)과 AI는 각각 패턴을 "추측"하는 데 뛰어난 신경망과 형식을 "체크"하는 데 뛰어난 공식 도구라는 상호 보완적인 강점을 가지고 있지만, 레거시 C 코드를 검증 가능한 사양(specification)으로 자동 변환하는 과정에는 공백이 존재합니다. 구체적으로, C 프로그램이 메모리(소유권, 할당, 해제)를 어떻게 조작하는지 결정하는 작업은 인간에게는 매우 번거롭지만, 대규모 언어 모델(LLM)에 의해 추론 가능한 영역입니다. 과제는 이러한 암시적 패턴을 정확하게 나타내어 검증이나 안전한 트랜스파일링(transpilation)을 가능하게 하는 형식적 사양을 생성하는 것입니다.

방법론

저자들은 "추측 및 확인(guess-and-check)" 루프를 통해 C 코드에 대한 메모리 안전성 어노테이션을 합성하는 도구인 CNnotator를 제시합니다. 이 시스템은 분리 논리(separation logic)에 기반한 계약 언어인 CN(Rust의 borrow checker와 유사하게 명시적인 메모리 표현을 가지며 Frama-C와 유사함)을 대상으로 합니다.

CNnotator 워크플로우

이 도구는 다음과 같은 반복적인 루프로 작동합니다:

1. 전처리(Preprocessing): 도구는 C 프로젝트 파일들을 하나의 컨텍스트로 병합하고, 할당/해제를 올바르게 처리하기 위해 필요한 CN 라이브러리와 매크로를 주입합니다. 이후 Tree-sitter를 사용하여 코드를 추상 구문 트리(AST)로 파싱합니다.
2. 함수 선택(Function Selection): AST 위치를 보존하기 위해 파일의 하단부터 시작하여 함수를 순회합니다.
3. LLM "추측" (어노테이션 생성):
   • LLM은 CN 문법 가이드(CN 튜토리얼에서 스크래핑됨), 전체 프로젝트 코드, 그리고 특정 대상 함수에 대한 프롬프트를 받습니다.
   • 어노테이션을 생성하기 전, LLM은 해당 함수가 본질적으로 안전하지 않은지(예: use-after-free) 식별하도록 요청받습니다. 만약 안전하지 않다고 판단되면, 해당 함수에 대한 프로세스를 중단하고 버그를 설명하는 주석을 삽착합니다.
   • 함수가 안전해 보이면, LLM은 전제 조건(소유권 요구 사항)과 사후 조건을 명시하는 CN 어노테이션을 생성합니다.
4. 형식적 "확인" (테스트):
   • 생성된 어노테이션은 C 코드에 주입됩니다.
   • Fulminate 백엔드가 사양을 런타임 체크로 컴파일합니다.
   • Bennet 프레임워크는 전제 조건으로부터 무작위 입력 생성기를 유도하여 구체적인 힙 상태를 생성합니다.
   • 시스템은 생성된 사양 하에서 코드가 메모리 안전성 위반 없이 실행되는지 확인하기 위해 **100개의 속성 기반 테스트(property-based tests)**를 실행합니다.
5. 정제(Refinement):
   • 성공: 100개의 테스트가 모두 통과하면 어노테이션이 수락됩니다.
   • 실패: 테스트가 실패하면 에러 메시지가 LLM에 피드백되어 어노테이션을 정제하는 데 사용됩니다. 이 루프는 최대 6회까지 실행됩니다.
   • 구문 오류(Syntax Errors): 초기 생성 시 구문 오류로 인해 실패하는 경우(종종 도움이 되지 않는 컴파일러 메시지를 생성함), 시스템은 에러 피드백을 사용하는 대신 LLM의 비결정론적 특성을 활용하여 원래의 프롬프트로 최대 2회 추가 재시도를 수행합니다.

주요 기여

• 도구 개발: 에이전트 제어를 위한 LangChain/LangGraph, 파싱을 위한 Tree-sitter, 그리고 자동화된 테스트를 위한 Fulminate/Bennet 프레임워크를 통합한 Python 기반 도구인 CNnotator을 제작했습니다.
• 하이브리드 검증 접근 방식: LLM이 분리 논리 사양(CN)을 생성하고, 형식적 테스트 백엔드가 이를 검증함으로써 LLM의 추론을 신뢰할 필요 없이 효과적으로 문제를 해결하는 실용적인 파이프라인을 입증했습니다.
• 벤치마크 스위트: 단순한 소유권부터 글로벌 변수 및 매크로가 포함된 복잡한 루프에 이르기까지, 어노테이션이 가능한 31개의 C 함수와 도구의 버그 탐지 능력을 테스트하기 위해 설계된 3개의 본질적으로 안전하지 않은 함수로 구성된 테스트 스위트를 구축했습니다.

실험 결과

저자들은 31개의 어노테이션 가능 함수에 대해 다섯 가지 OpenAI LLM 백엔드(o3, o4-mini, o3-mini, GPT-4.1, GPT-4o)를 대상으로 CNnotator을 평가했습니다.

• 성능: 추론 모델인 o3가 가장 높은 성능을 보였으며, 31개 함수 중 96.8%(30/31)를 성공적으로 어노테이션했습니다. o3는 첫 번째 시도에서 **90.3%**의 성공률을 기록했으며, 성공적인 어노테이션당 평균적으로 단 1.10회의 시도만을 필요로 했습니다.
• 채팅 모델: 채팅 모델인 GPT-4o조차 첫 번째 시도 성공률 64.5%, 전체 성공률 **71.0%**를 달려 새로운 o3-mini보다 높은 첫 번째 시도 지표를 보여주었습니다.
• 실패 모드:
  • 도구는 수동으로 삽입된 세 가지의 본질적으로 안전하지 않은 함수(use-after-free, double-free)를 모두 식별하였고, 어노테이션을 거부했습니다.
  • 수동 검사 결과, 잘못된 긍정(테스트는 통과하지만 틀린 어노테이션)은 관찰되지 않았습니다.
  • 과도하게 허용적인 어노테이션(필요 이상의 소유권을 요구하는 경우)이 잠재적인 문제로 지적되었으나, 여전히 유효한 사양을 제공하므로 수용 가능한 것으로 간주되었습니다.
• 효율성: 시스템은 소규모에서 중규모 프로그램에 대해 AI 보조 어노테이션이 높은 성공률과 함께 최소한의 반복만으로 실용적인 수준에 도달했음을 보여줍니다.

의의 및 주장

본 논문은 CNnotator가 실제 C 코드베이스에 대한 AI 보조 어노테이션의 생존 가능성을 입증한다고 주장합니다. LLM의 패턴 인식 능력과 형식적 테스트 도구의 엄격한 체크를 결합함으로써, 이 접근 방식은 형식 검증의 "추측 및 확인" 특성을 해결합니다.

저자들은 이 연구를 다음 단계로 포지셔닝합니다:

1. 코드 현대화: 먼저 메모리 안전성 계약을 확립함으로써 레거시 C 코드를 더 안전한 언어(예: Rust)로 마이그레이션하는 것을 용이하게 합니다.
2. 검증 자동화: 전통적으로 수동적이고 오류가 발생하기 쉬운 작업인 메모리 안전성 사양 생성을 자동화합니다.
3. 실용성: 현재의 모델들이 C의 메모리 소유권 복잡성을 다룰 수 있으며, 인간의 개입을 최소화하면서 높은 성공률을 달착할 수 있음을 보여줍니다.

본 논문은 벤치마크가 50줄 미만의 단순한 제어 흐름을 가진 함수들로 구성되어 있으며, 타입 캐스팅이나 고급 포인터 연산과 같은 복잡한 프로덕션 코드 패턴을 아직 다루지 않는다는 점을 언급하며 범위를 겸허하게 제한하고 있습니다. 그러나 결과는 LLM의 능력이 향로됨에 따라 이 기술이 더 크고 복잡한 시스템으로 확장될 수 있음을 시사합니다.