보안/논문 리뷰

[논문 정리] FUZZOLIC: Mixing fuzzing and concolic execution

pumisj 2026. 4. 28. 07:41

서론

이번에 Fuzzolic을 공부하게 되었다.

Fuzzolic은 Fuzzer와 Symbolic execution을 합친 hybrid concolic executor로 AFL++같은 퍼저의 방식을 일부 채용하면서 symbolic execution의 방법론을 따르는 기법이다.

이번 글에서는 Fuzzolic의 아키텍처, 구현 방식에 대해 정리해보았다.

참고 자료

Borzacchiello, L., Coppa, E., & Demetrescu, C. (2021). FUZZOLIC: Mixing fuzzing and concolic execution. Computers & Security, 108, 102368.

Introduction

소프트웨어를 자동으로 분석하는 기법의 양극단에는 coverage-guided fuzzing과 symbolic execution이 있다.

SE의 변형인 concolic execution은 퍼저와 유사하게 branch condition을 수집하며 한 방향으로 탐색을 진행한다.

조건을 부정하여 다른 길을 탐색하는 방법은 퍼저보다 실행 속도는 느리지만, solver를 이용하여 실행 자체를 더 적게할 수 있다.

이런 퍼징과 SE을 결합한 hybrid fuzzing은 심볼릭 실행의 확장성으로 인해 일반 퍼징보다 더 느리다. 따라서 탐색중 심볼릭 실행 속도를 높히는 것이 중요하다

concolic exploration은 다음 두 단계로 이루어진다

emulation
- 프로그램을 실행하며 symbolic expression과 query들을 수집하는 단계
reasoning
- executor가 해당 query들을 최적화하고 SMT solver을 통해 심볼릭 인풋을 만족시킬 수 있는 값을 찾아내 새로운 인풋을 만들어내는 단계
- 여기서 만들어진 인풋값은 coverage-guided fuzzer의 입력값으로 쓰인다

이 논문에서는 emulation, reasoning 두 단계의 성능을 높히는 시도를 했다.

emulation 단계에서는 새로운 QEMU에서 실행되는 concolic framework인 fuzzolic을 만들었으며, reasoning 단계에서는 기존 SMT solver의 높은 비용문제를 해결하기 위해 mutation을 이용한 solver인 Fuzzy-SAT을 만들었다.

Fuzzy-SAT의 잠재력을 입증하기 위해 해당 기능을 바이너리 기반 concolic framework인 Fuzzolic, QSYM과 소스코드 기반 concolic excutor인 SYMCC에 통합했다.

실험은 다음과 같이 요약될 수 있다

Fuzzolic의 심볼릭 표현과 쿼리를 만드는 효율성을 평가하여 그 성능을 바이너리 코드를 분석하는 QSYM과 SYMQEMU와 비교했으며, 또한 최근 릴리즈된 소스코드가 필요한 concolic 실행기인 SYMCC와도 비교했다.
Fuzzy-SAT와 SMT 솔버인 Z3 그리고 근사 솔버인 JFS를 QSYM이 만든 쿼리로 비교했다. 그 결과 fuzzy-sat은 속도와 해결 효율성 측면에서 좋은 trade off를 보여준다. (성능이 좋음)
fuzzyolic과 fuzzy-sat를 다른 최신 퍼징 도구들과 비교해봤을때, 다른 퍼저들보다 더 높은 코드 커버리지를 달성했고 실제로 리눅스 배포버전에서 취약점을 발견했다.

Background

concolic execution

concolic 실행의 문제는 한 인풋에 대한 탐색이 끝났을 때 다른 실행으로 분석을 다시 시작해야한다는 것이다.

QSYM은 심볼릭 상태만 유지하고 구체적인 상태는 CPU에 맡겨 프로그램의 실행 시간을 줄이는 DBI 방법을 사용했다.

최근에는 QSYM에서 에뮬레이팅 시간을 더 줄이는 source-based instrumentation 접근방식으로 발전시킨 SYMCC와, 바이너리 코드를 분석하는 SYMQEMU도 있다.

approximate constraint solving

path constraint가 너무 복잡해서 새로운 경로 조건이 추가됐을 때 해가 없거나 추론하기에 시간이 부족한 경우가 있다. QSYM은 이 경우 앞선 path constraint를 무시하고 오로지 이번 제약 조건만 만족하는 해를 찾는 optimistic solving 방식을 사용한다.

hybrid fuzzing

커버리지 기반 grey-box fuzzing 퍼저는 어떠한 상수값(magic number)을 체크하는 로직이 있을 때 무작위로 이를 넘어가기 힘들다.

이를 해결하기 위해 퍼징과 심볼릭 실행을 결합한 hybrid fuzzing이 등장했다.

Efficient generation of symbolic queries

심볼릭 실행은 hybrid fuzzing으로 사용될 때 매우 효율적이다. 하지만 하나의 경로를 분석하는 오버헤드가 너무 커서 이 방식을 확장하기 힘들다.

이 섹션에서는 Fuzzolic의 내부 작동 원리를 제시하며, symbolic expression과 쿼리를 생성하기 위한 방식을 살펴보고자 한다

Architecture

해당 아키텍처가 달성하고자 하는 목표는 다음과 같다

