💻 computer science

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

이 논문은 SMT 솔버의 정밀한 전역 추론 능력을 유지하면서 LLM 을 선택적으로 활용하여 난해한 코드 조각을 해결하는 경량 고스트 코드를 생성하는 하이브리드 심볼릭 실행 프레임워크 'Gordian'을 제안하며, 이를 통해 기존 심볼릭 실행 및 LLM 기반 기법 대비 커버리지를 획기적으로 향상시키고 토큰 사용량을 대폭 절감함을 입증합니다.

원저자: Dimitrios Stamatios Bouras, Sergey Mechtaev

게시일 2026-03-23

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Dimitrios Stamatios Bouras, Sergey Mechtaev

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

🕵️‍♂️ 문제: "미로 찾기"와 "수학 천재"의 딜레마

컴퓨터 프로그램을 분석하는 '상징적 실행 (Symbolic Execution)' 기술은 마치 거대한 미로를 탐험하는 것과 같습니다. 이 미로는 수많은 갈래길 (코드 경로) 이 있고, 각 길에는 문이 있습니다. 문은 특정 조건 (예: "숫자가 100 보다 커야 함", "삼각함수 계산 결과가 0.5 이어야 함") 을 만족해야 열립니다.

기존의 수학 천재 (SMT 솔버):
- 이 도구는 매우 정확하고 논리적입니다. "A 길로 가면 B 문이 열리려면 C 조건이 필요하다"라고 완벽하게 계산해냅니다.
- 하지만 약점이 있습니다: 너무 복잡한 수학 문제 (비선형 수학, 삼각함수 등) 나, 데이터 구조가 너무 복잡하면 (예: 연결된 고리 모양의 데이터), "이건 계산이 안 돼!"라고 포기해버립니다. 마치 미로에서 복잡한 수학 공식이 적힌 문을 만나면 멈춰 서는 것입니다.
최근의 AI 탐험가 (LLM 기반 접근법):
- 최근에는 AI 를 이용해 이 문을 직접 뚫으려 했습니다. AI 는 직관과 추론으로 "아마도 이 숫자를 넣으면 문이 열릴 거야!"라고 추측해서 입력값을 만듭니다.
- 하지만 약점이 있습니다: 미로가 너무 깊고 복잡하면, AI 는 앞선 길에서 어떤 조건이 필요했는지 기억하지 못합니다. "이 문은 열렸는데, 저 문은 왜 안 열리지?"라고 혼란을 겪으며, 전체적인 연결고리를 놓쳐버립니다.

💡 해결책: 고르디안 (Gordian) 의 등장

고르디안은 **"수학 천재와 AI 를 팀으로 묶어, 서로의 약점을 보완한다"**는 아이디어입니다. AI 가 직접 미로 전체를 다 탐험하게 하는 대신, 수학 천재가 막힌 곳에서만 AI 의 도움을 받아 '유령 코드 (Ghost Code)'라는 특수 도구를 만들어냅니다.

유령 코드는 프로그램의 실제 기능에는 영향을 주지 않으면서, 분석을 돕는 가상의 보조 장치입니다. 고르디안은 세 가지 전략을 사용합니다.

1. 🔄 "되돌리기" 마법 (역방향 추론)

상황: 미로에서 "삼각함수 계산"이라는 복잡한 문을 통과해야 하는데, 수학 천재는 계산이 안 됩니다.
고르디안의 해결: AI 에게 "이 복잡한 문을 거꾸로 뒤집는 마법 (역함수) 을 만들어줘"라고 요청합니다.
비유: 마치 "열쇠 (결과) 가 주어졌을 때, 어떤 자물쇠 (입력) 를 끼워야 열렸는지"를 역으로 계산하는 것입니다. AI 가 만든 이 '되돌리기 마법'을 사용하면, 수학 천재는 복잡한 계산 없이도 "아, 이 열쇠를 끼우려면 저쪽에서 이런 입력이 필요했구나!"라고 쉽게 길을 찾아갈 수 있습니다.

2. 🎭 "가상 배우" 활용 (대리 모델)

상황: 어떤 문이 너무 복잡해서 수학 천재가 이해할 수 없습니다.
고르디안의 해결: AI 에게 "복잡한 문 대신, 수학 천재가 쉽게 이해할 수 있는 **간단한 가상의 문 (대리 모델)**을 만들어줘. 실제 기능은 똑같지만 계산은 훨씬 쉬워야 해"라고 요청합니다.
비유: 무서운 괴물 (복잡한 코드) 이 지키는 문을 통과할 때, AI 가 그 괴물과 똑같이 생긴 **가짜 괴물 (간단한 모델)**을 만들어서 수학 천재가 그 가짜 괴물과 논리적으로 싸우게 합니다. 가짜 괴물을 이기면, 진짜 괴물도 이긴 것과 같은 효과를 얻습니다.

3. 🗺️ "지도 조각" 나누기 (의미 있는 공간 분할)

