« 2024/12 »
일	월	화	수	목	금	토
1	2	3	4	5	6	7
8	9	10	11	12	13	14
15	16	17	18	19	20	21
22	23	24	25	26	27	28
29	30	31

본 내용은 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE)에서 발표된 Grey-box Concolic Testing on Binary Code 논문에 대한 리뷰 글이다.

사실 리뷰보다는 번역이 더 맞다.. 요약도 정리해 봤는데, 표기법과 수식을 빼니 너무 밋밋해지고 다시 넣으니 그냥 번역과 같아졌다. (요약은 너무 어려워..)

해당 논문에서는 Grey-box Concolic Testing이라는 기법을 제안하는데, 여기서는 간단히 GCT라고 줄여서 부르겠다.

여담으로 얼마 전 정말 운 좋게도 본 논문의 저자 중 한 분이신 KAIST SoftSec Lab의 차상길 교수님께 해당 논문을 7분 내로 요약해 발표할 기회가 있었다.

특히 발표용 PPT 마지막 장표에서 본 연구와 논문에 대한 나의 견해를 발표했는데, 그에 대한 교수님의 피드백도 받을 수 있었다🥳.

[*] 정확한 정보 전달을 원하신다면 원문을 반드시 봐주세요.

[**] 본 글에는 발 번역, 틀린 내용, 애매한 내용 등을 다수 포함하고 있을 수 있습니다.

[***] 본 글에는 의도적으로 원본 내용을 일부 삭제/수정했을 수 있습니다.

본 논문의 기여는 다음과 같다.

novel path-based test case generation algorithm인 Grey-box Concolic Testing(이하 GCT)을 제안한다.

GCT는 Grey-box Fuzzing 방식보다 fitness function이 민감하는 장점이 있다.

GCT는 White-box Fuzzing 방식에 비해 경략적(lightweight)이면서 규모 가변적(scalable)이라는 장점이 있다.

GCT 전략과 기존의 고전적인 Grey-box Fuzzing 전략을 번갈아 사용하는 Eclipser라는 도구를 구현했다.

Eclipser를 평가한 결과 code coverage, bug finding, scalability 모두 비교 대상보다 뛰어났다.

Eclsiper를 open source하여 공개하고 있다. [링크]

ABSTRACT

본 논문에서는 화이트박스 퍼징과 그레이박스 퍼징의 장점을 결합한 새로운 경로 기반 테스트 케이스 생성 방법인 grey-box concolic testing을 제시한다. 고수준에서 우리의 기술은 화이트박스 퍼징, 일명 concolic tesing처럼 테스트 대상 프로그램의 실행 경로를 체계적으로 탐색하는데, 이때 그레이박스 퍼징의 단순성을 포기하지 않는다. 즉, 경량 계측만을 사용하고 SMT 솔버에 의존하지 않는다. 우리는 Eclipser라는 시스템에서 우리의 기술을 구현했고, 이를 최신의(:state-of-the-art) 그레이박스 퍼저(AFLFast, LAF-intel, Steelix, VUzzer 포함) 및 symbolic executor(KLEE)와 비교했다. 우리의 실험에서는 더 높은 코드 커버리지를 달성했고, 다른 도구보다 더 많은 버그를 발견했다.

Index Terms - software testing, concolic testing, fuzzing

I. INTRODUCTION

fuzz testing(줄여서 fuzzing)은 closed binary code의 보안 취약점을 찾는 사실상의 표준이었다. 퍼징은 증거와 함께 버그를 찾기 때문에 보안 실무자들은 퍼징을 높게 평가한다. Microsoft 및 Google과 같은 주요 소프트웨어 회사는 현재 제품의 보안을 보장하는 수단으로 소프트웨어 개발 life cycle에서 퍼징을 사용한다.

가장 주목할 만한 점은 AFL, AFLFast, Steelix, VUzzer, Angora, CollAFL, T-Fuzz와 같은 그레이박스 fuzzer가 버그를 찾는 최신 도구로 부상하고 있다는 점이다. 그레이박스 퍼징은 진화 과정(evolutionary process)을 통해 테스트 케이스를 생성한다. 특히 테스트 케이스틑 실행하고 그 테스트 케이스를 fitness function(objective function)을 기반으로 평가한다. 그러고는 더 좋은 fitness를 가진 테스트 케이스들에게 우선순위를 부여하고, 목표를 충족하는 테스트 케이스를 찾도록 발전(evolve)시키고, 프로그램 크래시를 트리거하는 buggy path로 실행하기 위해 전체 프로세스를 반복한다.

현재 그레이박스 퍼저들은 code coverage를 fitness function으로 사용한다. 따라서, coverage-based fuzzer라고도 한다. 예를 들어, AFL과 이를 계승한 퍼저들은 branch coverage의 근사적인 형태를 사용하고, VUzzer는 가중치 기본 블록(weighted basic block)의 hit count를 fitness function으로 사용한다. 이는 코드 커버리지를 최대화하는 것이 PUT(Program Under Test)의 흥미로운 실행 경로에 도달할 가능도(likelihood)를 증가시킬 수 있다는 것을 의미한다.

그러나 현존하는 그레이박스 퍼저들은 커버리지 기반의 guidance를 사용함에도 새로운 branch를 탐색하는 데에 어려움을 겪고 있는데, 이는 input mutation에 대해 코드 커버리지가 그다지 민감하게 바뀌지 않기 때문이다. 특히, 두 개의 서로 다른 입력을 사용하는 두 프로그램은 실행에서 조건 분기(conditional branch)의 비교된 값이 다르더라도 같은 코드 커버리지를 달성할 수도 있다. 즉, 코드 커버리지는 조건 분기가 랜덤하게 생성된 입력으로 통과한(penetrate) 경우에만 피드백을 제공할 수 있지만, 이런 피드백은 이러한 입력 생성에 직접적인 도움이 되지는 않는다. 이렇게 부족한 (변화의) 민감도로 인해 그레이박스 퍼저들이 특정 환경(예를 들어, PUT가 input을 특정 magic value와 비교하는 경우)에서 높은 커버리지를 만족하는 테스트 케이스를 생성하는 데에 어려움을 겪는다. 심지어 AFLGo, Steelix, VUzzer와 같은 현재의 최신 그레이박스 fuzzer들조차도 거의 동일한 문제를 가지고 있다.

결과적으로 그레이박스 퍼징은 취약점을 찾는 그 효과에도 불구하고, 그 자체만으로는 테스트 케이스 생성 알고리즘이 될 수는 없다고 알려져 있다. 따라서 그레이박스 fuzzer는 종종 동적 기호 실행이나 fine-grained taint analysis와 같은 heavy-cost white-box analysis 또는 테스트 케이스 생성 프로세스를 지시(direct)하기 위한 initial seed 입력을 제공함으로써 보강(:augmented)된다. 예를 들어, Angora와 Driller는 각각 fine-grained 오염 분석과 동적 기호 실행을 활용하여 그레이박스 퍼징의 코드 커버리지를 향상한다.

한편, 화이트박스 퍼징(동적 기호 실행, concolic testing)은 branch condition을 solve하여 테스트 케이스를 체계적으로 생성할 수 있지만, 기본적으로 규모 가변성(scalability)에 의해 제한되며 고전적인 경로 폭발 문제(path explosion problem)를 해결하지 못하고 있다(:leaving aside). 먼저 화이트박스 퍼저는 PUT의 모든 단일 명령어(single instruction)를 분석한다. PUT의 모든 단일 명령어를 계측하기 때문에, 모든 fuzz iteration에는 상당한 계산 비용이 수반된다. 두 번째로, 기호 실행은 모든 실행 경로에 대한 기호 경로 제약 조건(symbolic path constraints)을 구축(:build up)한다. 이러한 제약 조건을 SMT sovler로 solve하는 것은 계산 비용이 많이 든다. 게다가 symbolic input의 영향을 받는 모든 단일 메모리 cell에 대한 기호 표현식(symbolic expression)을 저장하려면 상당한 메모리 공간이 필요하다.

본 논문에서 Grey-box Conolic Testing(이하 GCT)이라고 하는 새로운 테스트 케이스 생성 기술을 제안하고 여기서 Eclipser라고 부르는 도구에서 구현한다. grey-box concolic testing(이하 GCT)은 화이트박스 퍼징과 같은 조건 분기를 충족하는 테스트 케이스를 효율적으로 생성하는데, 이때 단순성을 유지한다. 즉, 비용이 높은 프로그램 분석 기술에 의존하지 않는다. 따라서 그레이박스 퍼징과 같은 real-world 프로그램으로 확장될 수 있다.

