Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators

이 논문은 LLM 을 활용해 문법 규칙을 추출하고 재사용 가능한 생성기를 합성하여 구문 오류를 방지하고 실행 비용을 절감하면서도 Z3 와 cvc5 같은 주요 SMT 솔버에서 43 개의 버그를 발견한 'Once4All'이라는 새로운 스켈레톤 기반 퍼징 프레임워크를 제안합니다.

핵심

🧩 "한 번에 모두 해결" (Once4All): SMT 솔버를 위한 AI 기반 버그 사냥꾼

이 논문은 SMT 솔버(Satisfiability Modulo Theory Solver) 라는 복잡한 소프트웨어를 더 튼튼하게 만들기 위해 개발된 새로운 기술, Once4All에 대해 설명합니다.

이걸 이해하기 쉽게 일상적인 비유로 풀어보겠습니다.

---

1. 배경: SMT 솔버란 무엇일까요?

비유: "초고급 수학 문제 해결사"
SMT 솔버는 컴퓨터가 복잡한 논리 문제 (예: "A 가 참이고 B 가 거짓일 때 C 는 어떻게 될까?") 를 자동으로 풀어주는 프로그램입니다. 이 프로그램은 자율주행차, 보안 시스템, 소프트웨어 검증 등 아주 중요한 곳에 쓰입니다.
하지만 이 '해결사'에게도 실수가 있을 수 있습니다. 만약 이 해결사가 잘못된 답을 내놓으면, 그 위에 지어진 모든 시스템이 무너질 수 있습니다. 그래서 우리는 **버그 **(오류)를 찾아내야 합니다.

2. 문제점: 기존 방법들의 한계

기존에는 두 가지 방식으로 버그를 찾았습니다.

1. 규칙대로 만들기: 사람이 직접 규칙을 정해 문제를 만들어냈는데, 새로운 기능이 생기면 규칙을 다시 짜야 해서 귀찮았습니다.
2. **AI **(LLM) 최근엔 AI 에게 "문제 만들어줘"라고 했더니, **반은 엉터리 **(문법 오류)가 나왔고, 매번 AI 에게 물어보는 데 시간과 돈이 너무 많이 들었습니다.

핵심 문제: AI 가 만든 문제가 너무 엉망이라서 쓸모가 없거나, AI 를 계속 부르는 게 너무 비쌉니다.

3. 해결책: Once4All 의 혁신적인 아이디어

저자들은 **"AI 에게 문제를 직접 만들게 하지 말고, 문제를 만드는 '공장'을 만들게 하라"**는 아이디어를 냈습니다.

🏭 비유: "레시피 책 vs 요리사"

• **기존 방식 **(AI 직접 생성) 매번 AI 에게 "오늘 뭐 먹지?"라고 물어보면, AI 가 매번 엉뚱한 메뉴를 추천합니다. (문법 오류 많음, 비용 큼)
• **Once4All 방식 **(생성기 제작) AI 에게 "이 요리의 **레시피 **(문법)를 정리하고, 그 레시피대로 **요리사 **(생성기)를 만들어줘"라고 한 번만 시킵니다.
  • 이 **요리사 **(생성기)는 이제 AI 와 대화할 필요 없이, 스스로 규칙에 맞는 맛있는 요리 (올바른 문제) 를 무한히 만들어냅니다.
  • 한 번 투자, 영원한 수익: AI 와 대화하는 비용은 딱 한 번만 들면 됩니다.

4. 작동 원리: "뼈대 (Skeleton)"를 활용한 변형

Once4All 은 두 단계로 작동합니다.

**1 단계: AI 가 요리사 **(생성기)

• AI 가 솔버의 설명서 (문서) 를 읽고, 각 이론 (수학, 문자열 등) 에 맞는 **문법 규칙 **(CFG)을 자동으로 정리합니다.
• 그 규칙을 바탕으로 **올바른 문제를 만드는 Python 코드 **(생성기)를 작성하고, 스스로 오류를 수정하며 완벽하게 다듬습니다.

2 단계: 뼈대 (Skeleton) 에 살을 붙이기

• 비유: 이미 존재하는 훌륭한 요리 (실제 버그가 발생했던 문제) 에서 **재료 **(핵심 부분)만 빼내고 **뼈대 **(구조)만 남깁니다.
  • 예: (A 가 참이고 B 가 거짓일 때) → (A 가 참이고 <여기에 새로운 재료>일 때)