상황: 데이터가 너무 복잡하게 얽혀 있어 (예: 고리 모양의 연결 리스트), 미로의 갈래길이 무한히 생겨서 수학 천재가 미쳐버립니다.
고르디안의 해결: AI 에게 "이 복잡한 미로를 **의미 있는 몇 가지 모양 (토폴로지)**으로만 나누어줘"라고 요청합니다.
비유: "고리 모양", "선 모양", "부서진 모양"처럼 데이터의 형태를 몇 가지 카테고리로만 제한합니다. AI 가 "이곳은 고리 모양만 허용한다"라고 가상의 규칙을 세우면, 수학 천재는 무한한 갈래길을 고민할 필요 없이, 유용한 몇 가지 길만 집중적으로 탐험하면 됩니다.

🏆 결과: 왜 이것이 획기적인가요?

이 논문은 실제 실험을 통해 고르디안이 얼마나 강력한지 증명했습니다.

성공률 대폭 상승: 기존 방법으로는 50~60% 만 찾던 숨겨진 길 (코드 경로) 을, 고르디안은 90% 이상 찾아냈습니다.
비용 절감: AI 를 계속 쓰느라 돈 (토큰 비용) 을 많이 쓰는 다른 방법들에 비해, 고르디안은 필요할 때만 AI 를 호출하기 때문에 비용이 90% 이상 줄었습니다.
실제 적용: 단순한 예제뿐만 아니라, 실제 수학 라이브러리나 복잡한 데이터 처리 프로그램에서도 뛰어난 성능을 발휘했습니다.

📝 요약

고르디안은 "AI 가 모든 것을 다 하라"거나 "수학 도구만 믿으라"는 극단적인 접근을 버렸습니다. 대신 **"수학 도구가 막히면, AI 가 그 자리에서만 '유령 도구'를 만들어서 도와주고, 다시 수학 도구가 논리를 이어가게 한다"**는 협업 전략을 취했습니다.

이는 마치 수학 천재가 미로에서 길을 잃었을 때, AI 가 "여기서부터는 이렇게 가면 돼"라고 짧은 메모를 남기고, 천재는 그 메모를 보고 논리적으로 길을 찾아나가는 상황과 같습니다. 덕분에 더 빠르고, 더 정확하며, 더 저렴하게 프로그램의 숨겨진 버그와 문제를 찾아낼 수 있게 되었습니다.

1. 문제 정의 (Problem)

심볼릭 실행은 추상적인 입력으로 코드를 실행하고 논리적 제약 조건을 생성하여 SMT 솔버로 분석하는 강력한 기법이지만, 다음과 같은 근본적인 한계로 인해 실제 적용에 어려움을 겪습니다.

솔버 적대적 (Solver-hostile) 코드 조각: 비선형 산술, 삼각함수, 복잡한 부동소수점 연산 등은 SMT 솔버가 해결하기 매우 어렵거나 불가능한 제약 조건을 생성합니다.
정밀한 모델링의 어려움: 네트워크 통신이나 시스템 호출 등 외부 환경과의 상호작용을 정확하게 모델링하기 어렵습니다.
무제한 힙 (Heap) 구조: 동적 메모리 할당과 포인터 기반 데이터 구조는 경로 폭발 (Path Explosion) 을 유발하여 탐색 가능한 경로의 수를 제한합니다.

최근 LLM 을 솔버 대신 사용하여 이러한 문제를 우회하려는 시도가 있었으나 (예: ConcoLLMic), LLM 은 프로그램의 깊은 실행 경로에서 여러 함수 간의 전역적으로 일관된 제약 조건을 유지하는 데 어려움을 겪어, 실제 대규모 프로젝트 분석에는 한계가 있었습니다.

2. 방법론 (Methodology)

Gordian 은 LLM 을 솔버를 대체하는 것이 아니라, 솔버가 막힌 지점에서만 선택적으로 활용하여 솔버를 돕는 '고스트 코드'를 생성하는 하이브리드 방식을 채택합니다. LLM 은 어려운 코드 조각을 분석하고, 이를 해결하기 위한 세 가지 유형의 고스트 코드를 생성합니다.

3 가지 고스트 코드 유형