우리의 접근 방식은 화이트박스 퍼징에서 널리 사용되는 search strategy인 generational search과 유사하다. 이는 단일 프로그램 실행이 실행 중에 발생하는 모든 조건 분기를 해결(:resolve)하여 테스트 케이스 generation을 생성하는 방식을 말한다. GCT(grey-box concolic testing)는 경로 기반 테스트 케이스 생성도 수행하지만 (PUT를 계측하고, 테스트 케이스를 생성하기 위해 execution behavior를 관찰하는 방식인) 그레이박스 방식으로 조건 분기를 resolve하려고 시도한다.

GCT와 화이트박스 퍼징의 주요 차이점은 GCT의 접근 방식이 PUT의 각 실행 경로를 실행하기 위한 input condition을 부분적으로 설명(:describe)하는 근사적인(approximated) 형태의 경로 제약 조건에 의존한다는 것이다. approximated path constraint(이하 근사 경로 제약 조건)은 SMT solving과 같은 CPU 또는 메모리 집약적(:intensive) 연산에 의존하지 않고 조건 분기를 통과할 수 있는 입력을 찾는 데 도움이 된다. 물론 GCT에서 생성된 경로 제약 조건은 정확하지는 않지만 실제로는 다양한 실행 경로를 빠르게 탐색할 수 있을 만큼 정확하다. 여기서 주요 design decision은 단순성과 정확성을 trade off 하는 것이다.

물론 정확도가 떨어지면 PUT에서 불완전한 경로 탐색이 발생하지만 Eclipser는 Driller에서와 같이 GCT와 고전적인 그레이박스 퍼징을 교대로 사용하여 이를 보완한다. GCT가 PUT의 모든 조건 분기를 cover하는 것은 아니지만, 그레이박스 퍼징 모듈은 계속해서 새로운 경로와 분기를 cover하며, 그 반대의 경우도 마찬가지다. 우리는 실제로 이 design decision이 취약점을 발견하고 높은 코드 커버리지에 도달한다는 점에서 현재 최신의 그레이 및 화이트 박스 fuzzer들을 넘어 Eclipser의 능력을 효과적으로 확장한다는 것을 발견했다.

우리는 연구에서 최신 fuzzer들에 대해 Eclipser를 평가했다. test case generator로서의 우리 시스템의 실용성은 주어진 소스 코드에서 높은 커버리지로 테스트를 생성하는 데 탁월한 것으로 알려진 최신 symbolic executor인 KLEE에 대해 수행한 실험에서 확인되었다. 실험에서 Eclipser는 SMT solver의 도움 없이 테스트 케이스 생성 알고리즘을 평가하는 데 사용되는 잘 알려진 벤치마크인 GNU coreutils에서 KLEE보다 8.57% 더 높은 코드 커버리지를 달성했다.

Eclipser를 bug finding tool로서 평가하기 위해 AFLFast, LAF-intel, Steelix, VUzzer와 같은 여러 최신의 그레이박스 퍼저들과 비교했다. 또한 Debian 9.1에서 추출한 22개의 바이너리에서 Eclipser를 실행했고, 17개의 프로그램에서 40개의 unique 버그를 발견했다. 발견한 모든 버그는 개발자에게 제보했다. 요약하자면, 본 논문의 기여는 다음과 같다.

경량 계측을 활용하여 높은 커버리지의 테스트 케이스를 생성하는 새로운 경로 기반 테스트 케이스 생성 알고리즘인 grey-box concolic testing(GCT)을 소개한다.

GCT를 기반으로 Eclipser를 구현하고, 이를 AFLFast, LAF-intel, Steelix, and VUzzer를 포함하는 최신의 퍼저들에 대해 다양한 벤치마크로 평가한다. 평가 결과 Eclipser는 코드 커버리지 달성과 버그 발견 모두에서 비교 대상 퍼저들에 비해 뛰어났다.

Eclipser를 22개의 real-world Linux 응용 프로그램에서 실행했으며, 40개의 unknown bug를 발견했다. 그들 중 8개는 CVE id를 할당받았다.

open science를 위해 Eclipser의 소스 코드를 공개한다: https://github.com/SoftSec-KAIST/Eclipser.

II. BACKGROUND AND MOTIVATION

A. Grey-box Fuzzing

fuzzing은 본질적으로 생성된 테스트 케이스로 PUT(Program Under Test)를 반복적으로 실행하는 프로세스다. 그레이박스 퍼징은 feedback loop 내에서 테스트 케이스를 진화시키며, 여기서 각 테스트 케이스를 이용한 PUT의 실행은 fitness function이라는 기준에 의해 평가된다. 예를 들어, AFL은 branch coverage(modulo some noise)를 사용하여 다음에 fuzz해야 할 입력을 결정한다.

최근의 성공에도 불구하고, 커버리지 기반 그레이박스 퍼저는 퍼징 프로세스가 특정 분기를 실행하는 테스트 케이스를 찾기 위해 너무 많은 불필요한 시도를 포함한다는 주요 결점을 가지고 있다. 이는 주로 퍼징에 사용되는 fitness function의 둔감함 때문이다. informal하게 말하자면, 입력 값이 조금 변화했을 때 fitness가 쉽게 변한다면 fitness 함수가 민감하다고 할 수 있다. 모든 code coverage metric(ex. node coverage나 branch coverage)은 true branch와 false branch를 커버하는 두 실행 사이에 중간(intermediate) fitness가 없기 때문에 둔감하다. 그로 인해 주어진 조건 분기를 뒤집는(flip) 입력을 찾는 것이 어렵다.

테스트 케이스 생성이 최적화 문제로 고려되는 검색 기반 소프트웨어 테스팅에서 민감한 fitness function의 필요성이 널리 인식되고 있다. 주목할 만한 fitness function 중 하나는 조건 분기의 operand 값 사이의 거리인 branch distance다. 퍼징 커뮤니티는 최근 이 아이디어를 사용하기 시작했다. Angora는 퍼징 성능을 개선하기 위해 branch distance를 활용했다. Eclipser는 유사한 insight를 활용하지만, 메타휴리스틱에 의존하지 않고 민감도를 사용하여 근사 분기 조건을 직접 추론하고 solve 한다. 두 접근 방식은 서로 직교(orthogonal)하고 상호 보완적이다.

B. Notation and Terminologies

실행을 finite sequence of instructions로 가정한다. 예를 들어, 무한 루프가 있는 프로그램 실행은 고려하지 않는다. 이러한 가정은 fuzzing에서는 문제가 되지 않는데, 퍼저는 일반적으로 parameter 중 하나인 특정 시간이 지나면 PUT를 강제로 종료하기 때문이다. 프로그램 $p$ 를 input $i$ 로 실행하는 것을 $\sigma_p(i)$ 로 표기하겠다. 우리의 모델에서 입력은 byte sequence지만 bit string을 표현하기 위해 쉽게 확장할 수 있다. $i[n]$ 은 입력 $i$ 의 $n$ 번재 바이트 값을 의미한다. $i[n]$ 을 수정해 $v$ 가 되는 것을 $i[n \leftarrow v]$ 로 표기하겠다. 본 논문 전체에서 테스트 케이스와 test input이라는 용어를 같은 의미로 사용한다. input field는 input의 연속적인 부분열(:consecutive subsequence)이라고 하겠다. 주어진 입력에 대해 많은 입력 필드가 있을 수 있으며, 입력 필드가 겹칠 수도 있다.

Approximate Path Constraint.

기호 실행에서, 경로 제약이란 실행 경로가 실행 가능하면 해당 path condition이 충족되도록 하는 입력에 대한 술어(:predicate)이다. 우리의 접근 방식은 경량화를 시도하므로, 정확한 경로 조건을 추적하지 않고 approximate path constraint이라고 하는 근사적인 버전을 trace한다.

Seed.

본 논문에서 seed를 특정 프로그램에 대한 입력을 나타내는 data structure라고 하자. 프로그램 $p$ 에 대한 시드를 $s_p$ 로 표기하고, $p$ 를 시드 $s_p$ 로 실행하는 것을 $\sigma_p(s_p)$ 로 표기하겠다. $s_p[n]$ 은 시드 $s_p$ 의 $n$ 번째 바이트를 의미한다. 시드의 모든 바이트에는 바이트와 관련된 근사 경로 제약 조건의 독립적인 하위 집합인 "constr" field가 태그로 지정된다. $s_p[n].constr$ 라는 dot notation을 사용하여 시드 $s_p$ 의 $n$ 번째 바이트에 대한 근사 경로 제약 조건에 접근할 수 있다. 주어진 시드 $s_p$ 에 대해 시드의 $n$ 번째 바이트 $s_p [n]$ 는 $\sigma_p(s_p)$ 와 동일한 실행 경로를 실행하기 위해 $s_p[n].constr$ 를 만족해야 한다.

C. Motivation

Fig. 1. Our motivating example and a comparison of different fuzzers.

