A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

본 논문은 정적 분석과 LLM 기반 추론을 결합한 모듈형 프레임워크인 Preguss 를 통해 대규모 프로그램의 잠재적 런타임 오류를 기반으로 인터프로시저 명세를 자동 생성 및 정제함으로써, 기존 LLM 기반 접근법보다 우수한 확장성을 보이며 수천 줄 규모의 프로그램에 대한 검증 노력을 80.6%~88.9% 감소시킨다고 제안합니다.

핵심

🏗️ 비유: 거대한 성을 지어보는 건축가

상상해 보세요. 여러분이 **1,000 개가 넘는 벽돌 (코드 라인)**로 이루어진 거대한 성을 짓고 있습니다. 이 성이 무너지지 않고 안전하게 작동하려면, 모든 벽돌이 제자리에 있고, 문이 제대로 닫히며, 다리가 무너지지 않는지 확인해야 합니다. 이를 **'프로그램 검증'**이라고 합니다.

하지만 문제는 이 성이 너무 크다는 것입니다. 한 번에 전체를 다 살펴보는 것은 인간에게도, 최신 인공지능 (LLM) 에게도 불가능합니다.

1. 기존 방법의 문제점: "눈이 멀고, 기억력이 짧은 거인"

기존의 인공지능 (LLM) 은 이 거대한 성을 한 번에 보려고 하면 두 가지 치명적인 약점이 있습니다.

• 기억력 부족 (Context Limit): 성 전체를 한 번에 보려고 하면 인공지능의 '기억 창 (Context Window)'이 꽉 차서 중요한 부분을 놓칩니다.
• 혼란: 성의 각 부분 (함수) 이 서로 복잡하게 연결되어 있는데, 인공지능은 "어디서부터 시작해야 하지?"라고 헤매며 엉뚱한 부분만 지적하거나, 너무 많은 가정을 만들어냅니다.

2. 프레구스 (Preguss) 의 혁신: "위험 신호를 쫓는 탐정"

프레구스는 이 문제를 해결하기 위해 두 가지 전략을 사용합니다.

① 분할 정복 (Divide and Conquer): "작은 조각으로 나누기"
프레구스는 성 전체를 한 번에 보지 않습니다. 대신, **자동화된 검사기 (정적 분석기)**를 먼저 돌려서 "여기서 다리가 무너질 수 있어!"라고 경고하는 **위험 신호 (Runtime Error Assertions)**를 찾아냅니다.

• 비유: 성 전체를 다 보지 않고, "이 벽돌이 흔들리는구나!"라고 경고하는 특정 지점만 집중적으로 봅니다.
• 이 위험 신호들을 바탕으로 검증해야 할 **작은 단위 (V-Unit)**들을 만들어냅니다. 마치 거대한 성을 작은 방 (Verification Unit) 들로 쪼개는 것과 같습니다.

② 협력 (Synergy): "인공지능과 수사의 팀워크"
이제 인공지능 (LLM) 이 등장합니다. 하지만 그냥 "이 성을 검증해 줘"라고 하는 게 아닙니다.

• 위험 신호를 가이드로: "여기서 다리가 무너질 수 있다는 신호가 왔어. 이 다리가 무너지지 않게 하려면 어떤 조건이 필요할까?"라고 인공지능에게 물어봅니다.
• 상호작용: 인공지능이 "아, 이 다리가 무너지지 않으려면 저 벽돌이 튼튼해야 해 (전제조건)"라고 답하면, 검증 도구가 이를 확인합니다. 만약 틀리면 인공지능에게 "틀렸어, 다시 생각해 봐"라고 피드백을 주고, 인공지능이 다시 수정합니다.
• 연쇄 반응: 한 방의 다리가 튼튼해지면, 그 방을 연결하는 복도도 튼튼해집니다. 이렇게 작은 단위 하나하나를 검증하며 성 전체의 안전을 증명해 나갑니다.

---

🚀 프레구스가 이룬 성과

이 논문은 프레구스가 실제로 얼마나 강력한지 증명했습니다.

1. 거대한 프로젝트도 가능: 1,000 줄이 넘는 실제 소프트웨어 (우주선 제어 시스템, 암호화 모듈 등) 를 검증했습니다. 기존 방법들은 이 정도 규모에서는 아예 작동조차 안 했지만, 프레구스는 성공했습니다.
2. 인간의 노동을 90% 줄임: 예전에는 전문가들이 수개월 동안 수동으로 코드를 확인해야 했지만, 프레구스는 인간의 개입을 80~90% 이상 줄여주었습니다.
3. 실제 버그를 찾아냄: 단순히 "안전하다"고 말하는 것을 넘어, 실제 우주선 제어 시스템에서 **6 가지의 치명적인 버그 (초기화되지 않은 변수 접근 등)**를 찾아내어 개발자들이 수정할 수 있게 했습니다.