Deployability
- fuzzolic은 심볼릭 실행을 하는데 소스코드를 필요로 하지 않는다.
- 동적 바이너리 번역기인 QEMU를 사용하기 때문에 다양한 어플리케이션과 상용 소프트웨어를 대상으로 바이너리 코드를 분석하고 실행할 수 있다.
Efficiency
- fuzzolic은 런타임중에 symbolic expression과 branch query를 빌드하기 위해 QEMU를 활용하여 instrumentation 코드를 삽입하는 Just-In-Time (JIT) compilation을 활용한다.
- 콘콜릭 실행의 JIT compilation는 이미 QSYM에 적용되었으며, 주어진 기계어에 대해서 interpretation방식으로 symbolic expression을 만드는 성능보다 뛰어나다는걸 보여줬다.
Decoupling
- fuzzolic은 symobolic expression을 생성하는 QEMU기반 컴포넌트(tracer)로부터 이 수식을 분석하여 해를 찾는 컴포넌트(solver)을 분리했다.
- 왜 이렇게 했냐면 QEMU같은 DBT 프레임워크가 분석을 할 때 사이드 이팩트를 만들어낼 것 같은 외부 라이브러리 (Z3 solver같은거)를 사용하지 못하도록 했기 때문이다.
- fuzzolic은 이미 설계에서 저런 제약을 견딜 수 있도록 tracer와 solver를 분리해놨다
- tracer는 QEMU에서 돌아가면서 symbolic expression과 쿼리를 간략하게 표현해 solver도 사용할 수 있는 두 개의 공유 메모리에 저장한다.
- solver는 이 수식을 Z3 언어로 변환하고 solver 백엔드에 전달하여 새로운 인풋을 만들어낸다.
Portability and extensibility
- fuzzolic은 호환성이 좋은 QEMU를 기반으로 하고있기 때문에 다른 시스템으로 이식될 수 있다.
- 실제로 플랫폼 독립적인 QEMU에 사용되는 TCG intermediate representation(IR)를 분석했다
- 또한 하나의 어플리케이션의 범주를 넘어 OS를 에뮬레이팅할 수 있게 확장될 수 있다.

Just-in-time-binary instrumentation

fuzzolic의 핵심 요소는 tracer다.

다음은 QEMU가 바이너리 어플리케이션을 실행하는 흐름도다.

다음 basic block을 실행할 때 이미 그 기계어가 캐싱이 안되어있다면 해당 블럭은 처음 실행되었다는 뜻이므로 B단계로 넘어가고 아니면 C단계로 넘어간다
basic block을 컴파일하고 JIT 캐시에 저장한 뒤 C단계로 넘어간다
QEMU는 basic block의 기계어를 실행하고 다음 basic block의 주소를 가져와 다시 A단계로 이동한다. 단, 이 단계에서 시스템 콜이 실행되면 QEMU는 현재 블럭을 실행하기 전에 OS와 상호작용한다.

symbolic expression과 쿼리를 생성하는 instrumentation은 컴파일 단계에서 이루어지기 때문에 실행중에 그것들을 생성하는 ANGR이나 KLEE와는 다르게, fuzzolic은 분석 작업의 일부를 basic block 실행에서 컴파일 시간으로 옮겨질 수 있다.

fuzzolic에 의해 추가된 심볼릭 인스트루멘테이션은 두 가지 형태로 나뉜다

Inline-only instrumentation
basic block에 하나 이상의 TCG 명령어가 있다면, fuzzolic은 외부 함수 호출 없이 symbolic state를 조작하는 코드를 삽입한다

예를 들어 64비트 주소를 rax에서 rbx로 옮기는 명령어가 있다고 해보자

movq %rbx, %rax

이를 QEMU에서 실행할 수 있게 TCG IR로 변환하면 다음과 같다

mov_i64 tcg_reg_2, tcg_reg_1

여기서 fuzzolic은 심볼릭 표현을 추적할 수 있도록 tcg_reg_2와 tcg_reg_1을 추적하는 레지스터를 추가한다.

mov_i64 tcg_reg_symbolic_2, tcg_reg_symbolic_1
mov_i64 tcg_reg_2, tcg_reg_1

이렇게 할 경우 tcg_reg_2의 값이 어디서부터 유래했는지 tcg_reg_symbolic_2를 통해 확인할 수 있다.

Helper-based instrumentation

basic block에 하나 이상의 TCG 명령어가 있다면, fuzzolic은 미리 정의한 helper 함수를 호출함으로써 symbolic state를 조작하는 코드를 삽입한다.

예를 들어 위의 명령어는 다음과 같이도 인스트루멘테이션될 수 있다.

call fuzzolic_move_reg        # helper
            $0x0, $0,               # flags
            tcg_reg_symbolic_1,     # arg 1
            tcg_reg_symbolic_2_id   # arg 2
mov_i64 tcg_reg_2, tcg_reg_1  # original code

해당 코드는 똑같이 tcg_reg_symbolic1에서 tcg_reg_symbolic_2로 심볼릭 표현의 주소를 전달하는 역하을 하지만 fuzzolic_move_reg라는 함수를 호출하여 구현된다.

inline-only instrumentation은 외부 코드를 호출하지 않기 때문에 효율적이지만, 복잡한 연산을 처리할 때 에러를 일으킬 가능성이 높고, 제대로 작동하기 위해서는 분기 코드를 포함하지 않아야한다.

Analysis modes

fuzzolic은 세 가지 분석 모드를 지원한다.

A모드
- 심볼릭 인스트루멘테이션을 하지않고, 따라서 새로운 심볼릭 표현을 만들거나 분기 쿼리를 solver에 전달하지도 않는다.
- 이 모드는 실제 값이 있는 데이터를 처리하는 베이직 블럭, 또는 잘 알려져있는 함수(예를 들어 strcmp)를 처리할 때 사용된다.
B모드
- B모드는 베이직 블록이 심볼릭 상태에 미치는 side effect를 추적하기 위해 심볼릭하게 인스트루멘테이션 되는데, 단 코드 커버리지에는 별로 중요하지 않은 블럭을 처리하도록 설계되었다.
- 이 모드는 fuzzolic이 메인 프로그램에 대한 코드커버리지를 증가시키는 인풋을 생성할 때 사용하지만, 표준 라이브러리 실행에 대해서 테스트하는건 아니다.
- 예를 들어 realloc 함수의 side effect는 추적을 해야하지만, 이 함수의 커버리지를 높힐 필요는 없다
C모드
- 중요한 basic block을 처리할 때 사용되며 심볼릭 인스트루멘테이션과 브랜치 쿼리를 모두 생성한다.