Figure 1(a)는 우리의 연구에 동기를 부여한 예제 프로그램이다. 쉬운 설명을 위해 C 언어로 표기했지만, 우리의 시스템은 raw binary executable에 대해 동작한다. 이 예제에서는 파일을 입력으로 하며 파일의 전반부 4 바이트는 integer로, 나머지 4 바이트는 맨 뒤에 NULL character를 삽입하여(Line 10) 5-byte string으로 사용한다. 이 두 값은 vulnfunc 함수의 매개 변수로 사용된다. Line 4의 크래시를 찾기 위해 32-bit integer 15668과 string "Bad!"를 함수의 입력으로 제공해야 한다.

현재의 그레이박스 퍼저가 이 크래시를 트리거하는 테스트 입력을 찾을 수 있을까? 이런 단순한 버그를 찾는 데 그레이박스 퍼저가 얼마나 효과적일까? 이러한 질문에 답하기 위해 Intel Xeon E3-1231 v3 processor(3.40 GHz)의 single core에서 각각 1시간 동안 6개의 최신 퍼저와 Eclipser로 예제 프로그램을 퍼징했다. 우리는 AFL, AFLFast, AFLGo, LAF-intel을 포함하는 4개의 오픈 소스 그레이박스 퍼저를 선택했다. (Steelix 대신 LAF-intel을 선택했는데, 이는 Steelix가 오픈 소스가 아니기 때문이다. Steelix를 LAF-intel의 improved version으로 볼 수 있다.) 또한 유명한 symbolic executor, 즉 화이트박스 퍼저인 KLEE도 선택했다. KLEE, LAF-intel, AFLGo와 같은 퍼저들은 소스 코드상에서만 동작할 수 있다. 따라서 이들은 소스 코드와 함께 실행했고, 다른 퍼저들은 컴파일된 바이너리에서 실행했다. 예를 들어 AFL은 QEMU mode로 실행했다. AFL GO를 실행할 때는 guidance를 제공하기 위해 주어진 Line 4를 target location으로 지정했다.

Figure 1(b)는 그 결과에 대한 요약이다. 그레이박스 퍼저들 중 LAF-intel만이 buggy 테스트 케이스를 발견했다. LAF-intel은 multi-byte 비교문을 여러 개의 single-byte 비교로 쪼개서 코드 커버리지 metric을 입력 mutation에 효과적으로 민감하게 만들었기 때문에 성공했다. 그러나 LAF-intel은 바이너리 수준의 계측에 비해 더 낮은 오버헤드를 수반하는 소스 기반 계측으로도 버그를 찾는 데 Eclipser보다 671배 느렸다.

특히 결과는 KLEE와 비슷했다. Eclipser는 버그를 찾는 데 KLEE보다 두 배 느리지만 Eclipser는 바이너리 코드에서 직접 실행되는 반면 KLEE는 소스 코드가 필요하다. 또한 기호 실행은 SMT solving으로 인해 더 많은 조건 분기가 발생하므로 속도가 급격히 느려지지만, Eclipser의 경우 복잡한 경로 조건이 성능에 큰 영향을 미치지 않는다. 실제로 Eclipser는 GNU coreutils에서 KLEE보다 훨씬 더 높은 코드 적용 범위를 달성했으며(§V-C에서 논의), Eclipser가 규목 큰 real-world 응용프로그램을 처리하도록 확장(:scale)할 수 있음을 보여준다(§V-E에서 논의).

이는 GCT의 잠재적 가능성을 강조하는 예시이다. 우리의 기술은 화이트박스 퍼징의 정밀도에 비하면 부족함이 있는데, 대신 고비용 분석에 의존하지 않고 PUT의 다양한 고유 실행 경로를 실행하기 위한 테스트 케이스를 빠르게 생성한다는 점에 절충안을 두고 있다.

III. GREY-BOX CONCOLIC TESTING

GCT(Grey-box Concolic Testing)는 주어진 시드 입력에서 테스트 케이스를 생성하는 방법이다. 고수준에서 이는 generational search strategy를 사용하는 동적 기호 실행과 유사하게 동작한다. generational search strategy는 시드를 사용하여 PUT를 실행하면 실행 경로에서 실행 가능한 모든 분기 조건을 확장하여 테스트 케이스 generation을 생성하는 방법이다. GCT는 유사한 방식으로 동작하지만 SMT solving에 의존하지 않고, 경로에서 발생하는 분기 조건을 선택적으로 solve 한다.

우리 접근 방식의 핵심은 시드의 각 입력 바이트마다 근사 경로 제약 조건의 독립적인 subset을 유지하는 것이다. 제약 조건을 resolve하는 것은 PUT의 동일한(또는 유사한) 실행 경로를 실행하는 데 사용할 수 있는 고유한 테스트 케이스를 생성하는 데 도움이 된다. 이러한 테스트 케이스를 통해 경로의 일부 조건 분기가 동일한 실행 경로를 사용하더라도 다른 입력 값을 비교하는 것을 볼 수 있다. 이러한 execution behavior를 사용하여 그레이박스 방식으로 조건부 분기를 통과한다. 우리의 기술은 화이트박스 퍼징과 같이 분기 조건을 효과적으로 해결하는 동시에, 그레이박스 퍼징과 같이 시스템을 가볍고 확장 가능하게 유지한다.

A. Overview

GCT는 네 가지의 주요 함수인 SPAWN, IDENTIFY, SELECT, SEARCH로 동작한다. Algorithm 1은 이런 함수들을 사용하여 GCT의 핵심 알고리즘을 표현한다.

SPAWN $(p, s_p, k) → \text{execs}$
SPAWN은 프로그램 $p$ , 시드 $s_p$ , byte offset $k$ 를 입력으로 한다. 먼저 $s_p$ 의 $k$ 번째 바이트를 수정하여 $N_{\text{spawn}} (=10)$ 개의 고유한 input set을 생성한다. 이때 $N_\text{spawn}$ 은 사용자 매개 변수다. 그런 다음 생성된 입력으로 $p$ 를 실행하고, 실행( $\text{execs}$ )을 반환한다(§III-C 참조).

IDENTIFY $(p, \text{execs}) → \text{conds}$
IDENTIFY는 프로그램 $p$ 와 executions set( $\text{execs}$ )를 입력으로 한다. $k$ 번째 입력 바이트의 영향을 받는 sequence of conditional statements( $\text{conds}$ )를 식별한다(§III-D 참조).

SELECT $(\text{conds}) → \text{conds}^′$
SELECT는 주어진 sequence of conditional statements( $\text{conds}$ )의 subsequence를 반환한다. 현재의 Eclipser 구현에서는 이 단계은 단순히 최대 $N_\text{solve}(=200)$ 개의 랜덤하게 선택된 조건문의 subsequence를 반환한다(§III-E 참조). 이때 $N_\text{solve}$ 는 사용자 매개 변수다.

SEARCH $(p, k, \text{pc}, \text{execs}, \text{cond}) → s_p^′, c$
SEARCH는 주어진 조건문 $\text{cond}$ 를 통과하려고 시도하고, $\text{cond}$ 에서 (제약 조건 $c$ 와 더불어, $σ_p(s_p)$ 가 취하지 않는) new branch를 실행할 수 있는 새로운 시드 $s^′_p$ 를 반환한다. 제약 조건 $c$ 는 현재 실행 $\sigma_p(s_p)$ 를 따르기 위한 input condition이다. 생성된 시드는 $\sigma_p(s_p)$ 와 일치하는 $\text{cond}$ 까지 실행되고, $\text{cond}$ 에서는 opposite branch를 실행한다(§III-F 참조).

고수준에서 CGT는 프로그램 $p$ , 시드 입력 $s_p$ , 바이트 오프셋 $k$ 를 입력으로 사용하고 $\sigma_p(s_p)$ 와 다른 실행 경로를 포함하는 테스트 케이스 set을 출력한다. 일반적인 concolic testing과 달리 우리의 접근 방식은 추가적인 매개 변수 $k$ 를 사용하여 흥미로운 입력 바이트 오프셋을 지정한다. 이는 오프셋 $k$ 에 위치한 단일 입력 필드에만 초점을 맞춰 GCT 프로세스를 단순화하기 위한 것이다. 우리의 초점은 단일 입력 필드에 있지만, 조건이 여러 입력 필드의 영향을 받는 조건 분기를 통과하는 것도 역시 가능하다. 왜냐하면 우리의 전략은 한 번에 하나의 입력 필드에 대해 satisfying assignment를 찾을 수 있기 때문이다. 게다가 SEARCH가 만족하는 해를 찾지 못하더라도, Eclipser는 random mutation을 수행하여 오류를 보상한다(§IV). 이러한 경우를 일반적인 방식으로 처리하는 것은 본 논문의 범위를 벗어난다.