💡 핵심 요약

• 문제: 너무 큰 프로그램을 검증할 때, 인공지능은 기억력이 부족하고 복잡한 연결고리를 이해하지 못합니다.
• 해결책 (프레구스):
  1. **위험 신호 (Runtime Error)**를 찾아내어 검증할 대상을 작은 조각으로 나눕니다.
  2. 인공지능에게 **"이 특정 위험을 막으려면 어떤 조건이 필요한가?"**라고 구체적으로 물어봅니다.
  3. 검증 도구의 피드백을 받아 인공지능이 **조건 (명세)**을 수정하고, 이를 반복하며 성 전체를 안전하게 만듭니다.

한 줄 요약:

"거대한 성을 한 번에 다 보려 하지 말고, 위험한 곳을 찾아내어 조각조각 나누어 인공지능과 함께 하나하나 안전하게 다지는 새로운 검증 방법입니다."

이 기술은 앞으로 우리가 사용하는 스마트폰 앱, 자율주행차, 우주선 등 매우 안전이 중요한 소프트웨어를 자동으로 검증하는 데 큰 역할을 할 것으로 기대됩니다.

기술 요약

1. 문제 정의 (Problem)

대규모 소프트웨어 및 하드웨어 시스템의 완전 자동화된 검증은 형식 방법론의 성배 (Holy Grail) 로 간주되지만, 여전히 다음과 같은 심각한 도전 과제에 직면해 있습니다.

• LLM 의 확장성 한계: 최근 대규모 언어 모델 (LLM) 은 형식 명세 (Formal Specification) 생성을 통해 자동화 수준을 높였으나, 수천 줄의 코드 (LoC) 를 가진 대규모 프로그램의 경우 긴 컨텍스트 추론 (Long-context reasoning) 한계로 인해 전체 프로그램을 한 번에 처리하거나 정밀한 정보를 찾는 데 어려움을 겪습니다.
• 복잡한 절차 간 명세 (Interprocedural Specifications) 의 부재: 대규모 프로그램은 복잡한 호출 계층 구조를 가지며, 이를 검증하기 위해서는 전제조건 (Precondition), 사후조건 (Postcondition), 루프 불변식 등 다양한 절차 간 명세가 필요합니다. 기존 LLM 기반 접근법들은 주로 단일 함수 내 명세에 집중하거나, 전제조건과 사후조건의 본질적 차이를 고려하지 않고 전체적으로 명세를 생성하여 과도하게 제한적인 (Over-constrained) 전제조건을 생성하거나 실제 런타임 오류 (RTE) 를 놓치는 경우가 많습니다.
• 수동 검증의 비용: 기존 정적 분석 도구 (Abstract Interpretation 기반) 는 많은 수의 오탐 (False Positives) 을 발생시키며, 이를 제거하거나 정확한 명세를 작성하는 데는 여전히 높은 수준의 수동 전문가 노력이 필요합니다.

2. 제안 방법론: Preguss (Methodology)

저자들은 Preguss라는 모듈식, 세분화된 프레임워크를 제안합니다. 이는 정적 분석 (Static Analysis) 과 연역적 검증 (Deductive Verification) 을 시너지 효과로 결합하며, 분할 정복 (Divide-and-Conquer) 전략을 통해 두 단계로 작동합니다.

1 단계: 잠재적 RTE 기반 검증 단위 구축 및 우선순위 결정 (Divide)

• 가드 어설션 (Guard Assertion) 생성: 정적 분석기 (Frama-C/Eva, Frama-C/Rte) 를 실행하여 잠재적인 런타임 오류 (RTE) 를 나타내는 어설션을 추출합니다.
• 검증 단위 (V-Unit) 구성: 각 RTE 어설션을 중심으로 해당 함수 (Host function) 와 그 호출자/피호출자 (Callee) 를 포함하는 최소한의 프로그램 슬라이스를 추출하여 'V-Unit'을 구성합니다.
• 우선순위 큐: 호출 그래프 (Call Graph) 를 기반으로 V-Unit 을 하향식 (Bottom-up) 순서로 정렬합니다. 즉, 피호출 함수의 명세가 먼저 생성되어야 호출 함수의 검증이 가능하도록 순서를 제어합니다.

2 단계: 세분화된 절차 간 명세 합성 (Conquer)