런타임중에 세 분석 모드를 관리하기 위해서 fuzzolic은 두 개의 JIT 캐시를 사용한다.

하나의 캐시는 인스트루멘테이션이 없는 basic block을 저장하도록, 다른 하나는 인스트루멘테이션이 된 basic block을 저장하도록 사용된다.

같은 함수라도 콘크리트값만 있는 프로그램의 시작부분과, 심볼릭 수식이 삽입된 후에 시작부분이 다시 실행될 수 있으므로 하나의 basic block은 두 개의 JIT 캐시에 저장될 수 있다.

세 개의 모드는 자동적으로 전환되는데, A모드는 프로그램의 시작부터 계산에 심볼릭 데이터를 추가하는 시스템 콜을 호출할때까지 실행되며, 그 뒤에는 모두 C모드로 실행하고 특정 경우에만 A, B 모드로 전환된다.

특정 경우라 함은 A모드의 경우 라이브러리 함수를 사용할 때 미리 정의한 API 모델이 있다면 호출되고, API 모델이 없다면 B모드를 실행한다. 두 경우 모두 함수가 끝나면 다시 C모드로 돌아온다.

Interaction between tracer and solver

fuzzolic은 두 개의 컴포넌트로 이루어져있으며, 두 개의 컴포넌트는 expression pool과 query pool 두 개의 공유 메모리를 사용하여 데이터를 주고받는다.

tracer
- tracer는 QEMU 기반의 컴포넌트로 프로그램을 분석하여 심볼릭 표현과 쿼리를 두 개의 메모리에 생성한다
- solver에서 메모리 사용량을 최소화하고 parsing 처리를 쉽게 하기 위해서 심볼릭 표현과 쿼리를 두 개의 최적화된 C 구조체로 표현한다.
solver
- solver frontend
  - 프론트엔드에서는 쿼리 풀에 새로운 쿼리가 들어오면 쿼리에 포함된 모든 표현을 번역하여 Z3 쿼리로 번역한다.
  - 번역된 쿼리는 몇몇 최적화를 거쳐서 solver backend로 보내진다
- solver backend
  - 백엔드의 요소는 FUZZY-SAT이나 Z3가 될 수 있으며 해당 쿼리를 만족시키는 값을 추론한다.
  - 이렇게 찾아낸 식은 fuzzolic이 새로운 인풋을 만드는데에 사용된다
solver는 tracer와 동시에 실행되며 두 개의 서브 컴포넌트로 나뉜다

프로그램 실행 분석이 끝나면 tracer는 풀에 새로운 쿼리가 없음을 의미하는 fack query를 보내고, 남은 쿼리를 모두 처리한 뒤에 종료된다.

Hybrid fuzzing setup

하이브리드 퍼징은 심볼릭 탐색을 수행하는 인스턴스 fuzzolic 한 개와 서로 다른 실행 설정으로 구성된 coverage-guided fuzzer 두 개로 이루어진다.

fuzzer중 하나는 master, 하나는 slave로 명명되며 fuzzolic인스턴스는 아무 coverage-guided fuzzer와 호환된다.

대부분의 퍼저가 공통적으로 제공하는 동기화 절차를 통해 퍼저가 자신의 입력 큐를 파일 시스템상에 유지하게 하여 병렬로 실행중인 다른 퍼저들이 접근할 수 있도록 하고, 다른 퍼저들의 입력 큐와 주기적인 동기화를 수행한다.

따라서 다른 퍼저들에서 만들어낸 코드커버리지를 증가시키는 인풋을 자신도 사용할 수 있도록 한다.

fuzzolic은 slave 퍼저의 인풋 큐에서만 인풋을 가져오는데, 이는 slave가 결국 master의 인풋을 모두 가지고있기 때문에 중복 계산을 피하기 위해서이다.

concolic 실행기는 루프와 같이 이미 실행한 분기 명령어를 만날 때 반복적인 연산을 줄이기 위해서 현재 명령어와 이전 심볼릭 분기 명령어를 해싱하여 bitmap에 저장한다.

현재 명렁어와 이전 심볼릭 분기 명령어를 해싱하는 이유는 해당 분기문의 호출 문맥을 고려하기 위해서이다.

이렇게 할 경우 fuzzolic은 분기문에 도달했을 때 해당 해시값이 bitmap에 이미 있으면 쿼리를 스킵하고 없다면 쿼리를 solver에 전달하고 bitmap을 업데이트할 수 있다.

Efficient solving of symbolic query

최근의 커버리지 가이드 퍼저들은 단순히 코드 커버리지를 늘리는걸 넘어서 프로그램의 동작을 바탕으로 인풋을 새로 만들어낸다.

콘콜릭 실행기는 설계상 심볼릭 표현같이 프로그램 동작에 대한 정확한 묘사를 구축하지만, 전적으로 비용이 많이 드는 SMT solver를 이용하며 이 솔버는 보통 black box로 취급된다.

본문에서는 콘콜릭 실행기가 심볼릭 표현으로부터 학습하고 이를 바탕으로 간단하지만 빠른 인풋 변환을 구현함으로써 SMT solver에 의존하지 않고 쿼리를 풀어낼 수 있음을 보인다.

핵심 아이디어는 다음과 같다

주어진 쿼리 $\neg b \wedge \pi$ 에서 인풋 $i$는 콘콜릭 탐색에 의해서 $\pi$를 만족시킨다. 따라서 $\neg b$와 $\pi$를 만족하도록하는 새로운 테스트케이스 $i'$를 찾는걸 목표로 한다.