변수 pc는 실행 $\sigma_p(s_p)$ 에 대한 근사 경로 제약을 의미한다. 특히 pc는 $s_p$ 의 바이트에서 해당 바이트에 대한 독립 제약 조건으로의 map이며, 이는 초기에는 empty map이다(Algorithm 1의 Line 2). 근사 경로 제약은 실행 동안에 조건문을 마주칠 때마다 커진다. 이 데이터 구조는 KLEE, Unleashing mayhem on binary code에서 사용된 independent formulas에서 영감을 얻었다.

[KLEE의 경우 symbolic state를 fork하면서 state를 스케줄링 하는 탐색 방법이다.]

GCT는 실행에서 모든 comparison instruction을 계측하지만, 제약 조건 pc를 빌드하기 위해 Line 6에서 이들의 subset만을 선택하여 근사 경로 제약 조건을 생성한다. 선택된 각 조건문에서 corresponding formula를 pc에 추가( $\land$ )한다(Line 9). 이 프로세스는 경로 제약 조건의 근사된 부분집합을 유지한다는 점을 제외하면 동적 기호 실행과 동일하다.

B. Example

우리의 기술을 설명하기 위해, 동기 부여가 되었던 예제를 다시 살펴보자(§II-C). Figure 2는 예제의 code snippet과 그에 대응되는 binary code를 나타내고 있다.

다음을 가정하자.

(1) 초기 시드 파일 $s_p = \{0, 0, 0, 0, 0, 0, 0, 0\}$ . (연속하는 8개의 0).

(2) $N_\text{spawn} = 3$ .

(3) current offset $k = 0$ .

Eclipser는 §IV에서 설명한 대로 fuzzing campaign 전체에서 이 오프셋 $k$ 를 이동하면서 동작한다.

SPAWN이 세 입력 $s_p[0 ← 10]$ , $s_p[0 ← 50]$ , $s_p[0 ← 90]$ 를 생성했다고 가정하자. 그리고 이 입력들을 이용해 프로그램 $p$ 를 실행하면서 다음 세 실행을 생성했다고 하자: $\sigma_p(s_p[0 ← 10])$ , $\sigma_p(s_p[0 ← 50])$ , $\sigma_p(s_p[0 ← 90])$ . 그런 다음 IDENTIFY는 실행에서 첫 번째 cmp 명령어가 integer 31337을 eax의 세 가지 값(21, 101, 181)과 비교하는 것을 관찰한다. 세 개의 overlapping execution prefix에서 IDENTIFY는 comparison instruction pair와 그 뒤에 이어지는 conditional jump instruction을 반환한다. 다음으로 SELECT는 그 comparison insturction pair를 입력으로 하고, 고려할 항목이 하나만 있으므로 단순히 반환한다. 마지막으로 SEARCH는 overlapping execution에서 세 값(10, 50, 90)과 그에 대응하는 compared value(21, 101, 181) 사이의 관계를 확인한다. 이 경우, SEARCH는 eax = 2 × $s_p[0]$ + 1과 같은 선형 관계를 추론한다. 이 수식을 풀어서 intInput이 첫 번째 조건을 만족하는 15668(0x3d34)이라는 값을 얻는다.

그러나 실제 solution은 1 바이트로 표현할 수는 없다. 따라서 첫 번째 바이트( $k = 0$ 이므로)와 그 인접 바이트를 포함하는 corresponding 입력 필드의 크기를 추론해야 한다. 우리는 size 2부터 최대 8 바이트의 입력 크기를 고려한다. 이 경우, 2바이트 솔루션이 동작하고, $s_p$ 의 처음 2바이트를 replace하여 테스트 케이스( $s^′_p$ )를 생성하는 데 사용되며, 그 결과 다음 8 바이트 파일이 다음 16진수 표현으로 생성된다:(34 3d 00 00 00 00 00 00). SEARCH는 이 입력으로 PUT를 실행하여 조건 분기를 통과할 수 있는지 확인한다. 새로운 branch를 실행할 수 있기 때문에, 이 branch에 대한 근사 경로 제약 조건을 포함하는 시드를 반환한다: { $s_p[0] \mapsto$ [0x34, 0x34], $s_p[1]$ $\mapsto$ [0x3d, 0x3d]}(정확한 값을 찾았음을 알 수 있다). 이때 대괄호는 닫힌 구간을 의미한다. §IV-C에서 근사 경로 제약 조건을 인코딩하는 방법을 설명할 것이다.

Eclipser는 이제 $k$ 를 증가시키면서 $s^′_p$ 를 새로운 시드로 사용하여 위 과정을 반복한다. $k = 4$ 면, SPAWN은 다음 세 실행을 반환한다: $\sigma_p$ ( $s^′_p$ [4 ← 10]), $\sigma_p$ ( $s^′_p$ [4 ← 50]), $\sigma_p$ ( $s^′_p$ [4 ← 90]). IDENTIFY는 다섯 번째 입력 바이트 $(k = 4)$ 와 eax 간의 대응 관계를 찾는다.

그런 다음 SEARCH는 eax 값이 $s^′_p[4]$ 에 대해 단조 증가한다는 것을 알아낸다. $k$ 번째 입력 바이트를 변이하여 binary search를 수행하고 eax가 -1에서 1로 변경되는 경우(입력 바이트가 0x42('B')에서 0x43('C')으로 변경될 때)를 찾는다. eax를 0으로 만드는 해를 찾지 못했기 때문에, 입력 필드 크기를 1 확장하고 0x4200과 0x4300 사이에서 다른 binary search를 수행한다. PUT가 조건문의 true branch를 실행하게 하는 해 "Bad!"를 찾을 때까지 이 과정을 반복한다. 마지막으로 SEARCH는 "Bad!" 문자열을 포함하는 시드를 생성한다.

strcmp 동작 과정

#include <stdio.h>
#include <string.h>

void foo(char* strInput) {
	// return the ASCII difference after converting `char*` to `unsigned char*`
	printf("%d\n", strcmp(strInput, "Bad!"));
}

int main() {
	foo("A"); 	foo("B"); 	foo("C");
	// output: -1 -97 1

	foo("Bad "); 	foo("Bad!"); 	foo("Bad\"");
	// output: -1 0 1
}

// EOF

C. SPAWN

SPAWN은 constraint $s_p[k].\text{constr}$ 를 기반으로 시드 $s_p$ 의 $k$ 번째 바이트를 변이하여 테스트 입력을 생성하고 생성된 입력에 대한 $p$ 의 실행을 반환한다. 여기서의 핵심적인 목표는 $\sigma_p(i_1) \approx \sigma_p(i_2) \approx \cdots \approx \sigma_p(i_N)$ 를 만족하는 $N$ 개의 테스트 입력 $\{i_1,i_2,··· ,i_N\}$ 을 생성하는 것이다. 실제로는 SMT solver를 이용해 이러한 입력을 찾는 것이 가능하지만, 우리의 설계 목표 중 하나가 근사적 경로 제약 조건을 경량화하여 해결할 수 있도록 하는 것이다.

Eclipser는 근사 경로 제약 조건을 표현하기 위해 구간(interval)을 사용한다. 따라서 근사 경로 제약 조건을 만족하는 입력을 찾는 것은 구간 내에서 값을 선택하는 것만큼 쉽다. 제약 조건 $s_p[k].\text{constr}$ 가 기호 실행에서와같이 정확하다면, 우리는 항상 PUT의 정확히 동일한 경로를 실행하는 데 사용될 수 있는 고유한 테스트 입력을 생성할 수 있다. 즉, 우리는 $σ_p(i_1) = σ_p(i_2) = · · · = σ_p(i_N )$ 와 같은 입력을 생성할 수 있다. 그러나 우리의 접근 방식은 $s_p[k].\text{constr}$ 의 불완전함 때문에 실제 경로 제약 조건을 만족하지 않는 false input을 생성할 수 있다. IDENTIFY는 overlapping execution prefix에 focus하므로 이는 심각한 문제가 아니다.

우리는 SPAWN이 반환하는 실행의 최대 횟수를 $N_\text{spawn}$ 으로 표기한다. 즉, $N = N_\text{spawn}$ 이다. 이는 분석가가 설정할 수 있는 매개 변수다. 현재 Eclipser 구현에서는 이 값을 기본적으로 10으로 설정한다. 이 값은 경험적 연구를 기반으로 선택되었다(§V-B). 기존의 기호 실행은 PUT를 한 번만 실행하는데 반해, SPAWN은 주어진 시드에 대해 PUT를 $N_\text{spawn}$ 번 실행한다. 이는 scalable fuzzer 설계를 위한 trade-off다.

D. IDENTIFY

IDENTIFY의 주요 목표는 오프셋 $k$ 의 입력 바이트와 $\sigma_p(s_p)$ 의 조건문 간의 대응 관계를 확인하는 것이다. IDENTIFY는 $s_p[k]$ 의 영향을 받는 모든 조건문을 포함하는 $σ_p(s_p)$ 의 subsequence를 반환한다.

