이 논문은 컴퓨터 프로그램의 거대한 코드 바다에서 **보안 구멍 (취약점)**을 찾아내는 새로운 방법을 소개합니다. 기존 방법들은 너무 느리거나, 너무 많은 거짓 경보를 울려서 실용적이지 못했습니다. 이 연구팀은 정적 분석 (Static Analysis), 대형 언어 모델 (LLM), **기호 실행 (Symbolic Execution)**이라는 세 가지 기술을 결합한 **'세일러 (Sailor)'**라는 시스템을 만들었습니다.
이 시스템을 이해하기 위해 거대한 도서관과 탐험대의 비유를 들어보겠습니다.
🌊 1. 문제: 거대한 도서관의 숨은 위험
컴퓨터 프로그램 (코드) 은 수백만 권의 책이 쌓인 거대한 도서관과 같습니다. 해커들은 이 도서관의 특정 책 한 줄에 숨겨진 '함정'을 찾아내서 도서관을 무너뜨리려 합니다.
기존의 문제점:
정적 분석 (Static Analysis): 도서관의 모든 책 표지를 빠르게 훑어보는 로봇입니다. "이 책에 위험한 단어가 있네!"라고 수천 개를 알려주지만, 대부분은 거짓 경보입니다. (실제로는 안전한데 위험하다고 함)
퍼징 (Fuzzing): 도서관에 무작위로 책장을 넘기거나 종이를 던지는 방법입니다. 깊은 곳에 숨은 함정은 절대 발견하지 못합니다.
기호 실행 (Symbolic Execution): 도서관의 모든 책 내용을 하나하나 논리적으로 분석하는 매우 정밀한 방법입니다. 하지만 도서관이 너무 크고 복잡해서, 어디서부터 시작해야 할지 모르고 (어떤 책이 위험한지 모름), 어떻게 책장을 엽니까? (환경 설정이 어려움) 하는 문제가 있어 혼자서는 불가능했습니다.
🚢 2. 세일러 (Sailor) 의 해결책: 3 단계 항해
세일러는 이 세 가지 기술을 조화롭게 섞어 자동화된 탐험대를 구성했습니다.
📍 1 단계: 정적 분석이 '지도'를 그립니다 (Static Analysis)
비유: 먼저 정적 분석 로봇이 도서관 전체를 빠르게 훑습니다.
역할: "이 책 (코드) 의 2699 페이지에 'memcpy'라는 위험한 단어가 있네! 아마도 여기가 함정일 거야!"라고 후보 지점을 찾아냅니다.
결과: 수만 개의 후보 중에서 "이곳을 집중적으로 조사해라"는 **작업 지시서 (Vulnerability Specification)**를 만듭니다.
🤖 2 단계: AI (LLM) 가 '탐험 장비'를 만듭니다 (LLM-Orchestrated Synthesis)
비유: 이제 **AI(대형 언어 모델)**가 이 지시서를 받습니다. 하지만 AI 는 도서관 전체를 한 번에 볼 수 없기 때문에, 해당 책만 읽을 수 있도록 '가상 도서관'을 짓습니다.
역할:
드라이버 (Driver) 제작: "이 책을 열려면 어떤 열쇠가 필요할까?"라고 생각하며, 책장을 여는 시나리오를 코드로 작성합니다.
스텁 (Stub) 제작: 책과 관련 없는 다른 책들은 모두 '가짜 책'으로 대체하여 혼란을 줄입니다.
반복 수정: AI 가 만든 장비를 컴파일러와 기호 실행 엔진이 테스트합니다. "에라, 이 열쇠는 안 들어가요!"라고 하면, AI 는 "아, 그럼 이 모양으로 고쳐볼게!"라고 수정합니다. 이 과정을 수십 번 반복하며 완벽한 탐험 장비를 완성합니다.
🔍 3 단계: 기호 실행이 '함정'을 확인하고, 실전 테스트를 합니다 (Symbolic Execution & Concrete Validation)
비유: 완성된 장비로 기호 실행 엔진이 책장을 엽니다.
역할:
기호 실행: "만약 이 페이지가 100 이라면? 101 이라면?"처럼 모든 가능성을 논리적으로 따져 **"아! 여기서 책장이 찢어지는 함정이 있네!"**라고 찾아냅니다.
실전 재현 (Concrete Replay): AI 가 만든 가상의 장비를 실제 도서관 (수정되지 않은 원본 코드) 에 적용해 봅니다. "실제로 책이 찢어지나요?" 확인합니다.
결과: 실제로 찢어지면 확정된 취약점으로 인정받습니다.
🏆 3. 놀라운 성과: 왜 세일러가 특별한가?
연구팀은 오픈소스 프로젝트 10 개 (총 680 만 줄의 코드) 로 실험을 했습니다.
기존 방법들의 한계:
가장 강력한 경쟁자 (전체 코드를 볼 수 있는 AI 에이전트) 는 겨우 12 개의 취약점만 찾았습니다.
사람이 직접 장비를 만들어 준 경우 (기존 기호 실행) 는 0 개였습니다. (너무 복잡해서 못 만듦)
세일러의 성과:
379 개의 새로운 취약점을 찾아냈습니다! (경쟁자의 30 배 이상)
이 중 421 건이 실제로 프로그램이 멈추는 (Crash) 증상으로 확인되었습니다.
핵심 통찰: 세 가지 기술 중 하나라도 빼면 실패했습니다.
지도 (정적 분석) 가 없으면 AI 는 어디를 찾아야 할지 몰라 12 배나 적게 찾았습니다.
AI 의 반복 수정이 없으면 장비가 만들어지지 않아 0 개였습니다.
기호 실행이 없으면 논리적 검증이 안 되어 12 개 이상 못 찾았습니다.
💡 4. 결론: 함께하면 더 강력하다
이 논문은 **"혼자서 모든 것을 하려 하지 말고, 각자의 강점을 가진 전문가들을 팀으로 꾸리라"**는 메시지를 줍니다.
정적 분석은 '어디를 볼지' 알려주는 나침반입니다.
**AI (LLM)**는 복잡한 환경을 만들어주는 장비 제작자입니다.
기호 실행은 논리적으로 모든 가능성을 검증하는 검증관입니다.
이 세 가지가 협력하여 '세일러'를 만들자, 인간이 수년 동안 찾아내지 못했던 거대 코드 속의 숨은 위험들을 자동으로 찾아낼 수 있게 되었습니다. 이는 사이버 보안의 미래를 바꿀 중요한 기술입니다.
논문 요약: Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery (Sailor)
이 논문은 대규모 C/C++ 코드베이스에서 취약점을 발견하기 위해 정적 분석 (Static Analysis, SA), 대형 언어 모델 (LLM), **심볼릭 실행 (Symbolic Execution, SE)**을 결합한 자동화 파이프라인인 Sailor를 제안합니다. 기존의 심볼릭 실행 기술이 가진 확장성 문제를 해결하고, LLM 의 코드 생성 능력을 활용하여 정밀한 취약점 탐지를 가능하게 합니다.
1. 문제 정의 (Problem)
대규모 C/C++ 프로젝트에서 자동화된 취약점 탐지는 다음과 같은 한계로 인해 여전히 어려운 과제입니다.
정적 분석 (SA): 수백만 줄의 코드를 스캔할 수 있지만, 오탐 (False Positive) 비율이 매우 높아 신뢰할 수 있는 결과를 내기 어렵습니다.
퍼징 (Fuzzing): 구체적인 입력으로 프로그램을 실행하지만, 복잡한 라이브러리 내부나 정밀한 프로그램 상태가 필요한 깊은 경로를 도달하기 어렵습니다.
심볼릭 실행 (SE): 입력을 심볼릭 값으로 처리하여 경로를 정밀하게 탐색하고, 제약 조건 솔버를 통해 구체적인 실행 Witness 를 생성할 수 있습니다. 그러나 대규모 코드베이스에 직접 적용하기 어렵습니다.
경로 폭발 (Path Explosion): 탐색 깊이가 제한됩니다.
환경 의존성: 시스템 호출, 파일 I/O, 복잡한 라이브러리 API 를 모델링해야 합니다.
하네스 (Harness) 작성의 어려움: SE 엔진이 실행할 수 있도록 진입점 (Entrypoint) 을 설정하고, 불필요한 경로를 스텁 (Stub) 으로 대체하며, 심볼릭 입력을 준비하는 '하네스'를 수동으로 작성해야 합니다. 이는 전문가 지식이 필요하며 확장성의 주요 병목 현상입니다.
LLM 기반 탐지: 최근 LLM 이 취약점 탐지에 적용되고 있지만, 실행 기반의 검증이 없어 존재하지 않는 취약점을 보고하거나 실제 취약점을 놓칠 수 있습니다.
핵심 문제: 대규모 코드베이스에서 심볼릭 실행을 확장 가능하게 적용하기 위해, 자동화된 하네스 생성과 정확한 타겟 선정을 어떻게 해결할 것인가?
2. 방법론: Sailor 파이프라인 (Methodology)
Sailor 는 세 가지 주요 단계를 거쳐 자동화된 취약점 탐지를 수행합니다.
1 단계: 정적 분석 기반 타겟 생성 (Static Analysis Informed Target Generation)
목적: 코드베이스에서 잠재적인 취약점 위치를 식별하고, 심볼릭 실행을 위한 '취약점 명세 (Vulnerability Specification)'를 생성합니다.
과정:
Fact Generation: CodeQL 을 사용하여 34 가지 메모리 안전성 쿼리 (표준 및 커스텀) 를 실행하여 SARIF 형식의 취약점 후보를 찾습니다.
Fact Enrichment: 취약점 위치 주변의 함수 호출, 포인터 변수, 길이 변수, 바운드 힌트, 빌드 컨텍스트 (include 경로 등) 를 추출하여 'Fact Pack'을 구성합니다.
Specification Generation: 추출된 정보를 바탕으로 진입점 (Entrypoint), 어설션 템플릿 (안전성 속성), 필터링 규칙을 포함한 JSON 형태의 취약점 명세를 생성합니다.
효과: 정적 분석이 '어디 (Where)'에 취약점이 있을지 파악하여 LLM 이 탐색할 범위를 좁힙니다.
2 단계: LLM 오케스트레이션 심볼릭 실행 (LLM-Orchestrated Symbolic Execution)
목적: 생성된 취약점 명세를 바탕으로 심볼릭 실행 엔진 (KLEE) 이 실행할 수 있는 하네스 (Driver, Stubs, Assertions) 를 LLM 이 자동 생성하고 반복적으로 개선합니다.
과정 (반복 루프):
소스 탐색 (Source Exploration): LLM 이 프로젝트 소스를 탐색하여 구조체 정의, 함수 시그니처 등을 파악합니다.
하네스 생성 (Harness Synthesis):
Driver: 심볼릭 상태를 설정하고 진입점을 호출하는 main 함수를 생성합니다.
Stubs: 관련 없는 경로를 제거하거나 심볼릭 값으로 대체하는 스텁 코드를 생성합니다.
Assertions: 안전성 속성 (예: 버퍼 오버플로우 방지) 을 인코딩합니다.
피드백 루프 (Refinement Loop):
생성된 코드를 컴파일하고 KLEE 로 실행합니다.
컴파일 오류나 KLEE 의 실행 결과 (경로 도달 여부, 메모리 오류 발생 여부) 를 LLM 에게 피드백합니다.
LLM 은 피드백을 바탕으로 하네스를 수정 (Refine) 합니다. 이 과정은 최대 60 턴까지 반복됩니다.
효과: LLM 이 복잡한 프로젝트 구조를 이해하고, 컴파일러 및 SE 엔진의 피드백을 통해 하네스를 점진적으로 정교화합니다.
3 단계: 구체적 검증 (Concrete Validation)
목적: 심볼릭 실행이 발견한 취약점이 실제 코드에서도 재현되는지 확인하여 오탐을 제거합니다.
과정:
KLEE 가 생성한 구체적인 Witness 입력 (.ktest 파일) 을 추출합니다.
수정되지 않은 원본 프로젝트 소스를 AddressSanitizer (ASan) 로 컴파일합니다.
추출된 Witness 입력을 ASan 이 포함된 바이너리에 재입력 (Replay) 하여 실행합니다.
ASan 스택 트레이스가 프로젝트 소스 내 메모리 안전 위반을 보고하면 '확인됨 (Confirmed)'으로 판정합니다.
효과: LLM 이 생성한 비현실적인 하네스로 인한 오탐을 필터링하고, 실제 취약점임을 100% 보장합니다.
3. 주요 기여 (Key Contributions)
완전 자동화 파이프라인: 정적 분석으로 타겟을 선정하고, LLM 이 하네스를 생성/개선하며, 심볼릭 실행과 구체적 실행으로 검증하는 종단간 (End-to-End) 자동화 시스템을 최초로 제안했습니다.
Sailor 구현: CodeQL, GPT-5 (LLM), KLEE, AddressSanitizer 를 통합하여 수동 하네스 작성이나 프로젝트별 복잡한 설정 없이도 대규모 C/C++ 프로젝트에 적용 가능한 시스템을 구축했습니다.
대규모 평가 및 검증: 10 개의 오픈소스 C/C++ 프로젝트 (총 680 만 줄의 코드) 에서 379 개의 고유한 새로운 메모리 안전 취약점을 발견하고, 421 개의 충돌 (Crash) 을 확인했습니다.
4. 실험 결과 (Results)
성능: 10 개 프로젝트 (6.8M LOC) 에서 379 개의 고유한 새로운 취약점을 발견했습니다. (총 421 개의 확인된 충돌)
비교 대상 (Baselines) 대비 우위:
B1 (수동 하네스 SE): 0 개 발견 (하네스 작성의 어려움과 경로 폭발로 인해 실패).
B2 (LLM 생성 하네스 SE): 0 개 확인 (하네스 컴파일 실패율 81%, 오탐).
B3-B5 (LLM 기반 탐지): 최대 12 개만 확인 (높은 오탐률, 실행 기반 검증 부재).
Sailor:379 개 확인. 가장 강력한 베이스라인 (B5, Claude Opus 4.6 사용) 보다 30 배 이상 많은 취약점을 발견했습니다.
Ablation Study (성분 분석):
정적 분석 (SA) 제거 시: 발견된 취약점이 12.2 배 감소 (379 -> 31).
반복적 LLM 개선 (Iterative Refinement) 제거 시: 확인된 취약점이 0 개로 떨어짐.
심볼릭 실행 (SE) 제거 시: 발견 가능한 취약점이 12 개 이하로 제한됨.
결론: 세 가지 기술 (SA, LLM, SE) 은 상호 보완적이며, 모두 필수적입니다.
5. 의의 및 중요성 (Significance)
확장성 달성: 정적 분석의 확장성과 LLM 의 코드 추론 능력을 결합하여, 수동으로 하네스를 작성할 수 없었던 초대규모 코드베이스 (예: GNU Binutils, 184 만 줄) 에서도 심볼릭 실행을 적용할 수 있게 되었습니다.
정밀도 향상: LLM 의 추론 능력을 활용하되, 심볼릭 실행과 구체적 실행 (ASan) 을 통해 형식적 증명과 실제 재현을 보장함으로써 오탐률을 극도로 낮췄습니다.
실제 취약점 발견: 379 개의 새로운 취약점은 아직 공개되지 않았으며, 해당 프로젝트 유지보수자에게 보고될 예정입니다. 이는 자동화된 보안 도구들이 실제 보안 위협을 해결할 수 있음을 입증합니다.
기술적 통합의 새로운 패러다임: 정적 분석, LLM, 심볼릭 실행을 단순히 나열하는 것이 아니라, 각 단계가 다음 단계의 입력을 최적화하도록 설계된 '오케스트레이션' 구조를 제시했습니다.
이 논문은 자동화된 소프트웨어 보안 테스트 분야에서 LLM 을 활용한 실용적이고 확장 가능한 솔루션의 가능성을 크게 확장시켰다는 점에서 의의가 있습니다.