Reasoning primitives for concolic execution

SMT솔버는 보통 다앙한 응용 맥락에서 적용되어 방정식을 풀 수 있는 solving primitive를 제공하는데, QSYM, FUZZOLIC, SymCC같은 concolic 실행기에서는 필수적인 primitive만 제공한다.

Fuzzy-SAT은 다음 primitive를 가지고있다.

Solve($e, π , i, opt$)
- $e \wedge \pi$를 만족하는 입력값을 찾아 리턴하는 기능이다.
- $e$는 현재 분기 조건인 b를 뒤집은걸 의미한다. 즉 $e = \neg b$이다.
- opt 플래그는 입력값을 찾는데 실패했을 경우 optimistic solving을 수행할지 여부를 나타낸다.
SolveMax($e, π , i$) / SolveMin($e, π , i$)
- $\pi$를 만족하면서 $e$를 최대 또는 최소화 시키는 입력값을 찾는다. -> 메모리상 가질 수 있는 최대 최솟값을 찾는다
- 탐색 범위를 유지하기 위해 심볼릭 메모리 주소 $e$를 구체화하기 전에 사용한다
SolveAll(e, π , i)
- SolveMin과 Max를 결합하여 추론 과정에서 확인된 중간 할당값을 도출한다.
- 점프테이블에 접근하는 심볼릭 메모리 주소가 존재하거나 명령어 포인터(ip)가 탐색중에 심볼릭해지는 상황에서 사용된다

Fuzzy-SAT의 이런 primitive과 SMT 솔버와 대응하는 기능을 차별화하는 두 가지 주요 측면이 있다

Fuzzy-SAT은 근사 솔버이다. 따라서 $e \wedge \pi$가 unsatisfiable하다는걸 증명할 수 없다. 비슷하게 해당 식의 전역 최대, 최소값을 찾지 못하거나 가능한 모든 값에 대응하는 할당값을 전부 나열하지 못할 수 있다.
Fuzzy-SAT은 테스트중에 프로그램의 심볼릭 탐색을 유도하는 테스트케이스 $i$를 만드는 콘콜릭 엔진이 필요하다. 이는 fuzzy-SAT이 $e$와 $\pi$를 분석할 때 학습한걸로 인풋을 mutation하기 때문이다.

Overview

Fuzzy-SAT은 analysis, expression metadata, reasoning 총 세 가지 메인 블럭으로 구성되어있다

analysis 단계
- 심볼릭 표현을 분석해서 reasoning 단계에서 사용가능한 지식을 추출하는 과정
- 입력 $i$중에서 어떤 입력 바이트 $i_k$가 수식에 관여하는지 확인한다
- 또한 input-to-state 관계를 감지하여 mutation 단계에서 사용할 수식 내 상수를 수집한다
- 현재 수식이 이전에 분석 컴포넌트에서 처리된 다른 수식들과 입력 바이트를 공유하는지 여부를 감지하고, 이를 통해서 reasoning 단계에서 해당 바이트들을 변이시킬 때 발생할 수 있는 충돌 지점을 찾아낸다.
expression metadata
- analysis 단계에서 처리된 수식을 유지하는데 사용된다
- 이 메타데이터는 수식과 관련된 다양한 유형의 속성을 빠르게 조회할 수 있도록 최적화된 데이터 구조 집합으로 구현되어있다
- 이는 reasoning 단계에서 업데이트되며, analysis, reasoning 모두에서 조회된다.
reasoning 단계
- Fuzzy-SAT이 파악한 지식으로 테스트 케이스를 효과적으로 퍼징하고 할당값을 생성한다
- mutation engine을 이용해서 수식 $e$에 관여하는 입력 바이트에 대해 변환을 수행하고, $e$와 $\pi$를 만족하는 할당값을 찾거나 $\pi$를 만족하면서 $e$를 최대, 최소화하는 할당값을 찾는다.
- 이 단계에서 $e$에 대한 할당값을 찾았지만 $\pi$를 만족하지 못한다면 multi-goal strategy를 수행한다

solve함수는 다음과 같이 진행된다.

$\pi$와 $e$를 분석해서 reasoning 단계에서 사용될 수 있는 정보를 expression metadata $M$에 추가한다
다음은 reasoning으로, Mutate함수로 입력값을 조금 변형했을 때 $\pi$와 $e$를 모두 만족시키는 할당값 $a$를 찾아낸다면 즉시 반환한다
만약 $a$를 찾지 못했지만 일부 할당값 집합 SA가 $e$는 만족시킨다면 multi-goal 단계로 넘어간다
1. PickBestAssignment함수를 사용하여 SA중에서 $\pi$내의 가장 많은 수식을 만족하는 후보 할당값 a를 선택한다
2. FixInputBytes함수로 a에 의해 할당된 입력 바이트를 고정해서 이후 Mutate 호출이 이 바이트를 변경하지 못하도록 한다
3. 이후에 analysis 단계에서 e와 충돌하는 수식 e’를 고려하여 변형을 진행한다
4. 이 과정은 $e\wedge\pi$가 만족되지 않고, 변형했을 때 e’에 대해 최소 하나 이상의 할당값을 SA에 반환하며, 고려할 충돌 수식이 남아있는 동안 반복된다.
opt값이 true일 때 mutation engine이 찾은 $e$는 만족하지만 $\pi$는 만족하지 않는 마지막 후보 할당값을 반환한다. 이 경우 $\pi$의 제약조건을 무시하고 e의 정보만 사용하여 입력 바이트를 만들어낸다.

Fuzzy-SAT의 multi-goal strategy는 정확도를 희생하고 확장성을 얻기 위해 백트래킹을 하지 않는 greedy한 방식을 채택했다.