코드 역전 (Fragment Inversion):
- 목적: 솔버가 해결하기 어려운 복잡한 연산 (예: 삼각함수) 을 가진 코드 조각을 역방향으로 실행하여 제약 조건을 전파합니다.
- 작동 원리: LLM 이 어려운 함수 $f$ 의 역함수 $f^{-1}$ 을 생성합니다. 심볼릭 실행 시 이 함수를 '고스트'로 대체하고, 후속 경로 (Suffix) 의 제약 조건을 SMT 솔버로 먼저 해결한 후, 역함수를 통해 구체적인 값을 역방향으로 전파하여 전방 경로 (Prefix) 의 입력을 찾습니다. 이를 양방향 제약 전파 (Bidirectional Constraint Propagation) 알고리즘으로 구현합니다.
대리 모델 (Surrogate Modeling):
- 목적: 복잡한 행동을 솔버 친화적인 간소화된 모델로 대체합니다.
- 작동 원리: LLM 이 원본 코드의 핵심 동작을 유지하면서 비트벡터나 선형 산술 등 SMT 솔버가 쉽게 처리할 수 있는 형태로 코드를 재작성한 고스트 코드를 생성합니다. 이는 솔버가 처리하기 힘든 이론 (Theory) 을 피하면서도 관련 행동을 보존합니다.
의미론적 힙 분할 (Semantic Heap Partitioning):
- 목적: 동적 데이터 구조 (예: 링크드 리스트, 트리) 로 인한 경로 폭발을 방지합니다.
- 작동 원리: LLM 이 도메인 지식에 기반하여 힙의 의미 있는 구조 (Topologies, 예: 링 구조, 특정 길이의 리스트) 를 식별하고, 이를 제약하는 고스트 코드를 생성합니다. 이는 무제한적인 힙 공간을 의미 있는 소수의 시나리오로 제한하여 탐색 공간을 줄입니다.

안전성 보장

생성된 모든 고스트 코드는 원본 프로그램에 대한 검증 (Re-execution) 을 거치므로, LLM 의 환각 (Hallucination) 으로 인해 생성된 입력이 실제 프로그램에서 실행 불가능하더라도 심볼릭 실행의 **정합성 (Soundness)**은 유지됩니다.

3. 주요 기여 (Key Contributions)

새로운 접근법: LLM 을 사용하여 SMT 솔버를 보조하는 고스트 코드를 생성함으로써 심볼릭 실행을 강화하는 새로운 하이브리드 프레임워크 (Gordian) 를 제안했습니다.
실용적인 고스트 코드 변형: 역전 (Inversion), 대리 모델 (Surrogate), 의미론적 힙 분할 (Partition) 의 세 가지 구체적인 기법과 이를 생성하는 프롬프트 및 솔버 통합 알고리즘을 제시했습니다.
포괄적인 평가: 합성 벤치마크 (LogicBombs), 수학 라이브러리 (FDLibM), 구조화된 입력 프로그램 (libexpat, jq, bc) 에 대한 광범위한 평가를 통해 기존 심볼릭 실행 및 LLM 기반 기법 대비 우수한 성능을 입증했습니다.

4. 실험 결과 (Results)

Gordian 은 KLEE 심볼릭 실행 엔진 위에 구현되었으며, 다음과 같은 결과를 도출했습니다.

커버리지 향상:
- 전통적 심볼릭 실행 대비: 평균 52~84% 더 높은 커버리지를 달성했습니다.
- LLM 기반 기법 대비: 평균 86~419% 더 높은 커버리지를 달성했습니다.
- 특히 LogicBombs 벤치마크에서는 94.3% 의 논리 폭탄을 트리거하여 기존 최상위 LLM 기반 기법 (ConcoLLMic) 대비 47.1% 향상된 성능을 보였습니다.
- FDLibM (수치 계산 라이브러리) 에서는 기존 KLEE 대비 평균 22.09% 향상, ConcoLLMic 대비 183.5% 향상된 커버리지를 기록했습니다.
LLM 토큰 효율성:
- Gordian 은 LLM 을 전체 실행 경로가 아닌 특정 난관 구간에만 제한적으로 사용하므로, 토큰 사용량이 기존 LLM 기반 기법 대비 90~96% 감소했습니다.
- ConcoLLMic 대비 약 25 배, Cottontail 대비 약 10 배 적은 토큰으로 더 높은 커버리지를 달성했습니다.

5. 의의 및 결론 (Significance)

이 연구는 LLM 의 강력한 코드 생성 및 도메인 지식 활용 능력과 SMT 솔버의 정밀한 전역 제약 조건 해결 능력을 상호 보완적으로 결합한 성공 사례입니다.

실용성: LLM 을 솔버 전체를 대체하는 대신 '도구'로 활용함으로써, LLM 의 환각 문제를 최소화하면서도 실제 대규모 프로젝트 (수치 라이브러리, 파서 등) 에서 심볼릭 실행의 한계를 극복할 수 있음을 입증했습니다.
비용 효율성: LLM 호출 비용을 극도로 줄이면서도 높은 분석 효율을 달성하여, 실제 산업 환경에서의 적용 가능성을 높였습니다.
향후 방향: Gordian 은 현재 외부 오케스트레이터로 작동하지만, 향후 심볼릭 실행 엔진 내부에 네이티브로 통합되어 실시간으로 솔버가 막힌 구간을 감지하고 LLM 을 호출하는 형태로 발전할 수 있을 것으로 기대됩니다.

결론적으로, Gordian 은 심볼릭 실행의 '논리 폭탄'을 해체하고, 복잡한 프로그램 분석의 새로운 표준을 제시하는 중요한 진전입니다.