[Paper] Zorya: 단일 스레드 Go 바이너리의 자동 Concolic 실행

Source: arXiv - 2512.10799v1

Overview

이 논문은 Zorya 라는 콘콜리식 실행 엔진을 소개한다. Zorya는 컴파일된 단일 스레드 Go 바이너리를 자동으로 분석할 수 있다. Go 바이너리를 Ghidra의 P‑Code 중간 표현으로 변환하고, panic을 유발할 수 있는 경로에만 심볼릭 탐색을 집중함으로써, 기존 심볼릭 도구들이 어려워했던 Go 프로그램의 체계적인 취약점 탐지를 가능하게 한다.

Key Contributions

• Go‑specific binary translation: Go 바이너리를 Ghidra P‑Code 로 변환하여 Go 런타임 의미를 보존하고 정확한 분석을 수행한다.
• Panic‑reachability gating: panic 으로 이어질 수 있는 분기를 격리하는 다중 레이어 필터로, 심볼릭 탐색을 33‑70 % 감소시킨다.
• Concrete‑path bug detection: 초기 실행에서 실제로 수행되지 않은 경로에서도 버그를 표시하도록 콘콜리식 실행을 확장한다.
• Function‑mode analysis: Zorya는 main 에서 시작하는 대신任意의 함수(예: 취약한 핸들러)에서 심볼릭 실행을 시작할 수 있어 복잡한 코드베이스에서 최대 100배의 속도 향상을 제공한다.
• Empirical validation: 벤치마크 스위트에 포함된 다섯 개의 알려진 Go 취약점을 모두 탐지하며, 최대 세 개를 놓치는 최첨단 도구들을 능가한다.

Methodology

1. Binary Lifting – 컴파일된 Go 실행 파일을 Ghidra에 입력하면 기계어를 언어에 독립적인 P‑Code IR 로 변환한다. 이 단계에서 Go 고유의 호출 규약, 스택 레이아웃, 런타임 검사(예: 경계 검사, nil‑포인터 검사)를 포착한다.
2. Concolic Execution Engine – Zorya는 실제 입력으로 프로그램을 구체적으로 실행하면서 각 분기에 대한 심볼릭 제약조건을 동시에 구축한다. 구체적으로 선택된 분기와 반대 방향(미선택) 경로를 잠재적 심볼릭 분기로 기록한다.
3. Panic‑Reachability Filtering – 정적 분석을 통해 panic 으로 이어질 수 있는 모든 위치를 식별한다. 심볼릭 탐색 중에는 이러한 panic 지점에 도달할 가능성이 있는 분기만 확장하고 나머지는 버린다.
4. Function‑Mode Entry – 대형 바이너리의 경우, Zorya는 특정 함수(예: HTTP 핸들러)에서 심볼릭 실행을 시작하도록 지시받을 수 있다. 엔진은 구체 실행에서 얻은 컨텍스트(인자, 전역 변수)를 재구성해 불필요한 초기화 코드를 건너뛴다.
5. Bug Reporting – 심볼릭 경로가 panic을 유발하는 조건에 도달하면, Zorya는 해당 크래시를 재현할 수 있는 구체 입력을 추출해 개발자가 문제를 재현하고 수정할 수 있게 한다.

Results & Findings

실험 결과, panic과 관련된 경로에 심볼릭 노력을 집중하면 상태 공간을 크게 줄이면서도 커버리지는 유지할 수 있음을 확인했다. 또한 任意 함수에서 시작할 수 있는 능력은 많은 일반 콘콜리식 프레임워크가 겪는 “초기화 병목”을 해소한다.

Practical Implications

• Go 서비스 보안 감사 – 팀은 Zorya를 CI 파이프라인에 통합해 배포 전 자동으로 panic을 유발하는 버그를 찾아낼 수 있다. 특히 마이크로서비스 환경에서 유용하다.
• 버그 바운티 자동화 – 연구자는 Zorya를 이용해 발견된 panic에 대한 구체적인 익스플로잇 입력을 생성함으로써 취약점 보고서 검증 단계를 가속화할 수 있다.
• 언어 특화 도구 – Go에 특화된 콘콜리식 엔진의 성공은 Rust, Swift 등 풍부한 런타임을 가진 다른 언어에도 유사한 바이너리‑리프팅 + 게이팅 전략이 적용될 수 있음을 시사한다.
• 수동 퍼징 부담 감소 – 무관한 분기를 가지치기함으로써 Zorya는 퍼저와 보완적으로 작동해 CPU 사이클을 절감하고 더 깊은 커버리지를 달성한다.

Limitations & Future Work

• 단일 스레드에 국한 – 현재 Zorya는 단일 스레드 바이너리만 처리한다. Go의 goroutine 모델을 지원하려면 복잡한 스케줄링 및 동기화 모델링이 필요하다.
• Ghidra 의존성 – 변환 파이프라인은 Ghidra의 P‑Code 정확도에 의존한다. Go 런타임 지원에 빈틈이 있으면 버그를 놓칠 수 있다.
• 매우 큰 코드베이스에 대한 확장성 – 함수‑모드가 초기화 비용을 완화하지만, 수많은 내보낸 함수가 있는 초대형 바이너리는 여전히 성능 이슈를 야기할 수 있다.
• 향후 방향 – 저자들은 (1) 다중 스레드 콘콜리식 지원 추가, (2) 경로를 추가로 가지치기 위한 경량 타인트 분석 통합, (3) 프레임워크를 오픈소스화해 커뮤니티가 Go 런타임 기능을 확장하도록 하는 것을 계획하고 있다.

Authors

• Karolina Gorna
• Nicolas Iooss
• Yannick Seurin
• Rida Khatoun

Paper Information

• arXiv ID: 2512.10799v1
• Categories: cs.SE, cs.PL
• Published: December 11, 2025
• PDF: Download PDF