목표를 달성하기 위해 fine-grained taint analysis을 사용할 수 있다. 그러나 이는 각 입력 바이트에 identifier를 할당하고 주어진 입력의 영향을 받는 모든 expression에 대해 이러한 ID 집합을 유지하기 때문에 memory-hungry process다. fine-grained taint analysis의 공간 효율성을 줄이는 것에 대한 여러 연구가 있지만, 그 연구들은 set element 사이에 상당한 overlap을 가정한다. 게다가, 오염 분석은 PUT의 모든 single instruction을 계측하므로, 이는 퍼징에서 상당한 계산적 비용을 수반해 느려질 수 있다.

우리는 PUT를 여러 번 실행하는 간단하고 규모 가변적인 접근 방식을 사용한다. SPAWN은 $s$ 의 $k$ 번째 바이트를 변이하여 생성된 테스트 입력을 기반으로 $N_\text{spawn}$ 개의 execution을 반환한다고 했었다. 따라서 실행의 동작 차이를 관찰하여 실행에서 $k$ 번째 바이트와 conditional branch 간의 대응 관계를 식별할 수 있다. 특히, overlapping execution prefix의 동일한 위치에서 conditional statement set을 우선적으로 추출한다. 그런 다음 conditional statement $b$ 의 decision에서 차이를 관찰하여 $b$ 가 시드의 $k$ 번째 바이트에 의해 영향을 받는지를 결정한다. 이 간단한 접근 방식은 실행의 어떤 조건 분기가 입력 바이트의 영향을 받는지에 대한 민감한 피드백을 제공한다.

부분적으로 겹치는(overlap) 실행이 항상 있을 수 있으므로 근사 경로 제약 조건의 부정확성은 여기에서 문제가 되지 않는다. 또한 SPAWN은 변이에 의해 입력을 생성하기 때문에 생성된 실행 중 일부는 완전히 다른 실행 경로를 실행하여 PUT의 흥미로운 경로를 커버할 수 있다. Eclipser는 이러한 부산물(:by-products)로부터 이점을 얻을 수 있다.

Figure 3은 오프셋 10의 바이트 값만 다른 두 개의 입력 $i$ 와 $i^′$ 으로 프로그램 $p$ 를 실행하는 경우를 보여준다. $\sigma_p(i)$ 및 $\sigma_p(i^′)$ 실행의 overlapping prefixes에는 세 개의 조건문 $b_1$ , $b_2$ , $b_3$ 가 있다. 이 예제에서 $b_1$ 과 $b_3$ 에 대한 비교되는 값이 실행에서 서로 다른 것을 관찰할 수 있다. 따라서 우리는 11 번째 입력 바이트( $i[10]$ 와 $i^′[10]$ )가 $b_1$ 및 $b_3$ 에 대응한다는 결론을 내린다.

E. SELECT

IDENTIFY 동안에 처리할 조건문이 너무 많을 수 있다. 동적 기호 실행에서 이런 현상을 경로 폭발 문제(path explosion problem)라고 한다. 예를 들어, 다음 for loop을 고려해 보자. 여기서 inp가 user-supplied input을 나타낸다.

for (i=0; i<inp; i++) { /* omitted */ }

이 경우, 사용자 입력에 따라 임의의 수의 조건문을 마주칠 수 있다. 만약 IDENTIFY가 반환하는 모든 single statement를 처리한다면, 시스템은 주어진 시간 내에 흥미로운 경로를 탐색하지 못할 것이다.

이런 문제에 대처하기 위해서, SELECT는 그들의 appearance 순서를 유지하면서 주어진 조건문 sequence 중에서 임의의 $N_\text{solve}$ 개의 조건문을 선택한다. 프로그램이 실행되는 동안 근사 경로 제약 조건을 build해야 하기 때문에, 순서를 동일하게 유지해야 한다. Eclipser의 현재 구현에서, 경험적 연구를 기반으로 $N_\text{solve} = 200$ 으로 결정했다(§V-B). SAGE나 KLEE와 같은 dynamic symbolic executor도 동일한 문제를 처리하기 위해 여러 경로 선택 휴리스틱을 사용한다.

F. SEARCH

SEARCH는 주어진 조건문 cond에서 new branch를 커버하기 위해 분기 조건문을 resolve해야 한다. 그 결과 SEARCH는 현재 실행 경로 $σ_p(s_p)$ 를 따르기 위해 interval(§IV-C)로 근사된 분기 조건과 함께 새로운 시드를 반환한다. 여기서 주요 과제는 SMT solver의 도움 없이 근사 경로 제약 조건을 solve하는 것이다.

IDENTIFY는 $k$ 번째 입력 바이트와 관계가 있는 조건문을 반환한다. 우리는 이 관계를 입력이 $s_p[k]$ 이고 출력이 각 조건문의 operand 중 하나로 표현되는 data flow abstraction으로 표현할 수 있다. SEARCH에서의 핵심 직관은 이러한 input-output 관계를 실현함으로써, 근사 경로 제약의 잠재적인 해를 추론할 수 있다는 것이다.

특히 SEARCH는 입출력의 관계가 선형적이거나 단조적인 경우에 중점을 둔다. 이 설계 결정은 다양한 이전 연구들과 우리의 경험적 관찰에 의해 뒷받침된다. real-world 프로그램의 많은 조건 분기들이 선형적이거나 단조적인 제약 조건인 경향이 많다는 것을 관찰했다(§V-C1).

SEARCH는 다음 세 단계로 실행된다:

현재 분기 조건을 공식화하고 solve한다. (§III-F1)

그에 대응하는 입력 필드를 인식한다. (§III-F2)

조건문을 통과할 수 있는 새로운 시드를 생성한다. (§III-F3)

1) Solving Branch Condition

일반성을 잃지 않고(w.l.o.g) cond의 두 operand 중 오직 하나만이 input $i$ 의 영향을 받는다고 가정하자. 여기서 이 operand를 ${oprnd}(i)$ 라고 표기하겠다. 그러면 ${oprnd(i_1)-oprnd(i_2) \over i_1 - i_2} = {oprnd(i_2)-oprnd(i_3) \over i_2 - i_3}$ 를 만족하는 $i_1$ , $i_2$ , $i_3$ 이 존재하면 cond의 분기 조건이 선형이라고 결정할 수 있다. 이 경우, 선형 방정식이나 선형 부등식을 직접 구성하고 해를 구할 수 있다. 반면 $oprnd$ 가 cond를 실행한 모든 관찰된 입력 $i_1 , i_2 , ..., i_n (n \ge 3)$ 에 대한 단조 함수인 경우 cond는 단조 분기 조건을 갖는다. Figure 4는 두 바이트의 입력 필드(input)과 비교된 값(ebx)이 단조 입출력 관계를 갖는 경우의 예제를 나타내고 있다. 이런 단조 관계에서는 binary search를 수행하여 해를 구한다.

2) Recognizing Input Field

지금까지 우리의 초점은 입력 바이트, 즉 $s_p[k]$ 에 있었다. 그러나 많은 분기 조건이 입력 바이트뿐만 아니라 입력 필드(예: 32-bit 또는 64-bit integer)에 의해 제한된다. 이는 SEARCH가 임의의 크기의 입력 필드를 처리해야 한다는 것을 의미한다. 게다가 SEARCH에서 방정식을 푸는 연산은 임의의 정밀도 정수(arbitrary-precision integer)에서 작동하므로, 바이트에 맞지 않는 해를 제공할 수도 있다. 우리는 더 많은 입력 후보로 PUT를 실행함으로써 SEARCH의 능력을 확장할 수 있다. 구체적으로, 특정 크기의 해를 고려하면서 구한 해로 시드를 교체할 수 있다. 선형 방정식이나 부등식을 풀 때는 가능한 모든 후보를 시도하기 위해 최대 7개의 경우를 고려한다(Figure 5). 단조 조건에 대한 binary search의 경우 입력 필드의 크기를 1로 고려하여 search를 시작하여 임계값(:threshold)까지 (현재 구현에서 8로 설정) 크기를 점차 증가시킨다.

3) Seed Generation