• 이제 1 단계에서 만든 **요리사 **(생성기)가 만든 새로운 재료를 그 빈자리에 채워 넣습니다.
• 이렇게 만들어진 새로운 문제를 여러 개의 솔버에 던져보고, **결과가 다르면 **(예: 하나는 "해결됨", 다른 하나는 "해결 안 됨"이라고 하면) 거기서 버그를 발견한 것입니다.

5. 성과: 얼마나 잘했나요?

이 방법은 놀라운 성과를 냈습니다.

• 43 개의 실제 버그 발견: Z3 와 cvc5 라는 두 가지 유명한 솔버에서 43 개의 버그를 찾아냈고, 개발자들이 40 개를 이미 고쳤습니다.
• 새로운 기능도 잡았다: 기존에는 못 찾던 최신 기능이나 특수한 기능에서 숨어있던 버그도 찾아냈습니다.
• 효율성: 기존 방법들보다 더 많은 코드를 테스트했고, AI 와 대화하는 비용은 획기적으로 줄였습니다.

6. 요약: 왜 이 연구가 중요한가요?

이 논문은 **"AI 를 무작정 부르는 게 아니라, AI 가 만든 '도구'를 활용하라"**는 교훈을 줍니다.

• 한 번의 노력으로 영구적인 해결: AI 와의 대화 비용을 줄이면서도, 새로운 소프트웨어 기능에 빠르게 적응할 수 있습니다.
• 튼튼한 시스템: 우리가 매일 쓰는 소프트웨어와 시스템의 안전을 지키는 데 큰 도움이 됩니다.

결론적으로, Once4All 은 AI 를 이용해 소프트웨어의 '결함'을 찾아내는 가장 똑똑하고 효율적인 사냥꾼이 된 것입니다. 🕵️‍♂️🔍

기술 요약

1. 문제 정의 (Problem)

SMT (Satisfiability Modulo Theory) 솔버는 심볼릭 실행, 자동 검증 등 현대 소프트웨어 시스템의 핵심 구성 요소입니다. 그러나 솔버의 결함은 심각한 보안 취약점으로 이어질 수 있어, 고품질의 테스트 공식을 통한 버그 발견이 필수적입니다. 기존 테스트 기법들은 다음과 같은 한계를 겪고 있습니다:

• 진화하는 기능에 대한 대응 부족: SMT-LIB 표준과 솔버별 확장 기능 (예: cvc5 의 Set, Bag 이론 등) 이 빠르게 진화함에 따라, 수동으로 설계된 생성 규칙이나 뮤테이션 전략은 새로운 기능을 효과적으로 테스트하지 못합니다.
• LLM 기반 접근법의 한계: 최근 대규모 언어 모델 (LLM) 을 활용한 직접적인 공식 생성 연구가 등장했으나, 생성된 공식의 약 50% 가 문법적으로 유효하지 않으며 (syntactically invalid), LLM 과의 반복적 상호작용으로 인한 높은 계산 오버헤드가 존재합니다.

2. 방법론 (Methodology)

저자들은 Once4All이라는 새로운 LLM 보조 퍼징 (Fuzzing) 프레임워크를 제안합니다. 이 프레임워크는 LLM 을 사용하여 직접 공식을 생성하는 대신, 재사용 가능한 생성기 (Generators) 를 합성하고 이를 기존 공식의 구조적 뼈대 (Skeleton) 에 적용하는 방식을 취합니다.

핵심 단계:

1. LLM 보조 생성기 구축 (LLM-Assisted Generator Construction):

   • CFG 추출: LLM 을 활용하여 SMT-LIB 표준 문서 및 솔버별 확장 이론 (Z3, cvc5 등) 에 대한 문맥 자유 문법 (CFG) 을 자동으로 추출하고 요약합니다.
   • 생성기 합성: 추출된 CFG 를 기반으로 LLM 이 각 이론에 맞는 재사용 가능한 부울 항 (Boolean terms) 생성기를 Python 코드로 합성합니다.
   • 자기 수정 (Self-Correction): 생성된 생성기가 문법적으로 유효한 공식을 생성하는지 검증합니다. 솔버 (Z3, cvc5) 를 통해 파싱 오류를 확인하고, 오류 메시지를 LLM 에게 피드백하여 생성기 코드를 수정하는 과정을 반복합니다. 이는 일회성 투자로, 문법이 변경될 때만 반복됩니다.