• LLM 보조 합성: 각 V-Unit 에 대해 LLM 을 활용하여 명세를 생성합니다. 이때 **검증기 (Verifier) 의 피드백 (Proof Obligations)**을 활용하여 실패 원인을 진단하고 명세를 개선합니다.
• 세분화된 생성 전략:
  • 호스트 함수: 전제조건 (Precondition) 과 루프 불변식을 생성합니다. (호출 지점 정보를 배제하여 과도한 전제조건 생성을 방지)
  • 피호출 함수: 사후조건 (Postcondition) 만 생성하도록 제한합니다. (전제조건 생성을 금지하여 오탐을 줄이고, 호출자 함수의 검증에 필요한 정보를 제공합니다.)
• 반복적 정제: 생성된 명세의 문법적/의미적 유효성을 검증하고, 실패 시 LLM 에게 피드백을 주어 명세를 수정하는 과정을 반복합니다.
• 가정 (Hypothesis) 관리: 검증이 실패하는 경우 해당 RTE 를 '가정'으로 분류하여 수동 검토 대상 목록에 남기고, 나머지 검증 단위로 진행합니다.

3. 주요 기여 (Key Contributions)

1. 잠재적 RTE 기반 명세 합성 개념 정립: 정적 분석에서 도출된 RTE 어설션을 목표로 삼아 LLM 이 필요한 명세를 효과적으로 생성하도록 유도하는 새로운 패러다임을 제시했습니다.
2. Preguss 프레임워크 개발: 정적 분석과 연역적 검증을 결합하여 1,000 줄 이상의 실제 C 프로그램을 대상으로 RTE-free(런타임 오류 없음) 를 증명할 수 있는 최초의 자동화 방법론을 구현했습니다.
3. 오픈 소스 데이터셋 구축: Preguss 가 생성한 명세와 전문가가 수동으로 작성한 명세로 구성된 실제 C 프로그램 데이터셋을 공개했습니다.
4. 성능 입증: 기존 LLM 기반 접근법 (AutoSpec 등) 을 압도하는 성능을 보여주었으며, 대규모 실용 프로그램에서 80.6% ~ 88.9% 의 수동 검증 노력 감소를 달성했습니다.

4. 실험 결과 (Results)

연구팀은 Frama-C-Problems 벤치마크와 4 개의 대규모 실제 프로젝트 (Contiki, X509-parser, SAMCODE, Atomthreads) 를 대상으로 실험을 수행했습니다.

• 벤치마크 성능 (Frama-C-Problems):
  • Preguss 는 51 개 프로그램 중 **46 개 (79.7%)**를 성공적으로 검증했습니다.
  • 기존 최첨단 방법인 AutoSpec (32.7%) 및 AutoSpecRte (41.8%) 보다 월등히 높은 성공률을 기록했습니다.
  • 특히 배열과 루프가 복합된 복잡한 프로그램에서 Preguss 의 우위가 두드러졌습니다.
• 대규모 프로젝트 적용:
  • SAMCODE (우주선 제어 시스템, 1,280 LoC): 87.9% 의 V-Unit 성공률을 기록했으며, **6 개의 실제 런타임 오류 (초기화되지 않은 변수 접근 등)**를 발견하여 개발팀이 확인했습니다.
  • Contiki (544 LoC), X509-parser (1,199 LoC): 각각 94.7%, 86.6% 의 높은 검증 성공률을 보였습니다.
  • 인간 노력 감소: 기존 수동 검증에 비해 **80.6% ~ 88.9%**의 명세 수정/작성 노력이 절감되었습니다.
• 비용 효율성: LLM 추론 비용은 증가했으나, 이로 인해 절감된 수동 검증 비용이 이를 상쇄하고도 남았습니다.

5. 의의 및 중요성 (Significance)

• 실용적 자동화의 실현: 1,000 줄 이상의 대규모 임베디드 및 시스템 소프트웨어에 대한 형식 검증을 거의 완전히 자동화할 수 있는 가능성을 보여주었습니다.
• 정밀한 오류 탐지: 단순히 명세를 생성하는 것을 넘어, 정적 분석의 어설션을 기반으로 실제 버그 (RTE) 를 식별하고, 오탐을 제거하는 능력을 입증했습니다.
• 확장성: LLM 의 컨텍스트 제한을 극복하기 위한 '분할 정복' 및 '세분화된 명세 생성' 전략은 향후 더 복잡한 소프트웨어 검증에도 적용 가능한 중요한 방법론적 통찰을 제공합니다.
• 안전성 확보: 우주선 제어 시스템과 같은 안전 필수 (Safety-critical) 분야에서 실제 오류를 발견하고 검증함으로써 형식 방법론의 실용적 가치를 높였습니다.

결론적으로, Preguss 는 LLM 의 한계를 정적 분석의 강점과 결합하여 극복하고, 대규모 프로그램의 런타임 오류 없는 검증을 위한 새로운 표준을 제시한 획기적인 연구입니다.