새 경로를 실행하는 새로운 시드를 생성하려면 먼저 현재 분기의 제약 조건을 근사하고, 새로 생성된 시드의 $constr$ 필드로 인코딩해야 한다. 구체적으로, 분기 조건을 dictionary $c$ 로 변환하는데, 이 $c$ 는 입력 바이트 위치 $i$ 를 구간 $c[i]$ 에 매핑한다. $c$ 의 모든 바이트 위치 $i$ 에 대해, $s_p[i].\text{constr}$ 를 $\lnot c[i] ∧ pc[i]$ 로 업데이트한다. 여기서 $\land$ 는 두 구간의 conjunction을 의미한다. $s_p[i]$ 의 concrete value도 구간 $\lnot c[i]$ 내에 있는 값으로 업데이트된다. 현재 실행에서 가지 않는 경로로 가보기를 원하기 때문에 각 분기 조건 $\lnot c[i]$ 의 부정을 취한다. 즉, 새로운 시드가 PUT로 실행될 때 opposite branch로 인도해야 한다. SEARCH는 $c$ 를 반환하고, 이는 $pc$ 를 build하는 데 사용된다. 발견된 분기 조건을 근사하는 방법에 대한 자세한 내용은 §IV-C를 참조하라.

IV. ECLIPSER ARCHITECTURE

GCT는 그 자체만으로 주어진 시드 $s_p$ 와 바이트 위치 $k$ 에서 $p$ 에 대한 체계적인 테스트 케이스 생성은 가능하지만, 흥미로운 경로를 탐색하기 위해 다양한 바이트 위치와 다른 시드를 사용하여 GCT를 실행하는 방법을 고안해야 한다. 본 절에서는 Eclipser 설계에서 이러한 문제를 해결하는 방법을 설명한다.

A. Main Algorithm

§III-F를 상기해보면, 현재 GCT는 선형 및 단조 제약 조건에만 초점을 맞추고 있으며, 여러 입력 필드를 포함하는 일부 복잡한 분기 조건을 처리하지 못할 수도 있다. 이러한 문제들에 대처하기 위해, Eclipser는 고전적인 그레이박스 퍼징의 전략을 사용한다. 우리의 목표는 GCT와 그레이박스 퍼징을 교대로 사용하여 이 둘의 능력을 최대화하는 것이다. 퍼징 전략을 번갈아 사용하는 아이디어는 이전에 제안된 바 있으며 본 연구와 상호 보완적이다.

Algorithm 2는 Eclipser의 전체 과정을 나타낸 그림이다. Eclipser는 프로그램 $p$ , 시간제한 $t$ , 초기 시드 set $seeds$ 를 입력으로 받아 fuzzing campaign 동안 생성된 테스트 케이스 set $T$ 를 반환한다. Eclipser는 먼저 제공된 초기 시드 seeds로 우선순위 큐 $Q$ 를 초기화하고, 시간제한 $t$ 가 만료될 때까지 while loop에서 실행한다. Line 5에서 Schedule은 grey-box concolic testing( $R_G$ )과 grey-box fuzzing( $R_R$ )을 위한 리소스를 할당한다. 그런 다음 두 퍼징 전략, 즉 GCT(GreyConcolicLoop)와 그레이박스 퍼징(RandomFuzzLoop)은 할당된 모든 리소스를 사용할 때까지 새로운 테스트 케이스를 교대로 생성한다. 리소스 관리에 대한 자세한 내용은 §IV-B를 참고하라. Eclipser는 GreyConcolicLoop와 RandomFuzzLoop에서 단순히 새로 생성된 테스트 케이스, 즉 시드를 $Q$ 및 $T$ 에 각각 추가하는 방식으로 $Q$ 와 $T$ 를 업데이트 한다. $T$ 는 나중에 fuzzing campaign이 끝나면 메인 알고리즘에서 반환된다(Line 8).

Priority Queue.

생성된 각 테스트 입력에 대해 Eclipser는 코드 커버리지를 기반으로 fitness를 평가하고 테스트 케이스를 $Q$ 에 추가한다. 구체적으로, 새로운 노드를 커버하는 시드에게 높은 우선순위를 부여하고, 새로운 경로를 커버한 시드에는 낮은 우선순위를 부여한다. 코드 커버리지를 향상시키지 않은 시드는 삭제한다. Eclipser는 사용할 다음 값 $k$ 와 함께 시드를 큐에 삽입한다. Eclipser는 current $k$ 를 $k-1$ 및 $k+1$ 로 만들고, 두 위치에서 시드를 두 번 push 한다. 우선순위 큐의 중요한 측면 중 하나는 두 퍼징 전략이 시드를 공유할 수 있다는 것이다. 지금의 GCT는 새로운 테스트 케이스를 생성할 때 주어진 시드의 크기를 확장하지 않는 반면, 그레이박스 퍼징은 가능하다. 그레이박스 퍼징 모듈이 길이를 확장하여 흥미로운 시드를 생성하면, 그 시드는 우선순위 큐 $Q$ 를 통해 GCT 모듈과 공유된다.

B. Resource Scheduling

두 퍼징 전략을 번갈아 사용할 때 각 전략에 얼마나 많은 리소스를 할당할지 결정해야 한다. Eclipser에서 리소스는 허용된 프로그램 실행 횟수다. 만약 어떤 전략이 PUT를 허용된 횟수보다 더 많이 실행하면, Eclipser는 다른 전략으로 스위칭한다. 스위치 타이밍을 결정하기 위해, Eclipser는 각 퍼징 전략의 효율성을 평가하고 그에 비례하여 시간을 할당한다. $N_\text{exec}$ 를 while loop의 한 번의 iteration에 대한 총 프로그램 실행 횟수라고 하자(Algorithm 2의 Line 4). 우리는 효율성 f를 $f = N_{path} /N_{exec}$ 라고 정의한다. 이때 $N_\text{path}$ 는 새로운 실행 경로를 실행한 고유한 테스트 케이스의 개수다. 즉, Eclipser는 더 많은 새로운 경로를 탐색하는 전략에 더 많은 리소스를 할당한다.

C. Approximate Path Constraint

GCT는 경로 제약 조건을 구간으로 근사한다는 것을 상기해 보자. 근사 경로 제약 조건은 입력 바이트에서 해당 interval constraint 으로의 매핑이다. 우리는 각 제약 조건을 closed interval로 나타낸다. $[l, u]$ 를 제약 조건 $l \le x \le u$ 라고 하자. 그러면 두 제약 조건의 논리적 결합(:conjunction)을 두 구간의 교집합으로 다음과 같이 표현할 수 있다: $[l_1, u_1] ∧ [l_2, u_2] = [max(l_1, l_2), min(u_1, u_2)]$ . SEARCH가 $n$ 바이트 입력 필드 $x$ 와 관련된 분기 조건을 resolve하고 결과적으로 equality condition $x = k$ 를 구했다고 가정하자. 이 조건은 정밀도를 잃지 않고 다음과 같이 각 바이트에 대한 구간으로 표현될 수 있다: $\{x_0 \mapsto [k_0, k_0], x_1 \mapsto [k_1, k_1], \cdots , x_{n−1} \mapsto [k_{n−1}, k_{n−1}]\}$ . 이때 $k_i = (k \gg (8∗i))\ \&\ \text{0xff}$ 이고, $x_0$ 은 $x$ 의 least significant byte, $x_{n-1}$ 은 $x$ 의 most significant byte를 의미한다.

resolved branch condition이 inequality condition $l \le x \le u$ 라고 가정하자. 이 경우 조건은 $x$ 의 most significant byte에 대한 구간 제약으로 근사된다: $\{x_{n−1} \mapsto [l_{n−1} , u_{n−1} + 1]\}$ . 여기서 "integer" 타입으로 표시되는 구간을 over-approximate하기 위해 최상위 바이트만 선택한다. Eclipser는 element별 conjunction을 수행하여 이 근사 제약 조건을 pc에 추가한다(Algorithm 1의 Line 9).

D. Implementation

Eclipser의 메인 알고리즘을 4.4k 라인의 F# 코드로 구현하고 QEMU(2.3.0)에 800라인의 C 코드를 추가하여 Eclipser의 바이너리 계측 로직을 구현했다. 우리는 본질적으로 AFL의 단순화된 버전인 Eclipser의 그레이박스 퍼징 모듈을 F#으로 작성했다. 우리는 AFL에서 사용되는 mutation 연산을 사용했고, fuzzing campaign 동안 시드 수를 최소화하기 위해 greedy-set-cover 알고리즘을 사용했다. 바이너리 실행에서 실행 피드백을 얻기 위해 QEMU user mode emulation을 사용했는데, 이는 다양한 아키텍처를 처리하도록 Eclipser를 쉽게 확장할 수 있기 때문이다. 현재 Eclipser는 널리 사용되는 세 가지 아키텍처 x86, x86-64, ARMv7을 지원한다. Eclipser 구현은 GitHub에서 공개적으로 사용할 수 있다. 단 ARMv7 버전은 IP 문제로 인해 오픈소스 하지 않을 것이다.

https://github.com/SoftSec-KAIST/Eclipser-Artifact

V. EVALUATION

다음 질문들에 답하기 위해 Eclipser를 평가했다.

Eclipser의 configuration parameter는 성능에 어떤 영향을 주는가? (§V-B)