2. 뼈대 유도 뮤테이션 (Skeleton-Guided Mutation):

   • 뼈대 추출: 기존 시드 (Seed) 공식에서 원자적 부분 공식 (Atomic sub-formulas) 을 제거하여 <placeholder> 가 포함된 구조적 뼈대 (Skeleton) 를 추출합니다.
   • 항 채우기: 앞서 구축된 LLM 생성기를 통해 다양한 이론에 부합하는 새로운 부울 항을 생성합니다.
   • 합성 및 테스트: 생성된 항을 뼈대의 플레이스홀더에 채워 새로운 테스트 공식을 만듭니다. 이때 생성된 항의 타입 (Sort) 이 뼈대의 변수와 호환되도록 조정합니다.
   • 차등 테스트 (Differential Testing): 생성된 공식을 여러 솔버 (또는 다른 버전의 솔버) 에 입력하여 결과 (sat/unsat) 나 크래시 여부를 비교하여 버그를 탐지합니다.

3. 주요 기여 (Key Contributions)

• 혁신적 접근법: 뮤테이션 기반 퍼징의 높은 처리량과 LLM 의 맥락 이해 능력을 결합하여, 솔버의 진화하는 기능에 자동으로 적응할 수 있는 새로운 퍼징 패러다임을 제시했습니다.
• 실용성 및 확장성: SMT-LIB 표준과 솔버별 확장 이론을 모두 아우르는 생성기를 자동으로 구축하는 도구를 구현했습니다.
• 성능 입증: Z3 와 cvc5 두 가지 주요 솔버에서 45 개의 버그 리포트를 생성하여, 이 중 43 개가 개발자에 의해 확인되었고 40 개가 수정되었습니다. 특히 기존 퍼저가 발견하지 못했던 새로운 이론 및 솔버별 확장 기능 관련 버그를 다수 발견했습니다.
• 코드 커버리지 향상: 기존 최첨단 퍼저 (HistFuzz, OpFuzz 등) 대비 더 높은 코드 커버리지를 달성했습니다.

4. 실험 결과 (Results)

• 버그 발견: Z3 와 cvc5 에서 총 45 개의 버그를 보고했으며, 43 개가 확인되었습니다. 발견된 버그 유형은 크래시 (35 개), 잘못된 모델 (6 개), 정합성 오류 (4 개) 로 분류되었습니다.
• 장기적 버그 발견: 일부 버그는 6 년 이상 잠복해 있던 것으로 확인되었으며, 특히 최근 추가된 이론 (Finite Field, Set 등) 에서 발생한 버그를 효과적으로 찾아냈습니다.
• 코드 커버리지: 24 시간 실험 결과, Once4All 은 Z3 와 cvc5 모두에서 기존 퍼저들보다 더 높은 라인 및 함수 커버리지를 달성했습니다. 특히 cvc5 의 솔버별 확장 이론 (예: Set 이론) 관련 코드를 다른 퍼저는 전혀 커버하지 못했으나 Once4All 은 이를 테스트했습니다.
• 성분 분석 (Ablation Study):
  • 뼈대 (Skeleton) 의 중요성: 뼈대 없이 생성기만 사용하는 변형 (Once4Allw/oS) 은 커버리지와 버그 발견 능력이 현저히 떨어졌습니다. 이는 기존 공식의 구조가 솔버의 깊은 로직을 탐색하는 데 필수적임을 보여줍니다.
  • LLM 선택의 영향: GPT-4, Gemini, Claude 등 다른 LLM 을 사용해도 성능 차이가 미미하여 프레임워크가 LLM 선택에 민감하지 않음을 입증했습니다.

5. 의의 (Significance)

• 소프트웨어 테스트의 새로운 패러다임: LLM 을 직접적인 입력 생성기가 아닌, 테스트 생성 로직 (Generator) 을 합성하는 도구로 활용함으로써, LLM 의 환각 (Hallucination) 문제를 줄이고 계산 비용을 획기적으로 절감했습니다.
• 진화하는 시스템 테스트: SMT 솔버처럼 기능이 빠르게 추가되는 시스템에 대해, 수동 규칙 업데이트 없이도 문서 기반으로 자동으로 테스트 능력을 확장할 수 있음을 증명했습니다.
• 일반화 가능성: 이 접근법은 컴파일러, 인터프리터 등 문법 기반 또는 템플릿 기반 테스트가 필요한 다른 소프트웨어 시스템에도 적용 가능한 잠재력을 가지고 있습니다.

요약하자면, Once4All 은 LLM 의 생성 능력을 효율적으로 활용하면서도 문법적 유효성을 보장하는 하이브리드 접근법을 통해, SMT 솔버의 신뢰성을 높이는 데 있어 기존 기법들을 압도하는 성과를 거두었습니다.