콘콜릭 엔진이 생성하는 많은 쿼리가 어차피 unsatisfiable하기 때문에 이 전략의 복잡성을 높이는건 fuzzy-SAT에 큰 부담을 줄 수 있다.

Analyzing symbolic expression

analyze함수의 세부 사항

expression metadata M에 저장되는 정보는 다음과 같다

e에 포함되는 입력 리스트
e가 인풋 그룹인지
e의 하위 수식을 재귀적으로 고려했을 때 e에 포함된 입력 그룹들의 리스트

Detecting inputs and input groups

어떤 인풋 바이트 $i_k$가 수식에 관여하는지 확인하고, 이 바이트가 어떻게 그룹화 되어있는지 평가한다.

특히 해당 수식이 비트를 서로 섞지 않고 입력 바이트나 상수를 concatenation(+)한 것과 동일한지 체크한다.

예시

수식 $i_1 \ i_0$은 입력 $i_0$와 $i_1$을 포함하며, 이 바이트들의 비트가 서로 섞이지 않고 단순히 덧붙여진 것이므로 입력 그룹이다
수식 $0 \ i_0$은 입력 $i_0$를 포함하며, $i_0$에 대한 제로 확장(zero-extend) 연산이므로 1바이트 입력 그룹이다.
수식 $i_1 + i_0$은 입력 $i_0$와 $i_1$을 포함하지만, $i_0$의 비트가 $i_1$의 비트와 산술적으로 더해졌으므로 입력 그룹이 아니다. (여기서는 산술연산으로 사용됨)
수식 $(0 \ i_0) + (i_1 \ll 8)$은 $i_0$와 $i_1$을 포함하며, 이 수식이 $i_1 \ i_0$과 동일하므로 입력 그룹이다

Detecting uniquely defined inputs

입력 바이트에 대한 결정적인 정보중 하나는, 해당 바이트를 포함하는 equality constraint (==연산)으로 인해 그 값이 단일 값으로 고정되었는지를 아는 것이다. 이 값은 fuzzing하지 않는 것이 좋다.

이를 uniquely defined라고 하겠다.

수식 e가 주어졌을 때

만약 e가 등치 제약 조건이고, 한 피연산자가 입력그룹이면서 나머지가 상수라면 e가 $\pi$에 추가될 때 해당 그룹의 바이트는 e에 의해 uniquely defined이다.
$\pi$에 포함된 제약 조건이 어떤 입력을 uniquely defined라고 한다면 e 내의 해당 입력도 uniquely defined이다
e 내의 입력그룹을 구성하는 모든 입력이 $\pi$의 제약 조건에 의해 uniquely defined라면 해당 입력 그룹 자체가 uniquely defined이다

예를 들어서, $i_1 + i_0 == 0xABCD$ 에서 $i_0$과 $i_1$은 uniquely defined이다. (더하기 연산이 아니라 concatenation 연산)

Detecting input-to-state branch conditions

e가 input-state correspondence를 갖는 피연산자를 최소 하나 이상 포함하는지 확인한다.

이는 다음 조건을 사용하여 판단한다.

e가 $e’ \ op_{cmp} \ e’’$ 패턴과 일치해야한다. $op_{cmp}$는 비교연산자이다
피연산자중 하나가 입력 그룹이어야한다.

e가 boolean negation일 때 Fuzzy-SAT는 재귀적으로 subexpression( !(a and b) 같은 수식) 을 분석한다

예를 들어서, $10 ≥ i_1 + i_0$에서 ≥가 비교연산자이고 $i_1 + i_0$가 입력 그룹이므로 input-state 분기 조건이다.

Detecting interesting constants

e에서 reasoning 단계에서 사용될 상수를 찾아내고, mutation과정에서 사용할 사전을 동적으로 구성한다.

특정 패턴이 감지되면 e에 의해 수행되는 계산의 semantic을 바탕으로 해당 상수의 variant를 생성한다.

예를 들어서, $i_1 \oplus 0xF0 == 0x0F$를 분석할 때, Fuzzy-Sat은 상수 0xF0, 0x0F, 그리고 0xFF를 수집한다.

Detecting range constraints

e가 range constraint인지 확인한다.