GCT가 일반적인 테스트 케이스 생성 알고리즘이 될 수 있는가? 그렇다면 기존 화이트박스 퍼저와 비교하면 어떠한가? (§V-C)

Eclipser가 버그를 찾는 데 있어서 최신의 그레이박스 fuzzer들을 능가할 수 있는가? (§V-D)

Eclipser가 실제 애플리케이션에서 새로운 버그를 찾을 수 있는가? GCT는 그러한 크고 복잡한 프로그램을 처리할 만큼 충분히 scalable한가? (§V-E)

A. Experimental Setup

private cluster of 64 VM에서 실험을 진행했다. 각 VM은 single Intel Xeon E5-2699 V4 (2.20 GHz) core와 8GB of memory를 장착했다. 세 가지 벤치마크에 대한 실험을 수행했다. (1) 95 programs from GNU coreutils 8.27. (2) 4 programs from LAVA-M benchmark. (3) 22 real-world programs included in Debian 9.1 packages.

먼저 Eclipser와 KLEE를 비교하기 위해 GNU coreutils를 선택했는데, 이는 KLEE 및 기타 화이트박스 fuzzer가 성능을 평가하기 위해 이 벤치마크를 사용하기 때문이다. 두 번째로, Grey-box fuzzer들과 Eclipser의 buf finding 능력을 평가하기 위하여 기존의 많은 fuzzer를 평가하는 데 사용되는 LAVA-M 벤치마크를 이용했다. 마지막으로 Eclipser의 실무에서의 능력을 평가하기 위해 Debian 9.1에서 선택한 real-world 응용프로그램을 퍼징했다.

Comparison Targets.

우리는 비교를 위해 두 가지 기존 그레이박스 fuzzer AFLFast와 LAF-intel을 선택했다. Driller는 현재 ELF 바이너리에 대한 지원이 제한되어 있어 제외했다. VUzzer는 상용 제품인 IDA pro에 의존하기 때문에 실행할 수 없었다. Steelix, T-Fuzz, Angora도 공개되지 않았기 때문에 제외했다.

B. Eclipser Configuration

§III를 상기해보면, Eclipser는 사용자가 config 가능한 두 가지 매개변수 $N_\text{spawn}$ 와 $N_\text{solve}$ 를 사용한다. 이 두 매개변수는 각각 GCT로 identify하고 penetrate할 분기의 수를 결정한다. 매개변수의 영향을 추정하기 위해 첫 번째 벤치마크(coreutils 8.27)의 각 프로그램에서 한 시간 동안 다양한 config와 측정된 코드 커버리지 차이로 Eclipser를 실행했다. 특히 각 매개변수에 대해 기하급수적으로 증가하는 5개의 값을 선택했다.

Figure 6은 결과에 대한 요약을 나타낸 그림이다. $N_\text{spawn}$ 이 너무 작으면 IDENTIFY가 흥미로운 조건 분기를 식별하지 못해서 결과적으로 커버리지가 줄어들고, 너무 크면 Eclipser가 불필요한 프로그램 실행에 너무 많은 시간을 소비하게 된다. 이와 유사하게, $N_\text{solve}$ 가 너무 작으면 Eclipser에서 몇 가지 흥미로운 조건 분기를 놓치고, 너무 크면 경로 폭발로 인해 더 적은 노드를 커버한다.

이 결과에서 $N_\text{spawn} = 10, N_\text{solve} = 200$ 을 Eclipser의 기본 매개변수 값 set으로 사용하기로 결정했고, 이를 나머지 실험에 사용했다.

C. Comparison against White-box Fuzzing

test case generation algorithm으로서 GCT의 효율성을 평가하기 위해 화이트박스 퍼저 KLEE와 비교했다. (작성 당시 최신 버전 1.4.0과 비교). KLEE의 원본 논문과 마찬가지로 coreutils를 벤치마크로 선택했다. coreutils 8.27의 107개 프로그램 중 퍼징 프로세스 자체에 영향을 줄 수 있는 8개 프로그램을 제외했다(kill, rm과 KLEE에서 unhandled exception을 발생시킨 4개의 프로그램). 남은 95개의 프로그램을 각 한 시간씩 테스트했다. 추가적으로 KLEE를 실행할 때는 KLEE website에서 제시한 명령어 옵션을 사용했다. 공정한 비교를 위해 Eclipser를 실행할 때 입력 크기에 동일한 제한을 설정했다. 여기에 나와있는 모든 숫자는 8번 반복한 결과에 대한 평균값이다.

다음 세 가지 질문에 답을 찾으려고 했다.

GCT가 그레이박스 퍼징 모듈 없이 그 자체만으로 코드 커버리지 측면에서 KLEE를 능가할 수 있는가?

GCT를 그레이박스 퍼징과 번갈아 가면서 사용하는 전략이 이점이 있는가?

Eclipser가 coreutils에서 현실적인 버그를 찾을 수 있는가? 이를 어떻게 KLEE와 비교할 것인가?

1) Grey-box Concolic Testing Effectiveness

Eclipser를 두 가지 다른 모드로 실행했다. (1) GCT만 사용하기 (2) 그레이박스 퍼징만 사용하기. Figure 7의 파란색 선과 분홍색 선이 각 모드에 대한 커버리지를 나타내고 있다. 총 32,223개의 소스 라인 중 GCT는 20,737라인(64.36%), 그레이박스 퍼징 모듈 단독 사용은 18,540라인(57.54%), KLEE는 20,445라인(63.45%)을 커버했다. 이 결과는 GCT 단독 사용이 KLEE와 비교할 수 있음을 나타낸다. 우리 도구는 바이너리 실행 파일에서 직접 실행되는 반면 KLEE는 소스 코드에서 실행된다. 이 결과는 선형 또는 단조 분기 조건을 해결하는 데 중점을 둔 (GCT의) 설계 결정이 경험적으로 옳았음을 보여준다.

(그래프의 마지막 약 60분 동안 KLEE의 라인 커버리지가 급격히 증가했다고 해서 KLEE가 해당 포인트 주변에서 코드를 빠르게 탐색하기 시작한다는 의미는 아니다. KLEE는 시간제한이 만료되면 기호 실행이 완료되지 않은 경우라도 메모리에 남아 있는 테스트 케이스를 출력한다. 실제로 KLEE를 6시간 이상 더 실행했지만 적용 범위는 2.10%만 증가했다.)

2) Alternation between Two Strategies

Figure 7의 초록색 선은 Eclipser가 두 전략을 번갈아 사용하면서 달성한 소스 라인 커버리지를 나타낸다. 이는 두 전략을 교대로 사용하는 설계 결정이 실제로 시너지 효과를 보임을 알 수 있다. Eclipser는 23,499줄(72.93%)을 커버하여 코드 커버리지 측면에서 KLEE를 능가했다. Eclipser의 Coverage 표준편차는 0.54%, KLEE의 Coverage 표준편차는 0.49%였다. 또한 Figure 8은 각 프로그램에 대한 Eclipser와 KLEE의 커버리지 차이를 보여주고 있다. x 축은 테스트된 프로그램이고, y 축은 Eclipser가 KLEE보다 더 많은 라인을 커버했음을 보여준다. 맨 왼쪽 프로그램은 stty로 KLEE가 66줄을 더 커버했고, 가장 오른쪽 프로그램은 vdir로 Eclipser가 554줄을 더 커버했다.

3) Real Bugs from coreutils

GNU coreutils의 프로그램들이 많은 테스트를 거쳤다. Eclipser는 그 안에서 의미 있는 버그를 찾을 수 있는가? 실험 과정에서 Eclipser는 unkown 버그 두 가지를 발견했으며, 각각 b2sum 및 stty에 크래시를 일으킬 수 있다. 반면 KLEE는 실험 중에 버그 중 하나만 발견했다. 이 결과는 Eclipser의 실용성을 보여준다.

D. Comparison against Grey-box Fuzzers

Eclipser를 최신 그레이박스 fuzzer와 비교하면 어떤가? 이 질문에 답하기 위해 Eclipser의 버그 찾기 능력을 최신 그레이박스 퍼저와 비교하기 위해 LAVA-M을 이용했다. §V-A에서 우리는 이 실험을 위해 Steelix와 VUzzer를 실행할 수 없었다고 했었다. 대신, 다른 fuzzer들과 비교하기 위해 그들의 논문에 보고된 숫자를 사용했다. 공정성을 위해 Steelix가 사용한 것과 유사한 설정으로 fuzzer를 실행했다. Steelix 논문에서 사용한 것과 동일한 초기 시드를 사용하고 동일한 시간(5시간) 동안 실험을 진행했다.

Table I는 LAVA-M 벤치마크에서 발견된 버그의 수를 보여준다. Eclipser는 LAF-intel, VUzzer 및 Steelix보다 각각 18.3배, 13.3배, 4.7배 더 많은 버그를 발견했다. AFLFast는 실험 중에 버그를 찾지 못했다. 일부 프로그램에서 Eclipser는 LAVA 작성자가 reproduce하지 못한 버그도 찾을 수 있었다. 예를 들어, base64에서 LAVA의 작성자는 LAVA 논문에서 44개의 버그만 재현할 수 있다.

LAF-intel은 바이너리 기반 도구에 비해 계측 오버헤드가 적은 소스 기반 퍼저다. 예를 들어, LAVA-M 벤치마크에서 AFL을 실행했을 때 소스 기반 계측을 사용한 초당 실행 횟수는 평균적으로 바이너리 기반 계측보다 9.3배 더 높았다. 이러한 단점에도 불구하고 Eclipser는 LAF-intel보다 훨씬 더 많은 버그를 발견했다. 이 결과는 GCT가 LAVA-M에 의해 주입된 버그를 유발하는 복잡한 조건을 효과적으로 해결할 수 있음을 보여준다.

E. Fuzzing in the Real World

real-world의 다양한 프로그램에서 Eclipser를 추가로 평가했다. 구체적으로, 다음 단계에 따라 Debian OS에서 22개의 프로그램을 수집했다. 첫째, CLI를 통해 이미지, 오디오, 비디오를 처리하는 C 프로그램이 포함된 패키지를 검색하기 위해 debtags를 사용했다. 다음으로, Debian popularity contest를 기반으로 인기 있는 상위 30개 패키지를 선택했다. 그런 다음 (1) 파일을 입력으로 받고 (2) LAF-intel로 컴파일할 수 있고 (3) 오류 없이 AFLFast로 퍼징할 수 있는 패키지만 수동으로 선택했다. 마지막으로 각 패키지에서 최대 2개의 프로그램을 추출하여 총 22개의 프로그램을 얻었다. 각 프로그램을 16개의 연속적인 NULL 바이트로 구성된 더미 시드를 이용해 24시간 동안 퍼징했다.

Table II는 그 결과를 보여준다. 전반적으로 Eclipser는 node(branch)를 AFLFast의 1.43x(1.44x)배, LAF-intel의 1.25x(1.25x)배 더 많이 커버했다. 결과를 조사하면서 Eclipser의 GCT가 실제로 높은 커버리지를 달성하는 데 중요한 역할을 했음을 확인했다. 예를 들어 oggenc에서 Eclipser는 AFLFast보다 3.8배 더 많은 노드를 커버했는데, 이는 GCT가 처음부터 FLAC 또는 RIFF 형식에 대한 유효한 서명을 성공적으로 생성했기 때문이다.

우리는 추가적으로 발견한 크래시를 조사했고, 수동으로 분류한 결과 51개의 고유한 버그를 식별했다. Eclipser, AFLFast, LAF-intel는 각각 40, 10, 25개의 고유한 버그를 발견했다. 우리는 결과를 추가로 분석했고, GCT가 실제로 버그를 찾는 데 중요한 역할을 한다는 것을 발견했다. 순정 AFL에 가까운 Eclipser의 그레이박스 퍼징 모듈로만 동일한 실험을 수행한 경우 24시간 후에 8개의 고유한 버그만 찾을 수 있었다. 즉, GCT는 Eclipser가 5배 더 많은 고유한 버그를 찾는 데 도움이 되었다. Eclipser가 발견한 모든 버그를 개발자에게 보고했으며, 본 논문 작성 당시 총 8개의 새로운 CVE가 할당되었다. 이는 실무에서 Eclipser의 영향을 보여준다.

VI. DISCUSSION

현재 GCT 설계는 comparison operand가 입력 필드의 선형 또는 단조 함수로 표현될 수 있는 분기 조건을 해결하는 데 중점을 두고 있다. Eclipser는 현재 복잡한 제약 조건이 있는 분기를 통과하기 위해 전통적인 그레이박스 퍼징에 의존하고 있음을 기억하자. 하지만 비선형 제약 조건을 해결하는 것이 어렵기 때문에 이것은 중요한 결함은 아니다. 그러나 §VII에서 논의한 메타휴리스틱 기반 알고리즘을 채택할 수 있다.

Eclipser는 현재 바이너리 기반 계측을 사용하여 소스 코드 없이 다양한 프로그램을 테스트할 수 있다. 그러나 §V-D의 실험 중 하나에서 관찰한 것처럼 바이너리 기반 계측은 상당한 오버헤드를 발생시킨다. 소스 기반 계측을 채택하여 Eclipser의 성능을 향상시키는 것은 간단하다.

VII. RELATED WORK

Eclipser는 그 자체로 fuzzer가 아니지만 fuzzing 모듈을 사용한다. 따라서 퍼징에 대한 모든 훌륭한 연구는 실제로 우리의 연구와 상호 보완적이다.

GCT는 화이트박스 퍼징에서 영감을 얻었으므로 자연스럽게 경로 폭발 문제가 발생한다. 경로 폭발 문제에 대처하기 위해 다양한 검색 전략이 제안되었다. 예를 들어 KLEE는 임의 경로 선택을 채택하는 데 반해, 다른 연구들에서는 이동이 적은(less traveled) 실행 경로 또는 노드의 우선순위를 지정하거나 정적 분석을 활용하여 검색을 guide한다. Eclipser는 'Automated whitebox fuzz testing'에서와 유사한 접근 방식을 따르지만 더 복잡한 전략을 채택하는 것이 유망한 future work이라고 생각한다. 한편, 화이트박스 퍼징의 scalability를 높이기 위한 시도는 state merging 등 여러 가지가 있다. 대조적으로, 우리의 작업은 주로 symbolic formulas를 구성하고 solve하기 위한 기본 오버헤드를 완화하는 데 중점을 둔다.

비용이 많이 드는 data flow analysis 없이 프로그램을 분석하는 아이디어는 다양한 context에서 연구되었다. 예를 들어, MUTAFLOW는 단순히 source point에서 입력 데이터를 mutate하고 sink point에서 출력 데이터에 영향을 미치는지 관찰함으로써 오염 분석 없이 정보 흐름을 감지한다. Helium은 회귀 분석을 사용하여 코드 세그먼트의 입력과 출력 간의 관계를 추론한다. 이러한 동적 분석은 알려지지 않은 라이브러리 함수 또는 루프가 있는 경우 기호 실행을 보완하는 데 사용된다. 우리의 연구는 이러한 아이디어를 확장하고 더 적극적으로 적용하여 일반적인 테스트 케이스 생성 알고리즘을 고안한다.

Angora와 SBF는 우리와 가장 가까운 퍼저다. 그들은 motivation example(§II-C)에서 논의된 분기 침투 문제(:branch penetration issue)를 다루기 위해 검색 기반 소프트웨어 테스팅의 아이디어를 적용한다. 특히, Angora는 조건 분기의 branch distance를 최소화하는 입력을 찾으려고 시도한다. Angora는 fine-grained 오염 분석을 사용하여 대상 조건 분기에 영향을 미치는 입력 바이트를 식별하는 반면, Eclipser는 PUT을 반복적으로 실행하여 이러한 관계를 동적으로 추론한다. 따라서 우리는 두 접근 방식이 서로 보완적이라고 믿는다. 예를 들어, 먼저 간단한 분기 조건에 침투하기 위해 GCT를 적용한 다음 더 복잡한 조건을 처리하기 위해 Angora의 전략으로 전환할 수 있다.

VIII. CONCLUSION

본 논문은 퍼징의 design space에 새로운 관점을 제시한다. 제안한 기법인 GCT는 경로 기반 테스트를 수행하면서 SMT solver에 의존하지 않고 화이트박스 퍼징을 효과적으로 어둡게(:darkens) 한다. 우리는 Eclipser라는 시스템에서 기술을 구현하고 coreutils, LAVA-M을 포함한 다양한 벤치마크와 Debian의 22개 프로그램에서 이를 평가했다. 우리는 우리 기술이 코드 커버리지와 발견된 버그 수 모두에서 현재 최신의 도구와 비교하여 효과적임을 보여주었다.

Uploaded by Notion2Tistory v1.1.0

[논문 리뷰] Fight against 1-day exploits: Diffing Binaries vs Anti-diffing Binaries (0)	2022.01.22
Git Source Code Review: Diff Algorithms (0)	2022.01.22
[논문 리뷰] 소프트웨어 보안과 바이너리 분석 (0)	2021.03.04
[논문 리뷰] Reflections on Trusting Trust - 어디까지 신뢰할 것인가? (0)	2021.03.04
[논문 리뷰] DIFUZE : Interface Aware Fuzzing for Kernel Drivers (0)	2021.02.22

topcue

[논문 리뷰] Grey-box Concolic Testing on Binary Code 본문

[논문 리뷰] Grey-box Concolic Testing on Binary Code