예를 들어서, e’가 입력 그룹이고 e’’가 상수인 $e’ \ op_{cmp} \ e’’$ 패턴의 제약 조건을 찾는다. 또한 e’가 입력 그룹이고 e’’ e’’’가 상수인 $(e' - e'') \ op_{cmp} \ e'''$같은 패턴도 범위 제약 조건으로 취급한다.

또한 e와 $\pi$로부터 구한 경계값을 함께 고려함으로써, fuzzy-SAT은 수식에 포함된 입력 그룹에 대해 정제된 범위 구간을 구할 수 있다.

이러한 구간을 효율적으로 유지하기 위해 signed, unsigned 비교 연산자를 모두 처리할 수 있는 wrapped intervals를 사용한다

예를 들어서, 수식 $i_1 + i_0 > 10$과 $i_1 + i_0 \leq 30$이 주어지면, Fuzzy-Sat은 $i_0$와 $i_1$로 구성된 입력 그룹에 대해 범위 구간 $[11, 30]$을 계산한다.

Detecting conflicting expressions

e의 입력 바이트 중 일부를 할당할 때 $\pi$에 포함된 수식 중 어떤게 e와 충돌할 수 있는지 찾는다.

예를 들어서, 수식 $i_1 + i_0 > 10$은 $i_1 + i_2 < 20$과 충돌한다. 이는 모두 입력 바이트 $i_1$를 포함하고있기 때문이다.

conflicting expression의 집합을 구하는건 reasoning 단계에서 multi-goal strategy를 수행할 때 필수적이다

Fuzzing symbolic expressions

Fuzzy-SAT의 reasoning 단계의 핵심은 유효한 할당값 a를 찾기 위한 mutate 함수의 실행이다.

다음은 mutate함수의 인풋 변환 상세 내용이다.

Fuzzing input-to-state relations

수식 e가 input-to-state branch condition일 때 만약 피연산자가 상수라면 입력 그룹의 바이트에 해당 값을 대입하고, 만약 상수가 아니라면 해당 값의 기댓값을 파악해 대입한다.

만약 피연산자가 상수이며 ==관계일 때 할당값이 $\pi$를 만족하지 않는다면 해당 쿼리를 unsatisfiable한 것으로 간주한다.

반대로 비교 연산자가 ==가 아닐경우, 인풋 그룹을 조금씩 변형하여 테스트한다.

예를 들어서, $i_1 + i_0 == 0xABCD$가 주어지면, $i_0 ← 0xCD, \ i_1 ← 0xAB$로 할당한다.

만약 $\pi$의 제약 조건으로 인해 $i_0$의 범위 구간이 $[0xDD, 0xFF]$라면, 테스트를 하지 않고 해당 쿼리는 unsatisfiable한걸로 간주한다

Range interval brute force

e에 포함된 입력 그룹에 대해 범위 구간이 알려져있을 때, brute force를 시도하여 할당값을 찾는다.

이 때 범위구간이 2048보다 작다면 모든 가능한 값을 할당하며, 이보다 클 경우에는 구간의 최솟값과 최댓값을 테스트한다.

예를 들어서, $(i_1 + i_0) * 0xABCD == 0xCAFE$가 주어지고, $\pi$의 제약 조건에 의해 그룹 $g(i_0, i_1)$에 대한 범위 구간이 $[1, 9]$라면, $g \in [1, 9]$에 대한 할당값들을 만든다.

그 중 $e \wedge \pi$를 만족하는게 없다면 해당 쿼리는 unsatisfiable한 것으로 간주한다

Trying interesting constants

analysis 단계에서 수집한 각 상수 c와 e에 포함된 입력 그룹 g에 대해서, g의 바이트를 c값으로 대입한다.

이때 상수 c는 relaxed pattern(범위가 넓게)으로 수집되므로 각 상수에 대해서 little-endian이나 big-endian같이 다양한 인코딩으로 테스트한다.

Gradient descent

e에 대해서 유효한 할당값을 찾는 문제에서 최소화/최대화 문제로 변환한다.

예를 들어서, $e' < e''$는 $f = e' - e''$일 때 $f < 0$으로 변환될 수 있다

여기서 할당값을 찾는데에 구현된 탐색 알고리즘은 경사 하강법을 기반으로 한다.

물론 경사 하강법은 global minimum을 찾는데에 실패할 수 있지만 concolic execution에서는 local minimum을 찾는걸로 충분한 경우가 많다.

e의 입력 그룹들이 disjoint한 바이트를 가질 때는 바이트 그룹 단위로 경사를 계산하여 더 효과적으로 할당값을 찾도록 한다.

예를 들어서, $(i_0 + i_1) − 10 > (i_2 + i_3) − 5$ 라는 수식이 있다고 해보자.

이를 $f = ((i_2 + i_3) - 5) - ((i_1 + i_0) - 10) < 0$ 로 변환할 수 있고 $i_1+ i_0$와 $i_2+ i_3$에 대해서 경사를 계산해서 ${i_0 \leftarrow 0x80, i_1 \leftarrow 0x06, i_2 \leftarrow 0x84, i_3 \leftarrow 0x01}$라는 할당값을 찾아낸다.

Deterministic and non-deterministic mutations

해당 기법은 AFL에서 가져온 개념이다.

deterministic mutation에서는 비트나 바이트를 flip하거나 바이트를 MAX_INT같이 알려진 상수로 대체하는 기법을 쓴다.

non-deterministic mutation에서는 무작위로 선택된 입력 바이트 내부의 무작위 비트를 반전시키거나 무작위로 선택한 유의미한 상수로 설정하는 등의 mutate를 진행한다.

하지만 AFL과 몇 가지 차이점이 있다

mutation는 e에 포함되는 입력 바이트들에 대해서만 적용된다
multi-byte mutation은 multi-byte 입력 그룹이 존재할때만 고려한다
non-deterministic mutation의 경우 k개의 서로 다른 할당값을 생성한다
1. k는 max{100, $n_i$ · 20}와 같다. 여기서 $n_i$는 e에 관여하는 입력의 개수이다.

Evaluation

다음 research questions를 다룬다

실제 프로그램에서 심볼릭 쿼리를 생성하는 Fuzzolic의 효율은 어떤가
콘콜릭 실행기가 생성한 쿼리를 해결하는 Fuzzy-SAT의효과와 효율은 어떤가
하이브리드 퍼징 설정에서 Fuzzolic과 Fuzzy-SAT의 성능은 어떤가

커뮤니티에서 집중적으로 퍼징된 다음 12개의 프로그램을 대상으로 벤치마크를 진행한다.

advmng 2.00, bloaty rev 7c6fc, bsdtar rev. f3b1f, djpeg v9d, jhead 3.00–5, libpng 1.6.37, lodepng-decode rev. 5a0dba, objdump 2.34, optipng 0.7.6, readelf 2.34, tcpdump 4.9.3 (libpcap 1.9.1), tiff2pdf 4.1.0

테스트는 ubuntu 18.04 이미지 기반의 Docker 컨테이너에서 수행되었으며 2개의 Intel Xeon E5-4610v2 @ 2.30 GHz CPU와 256 GB RAM을 탑재한 서버를 사용했으며, 운영체제는 Debian 9.2 x86_64 환경이다.

Efficiency of Fuzzolic

Fuzzolic과 다른 최신 콘콜릭 실행기들과 심볼릭 쿼리를 생성하는데 걸린 emulation time을 비교한다.

Fuzzolic은 소요시간이 항상 0.4초 미만이고 Qsym은 항상 14초 이상 소요되었다.

이는 Qsym이 최신 버전의 포팅이 어려운 구 버전의 Intel PIN을 기반으로 하고있으며, instrumentation이 최적화되어 있지 않았기 때문이다.

SymCC와 비교했을 때는 3개의 벤치마크에서 뒤쳐졌는데, SymCC는 소스코드 기반임에도 불구하고 그 격차가 2배 미만임을 보여주었다.

Fuzzolic과 SymQEMU는 디자인 자체가 유사하고 동적 바이너리 변환기를 기반으로 한다.

그럼에도 Fuzzolic은 항상 SymQEMU보다 빠른걸로 측정되었다.

djpeg, objdump에 대해서 performance profiling을 수행했을 때, SymQEMU가 느린 이유는 바이트 그룹을 처리하는 일부 TCG 명령어를 다루는 방식이라고 판단됨.

Fuzzolic은 바이트 그룹으로부터의 concat 과 extract 연산을 효율적으로 하기 위한 저수준 최적화를 포함하고있다.

따라서 Fuzzolic이 SymQEMU보다 빠른 이유는 두 가지 요인이다

일부 TCG 연산을 처리할 때 수행되는 inline instrumentation
최적화된 분석 모드

Impact of different analysis modes in Fuzzolic

Fuzzolic의 분석 모드가 미치는 영향과 공유 메모리를 통한 솔버 컴포넌트와의 동기화 및 통신 비용을 측정하기 위해 위의 테스트를 반복 측정한 결과이다.

설정 X: tracer가 가장 오버헤드가 큰 모드 C로만 작동하여 활성화된 공유 메모리가 없다
설정 Y: tracer가 상황에 따라 모드 A, B, C 모드를 동적으로 전환하지만 공유 메모리는 사용하지 않는다
설정 Z: tracer가 상황에 따라 모드 A, B, C 모드를 동적으로 전환하며 공유 메모리를 사용하여 솔버 컴포넌트에 쿼리를 전달한다. (다른 도구와 비교할 때 사용한 모드)

실험 결과 모드를 전환한 결과가 모드를 전환하지 않은 설정 X보다 평균 1.5배의 속도 향상이 이루어졌다.

여기서 분석한 내용을 솔버에게 전달하는 과정을 추가하면 평균 1.2배 느려진다.

Solving effectiveness of Fuzzy-SAT

쿼리를 해결하는데에 있어 Fuzzy-SAT과 Z3및 JFS와 비교 실험을 진행했다.

먼저 optimistic solving을 비활성화한 상태에서 12개 프로그램을 QSYM으로 실행하여 세 가지 솔버를 사용할 때의 solving time과 satisfiable로 입증된 쿼리의 수를 비교했다.

그 후 Fuzzy-SAT과 Z3를 사용할 때 LAVA-M 데이터셋에서 버그를 찾아내는 Qsym의 성능을 분석했다.

Fuzzy-SAT와 Z3를 비교했을 때 두 가지 흥미로운 점이 있다

두 솔버 모두 쿼리의 10%미만만 satisfiable로 증명되었다.
satisfiable한 쿼리들을 봤을 때 Fuzzy-SAT는 대부분 해결할 수 있으며 Z3보다 더 나은 성능을 보이기도 한다
Fuzzy-SAT이 Z3보다 평균 31배 적은 시간을 소요한다

위 그림은 제한 시간을 1초로 설정했을 때 Z3가 해결한 쿼리 수와, fuzzy-SAT의 속도 향상이 어떻게 감소하는지 보여준다.

제한 시간을 줄여도 Z3의 속도와 해결한 쿼리 수는 fuzzy-SAT이 좋다는걸 확인할 수 있다.

Fuzzy-SAT과 JFS를 비교했을때 JFS는 Fuzzy-SAT보다 훨씬 적은 쿼리를 해결할 수 있었다.

bsdtar 의 325개의 쿼리 중 127개에서 JFS는 쿼리에 포함된 수많은 nested expression으로 인해 퍼징할 프로그램을 생성하는데 실패했다.

solving time을 고려한다면 Fuzzy-SAT는 JFS보다 1.5배 빠르고 여기서 analysis cache를 활성화하면 최대 4.8배까지 증가한다

Impact of different mutations in Fuzzy-Sat

여기서 흥미로운 점은 input-to-state 변환을 적용하여 쿼리의 51% 이상을 해결하였고, 17%는 interesting constants를 활용하여 해결되었다.

Fuzzy-SAT on LAVA-M

Fuzzy-SAT이 콘콜릭 실행기에게 가치있는 쿼리를 해결할 수 있는지 테스트하기 위해 LAVA-M 테스트셋을 대상으로 base64, md5sum, uniq, who 4 개의 벤치마크 내의 버그를 찾는 실험을 진행했다.

실험 결과는 5회 반복 실행된 실험에서 발견된 버그의 평균 및 최대 개수이다.

Fuzzy-SAT는 3개의 항목에서 Z3보다 평균적으로 더 많은 버그를 발견했으며, 이는 하이브리드 퍼징에서 정확도와 성능을 맞바꾸는 것이 가치가 있음을 시사한다

또한 Fuzzy-SAT은 who 에서 136개의 새로운 버그를 찾아내었으며, false positive일 가능성은 낮다.

Fuzzy-SAT and Fuzzolic in hybrid fuzzing

Fuzzolic과 Fuzzy-SAT을 평가하기 위해 위의 12개의 벤치마크를 대상으로 8시간동안 10회 반복하여 실행을 진행하였고, 달성된 코드 커버리지를 추적하여 hybrid setup에서의 솔루션을 평가했다.

fuzzolic외에도 다음 세 가지 바이너리 퍼징 도구에 실험을 진행했다.

QEMU모드의 AFL++
Eclipser
Qsym

추가적으로 에뮬레이션 단계에서 효율적인 것으로 알려진 소스 기반 콘콜릭 실행기 SymCC와, fuzzolic과 여러 설계를 공유하는 바이너리 콘콜릭 실행기 SymQEMU도 비교 대상에 포함했다.

각 도구는 두개의 coverage-guided 퍼저 인스턴스 $F_m, \ F_s$와 병렬로 실행되며, 주기적인 입력 큐 동기화를 허용한다. 따라서 각 실행은 CPU시간으로 24시간을 소모한다.

차트에는 엣지 커버리지를 표시하고 음영으로 95% 신뢰 구간을 표시한다.

Fuzzy-SAT을 결합한 Fuzzolic은 6개 프로그램에서 다른 도구보다 높은 코드 커버리지에 도달한다.

Fuzzolic과 Qsym을 비교해보면 커버리지의 향상은 fuzzolic이 Qsym보다 더 나은 확장성을 가졌기 때문으로 보인다..

Fuzzolic with Fuzzy-SAT vs SymCC

Fuzzolic은 SymCC와 비교했을 때 4개 중 3개 벤치마크에서 더 높은 코드 커버리지에 도달했다.

이는 SymCC는 소스코드 기반의 콘콜릭 실행기이기 때문에 이미 컴파일된 라이브러리 함수를 호출할 때 제대로 쿼리를 만들어내지 못한다. 이로 인해 커버리지가 낮게 나오는 것이다.

다음은 동일한 tracer환경에서 solver만 변경했을 때의 결과이다.

Fuzzolic을 사용하고 Fuzzy-SAT, Z3를 솔버로 사용했을 때 Fuzzy-SAT은 4개의 대상 프로그램 중 3개에서 우위를차지한다.

Qsym을 사용하고 Fuzzy-SAT, Z3를 솔버로 사용했을 때 개선의 정도는 전반적으로 분석 대상이 되는 특정 벤치마크에 따라 다르게 나타난다.

SymCC을 사용하고 Fuzzy-SAT, Z3를 솔버로 사용했을 때 readelf 에서만 유의미한 향상이 나타났고 다른 타겟들에서는 매우 유사하게 측정되었다.

이론적으로 효율적인 콘콜릭 실행기라면 더 빠른 솔버의 혜택을 받아야한다. 하지만 결과가 이렇게 나온 원인은 다음과 같다.

SymCC는 Fuzzolic이나 Qsym같은 다른 바이너리 프레임워크에 비해 제한된 수의 쿼리만 생성한다.
이는 SymCC가 라이브러리를 심볼릭하게 instrumentation하지 않기 때문에 풀 수 있는 쿼리가 차이가 없는 것이다.

실제로 Fuzzy-SAT을 사용했을 때 대기 상태의 시간이 크게 증가했다.

마지막은 Fuzzolic과 SymQEMU의 비교이다

다른 실험 결과와 마찬가지로 fuzzolic은 libpng에서 Z3를 사용하는 다른 콘콜릭 실행기들보다 성적이 좋지 않았다.

나머지 objdump , readelf, tcpdump, tiff2pdf 에서는 Fuzzy-SAT을 사용한 Fuzzolic은 항상 SymQEMU보다 높은 커버리지를 달성한다.

Conclusions

Fuzzolic은 실행중에 바이너리 프로그램을 instrumentation하여 심볼릭 수식과 쿼리를 구축할 수 있는 QEMU 기반의 새로운 콘콜릭 실행기이다.

Fuzzy-SAT은 콘콜릭 실행 과정에서 생성된 쿼리를 처리하는 새로운 근사 솔버이다.

앞으로의 개선사항

AFL과 같은 바이너리 퍼저에서 볼 수 있는 fork server를 구현하여 서로 다른 실행간에 JIT 캐시를 활성화한상태로 instrumentation 시간을 최소화한다.
서로 다른 실행 간에 symbolic expression과 쿼리를 캐싱해서 이를 최적화하고 Z3 수식으로 변환하는 시간을 줄일 계획이다. 추가적으로 symbolic expression을 분석할 때 Fuzzy-SAT이 학습한 analysis facts를 캐싱해서 비슷한 수식에 대해서 빠른 계산을 가능하게 한다.

후기

목표는 심볼릭 실행처럼 분기 제약조건을 만족시키는 할당값을 찾는건데, 그 방법으로 SMT solver처럼 수학적으로 계산을 하는게 아니라 퍼징의 방법을 채용하면서 경사하강법이나 부르트포스로 만족하는 값을 찾는 방법이 인상적이었다.

근데 libpng처럼 이미지를 처리하거나 tcp 패킷을 처리하는 프로그램에 대해서는 Z3처럼 정확성을 요구하는 방법이 더 효율적이라는 실험 결과가 있었다.

이 경우에 정확한 값을 요구하거나 근사하는 방법으로 최적해를 구할 수 없다면 fuzzy-SAT에서 Z3로 전환하는 방법이 있지 않을까 싶다.

'보안 > 논문 리뷰' 카테고리의 다른 글

[논문 정리] SCASE: Automated Secret Recovery via Side-Channel-Assisted Symbolic Execution (0)	2026.05.03
[논문 정리] The Art, Science, and Engineering of Fuzzing: A Survey (0)	2026.03.29

현재글[논문 정리] FUZZOLIC: Mixing fuzzing and concolic execution

pumisj 님의 블로그

pumisj 님의 블로그 입니다.

Today :
Yesterday :