이 글은 Linear-time Temporal Logic guided Greybox Fuzzing 논문을 바탕으로 정리한 것입니다.
Abstract
소프트웨어 모델 체킹 및 런타임 체킹은 소프트웨어 시스템의 시간적인 속성을 확인하기 위해 널리 사용되는 기술이다.
이러한 기술은 주로 '버그 찾기' 즉, 시간적인 속성 위반을 찾는 실제 응용에서 주로 사용된다.
이 논문은 선형 시간 시계열 논리, 즉 LTL 속성 위반을 찾기 위한 그레이박스 fuzzing framework에 대해 소개하고 있다.해당 프레임워크는 C/C++ 로 작성된 순차 프로그램과 LTL 속성을 입력으로 받는다. 이후 상태를 가진 소프트웨어 시스템에서 LTL 속성 위반 또는 counterexample trace를 찾는다.
하지만 이 자체로 검증이 되지는 못하며, 소프트웨어 시스템에서 임의의 복잡한 이벤트 순서를 추적하기 위해 지향된 그레이박스 퍼징을 확장한 것에 해당한다.기존의 그레이박스 퍼징 접근 방식은 reaching a location이나 use-after-free와 같이 단순한 이벤트 순서를 증명하는데 한정되어 있었다.
모델 체커와 비교하면 논문에서 제공하는 방법은 빠르게 반례를 찾아내서 주어진 시간 내에서 더 많은 반례를 찾아낼 수 있다. AFL 퍼지를 기반으로 한 LTL-Fuzzer 도구는 OpenSSL 및 Telnet과 같은 잘 알려진 프로토콜 구현에서 버그를 검출하는데 효과적이다. 논문에서는 LTL-Fuzzer를 사용하여 잘 알려진 취약성(CVE)를 재현하고, RFC(12 CVE가 할당된)에서 추출된 속성을 확인하여 15개의 zero-day bugs를 찾고 실제 프로토콜 구현에서의 한정성 위반을 찾는다.
Introduction
소프트웨어 모델 체킹은 소프트웨어 시스템에 대한 인기 있는 유효성 검증 방법이다. 이 방법은 프로그램 실행에서 이벤트 순서를 제한하는 logic property를 자동으로 확인하는 기술이다. 모델 체킹은 일반적으로 state space explosion 문제를 겪는다. 이는 기본적으로 infinite state인 소프트웨어 시스템에서 더욱 악화된다. 이를 극복하기 위해, research community는 프로그램 데이터 메모리의 술어 추상화와 추상화 개선을 통해 finite state state abstraction으로 자동으로 유도하는 방법을 탐구했다. model checking 실행 중, 카운테 예제 trace가 발견되면 이 trace를 분석하여 추상화로 인해 도입된 가짜 반례인지 혹은 반례를 유발하는 원인/ 버그인지 확인할 수 있다.
Runtime verification은 가벼우면서도 엄격한 검증 방법으로 모델 체킹을 보완한다. 런타임 검증에서는 시스템의 단일 실행이 동적으로 formally specified properties를 검증한다.(Ex. temporal logic properties). 구체적으로, formal properties는 시스템의 올바른 동작을 지정하고 있는 내용이다. 그런 다음 시스템은 확인 중인 속성과 관련된 이벤트를 캡처하기 위해 instrumented 된다. 런타임동안, 모니터는 이벤트를 수집하여 실행 트레이스를 생성하고 해당 트레이스가 지정돤 속성과 일치하는지 확인하며 속성이 위반될 때 이를 보고한다. 이 방법은 소프트웨어 시스템에 대한 모델을 구축하지 않고 런타임에서 소프트웨어 시스템을 검증하려는 시도이다. 그러나 효과적인 execution traces를 생성하려면 소프트웨어 시스템에 많은 입력이 필요하다. 이러한 입력은 수동으로 얻거나 무작위 생성을 통해 얻어지며, 따라서 런타임 검증은 속성 위반을 드러내기 위한 과정에서 더 많은 manual effort와 useless inputs을 탐색하게 될 수 있다.
모델체킹과 런타임 체킹과 병행하여, greybox fuzzing methods도 최근 많은 발전을 이루었다. 이러한 방법들은 프로그램 입력 도메인에서 편항된 무작위 검색을 수행하여 버그 또는 취약점을 찾는다. greybox fuzzing의 주요 장점은 대규모 소프트웨어 시스템에 대한 확장성에 있다. 그러나 greybox fuzzing은 검증이 아닌 테스트 방법이며 주로 충돌 또는 오버플로우와 같은 간단한 oracles에 대한 증거를 찾는데 유용하다. 최근에는 greybox fuzzing 방법의 확장이 특정 location에 도달하는 테스트와 같은 더 복잡한 oracle을 생성하도록 확장되었다. 그러나 복잡한 temporal property를 충족하는 입력과 트레이스를 생성하는 것은 현재의 greybox fuzzing 도구로는 어려운 과제이다. 따라서 현재의 greybox fuzzing 기술은 소프트웨어 모델 확인 및 런타임 확인의 버그 찾기 능력을 대체할 수 없다.
이 논문에서는 소프트웨어 모델 체킹, 런타임 체킹 및 그레이박스 퍼징 간의 상호작용을 이해하는데 있어 한 걸음 더 나아간다. sequential program과 Linear-time-Temporal Logic(LTL) 속성 𝜙가 주어졌을 때 우리는 ¬𝜙를 수용하는 Buchi 오토마타 A¬𝜙를 구축하고 이 오토마타를 fuzz campaign을 guide하기 위해 사용한다. 따라서 execution trace 𝜋를 사용하여 A¬𝜙의 수용상태에 도달하는 데 𝜋의 progress를 확인하고, A¬𝜙에서 더 많은 progress를 만들기 위해 필요한 이벤트를 도출할 수 있다. 또한 일반적으로 A¬𝜙에서 수용되는 trace는 무한 길이이며 accepting state를 무한히 자주 방문한다. fuzz campaign 중 이러한 무한 길이 trace를 생성하기 위해 application state snapshot을 취할 수 있고 A¬𝜙의 accepting state가 동일한 프로그램 상태로 방문되는지 감지할 수 있다. application state snapshot은 필요한 경우 state abstraction을 포함할 수 있으며 이 경우 반례 trace는 구체적인 실행을 통해 유효성을 검증할 수 있다.
이 논문은 임의의 LTL 속성 위반을 찾기 위해 퍼징을 이용한 기술을 제안하고 있다. 기존의 Greybox fuzzing은 충돌 또는 사용 후 메모리 해제와 같은 간단한 속성에 대해 제한되어 있다. 논문에서 제공하는 아이디어를 구현한 알고리즘과 도구는 어떤 LTL 속성도 확인할 수 있는 도구를 개발하여 충돌 또는 사용 후 메모리 해제와 같은 속성보다 훨씬 더 풍부한 속성 클래스들을 다룰 수 있게 한다. 새로운 그레이박스 퍼징 도구 "LTL-Fuzzer"를 제공한다. LTL-Fuzzer는 AFL 퍼징 도구를 기반으로 만들어졌으며, 주어진 LTL 속성의 부정을 나타내는 Buchi automaton이 특정한 exectuion trace를 accept하는지 확인하기 위한 instrumentation을 포함하고 있다.
APPROACH OVERVIEW
high level에서, 논문의 접근 방식은 sequential program P와 Linear-time Temporal Logic 속성 𝜙를 입력으로 사용한다.
𝜙의 atomic proposition 프로그램의 variables에 대한 predicates를 나타내며 참 또는 거짓으로 평가될 수 있다. 예를 들어, x>y와 같은 predicate가 있고 x와 y가 프로그램 변수인 경우를 들 수 있다.
논문의 접근 방식은 LTL 속성의 atomic proposition가 영향을 받을 수 있는 program location을 식별한다.
이를 위해 atomic proposition과 aliases가 변경될 수 있는 program location을 찾는다.
또한 conterexample을 출력하는데 있어 violation으로 이어지는 구체적인 프로그램 input을 찾아낸다.
반례 생성 과정은 크게 두 페이즈로 이루어진다.
첫 번째 단계에서 프로그램 P는 P'으로 변환되며 이를 위해 프로그램 실행 중 프로그램의 behaviors와 state transition을 모니터링 하는 code instrumentation을 사용한다. 우리는 이를 LTL 속성과 비교하여 체크한다.
두 번째 단계에서는 directed fuzzing을 통한 conterexample을 찾기 위한 fuzz campaign을 수행한다.
논문에서는 이 기술을 Pure-FTPd2라는 FTP 구현 예제를 통해 설명한다.
Pure_FTPd는 널리 사용되는 오픈소스 FTP 서버로, FTP RFC3를 준수한다. 해당 서버는 데이터를 수신하는 동안 사용자 할당량이 초과되면, 클라이언트로부터 데이터 수신을 중단하고 코드 552로 응답하며 코드 552는 할당된 저장 공간이 초과되었음을 의미한다. 이 논문에서는 LTL 속성인 𝜙로 나타낸 FTP 속성을 사용하여 속성 위반을 찾는 방법을 설명한다.
LTL Property Construction
RFC의 비공식 property를 LTL 속성 𝜙로 변환하는 과정은 다음과 같다.
keyword APPE와 552를 사용하여 Pure_FTPd 소스 코드를 검색한다.Source code 분석은 다음과 같은 결과를 나타낸다. (1) Pure-FTPd는 사용자 저장 공간을 관리하기 위한 할당량 기반 메커니즘을 구현하며, 이는 활성화된 경우에만 작동하며(2) APPE command는 dostor() 함수에서 처리되며 데이터를 수신할 때 user_quota_size가 확인된다. 할당량이 초과되면 서버는 코드 552(MSG_QUOTA_EXCEEDED)로 응답한다.따라서 우리는 속성 𝜙를 다음과 같이 구성할 수 있다.
¬𝐹 (𝑎 ∧ 𝐹 (𝑜 ∧ 𝐺¬𝑛))
당연하게도, 𝜙의 부정은 다음과 같다.
𝐹 (𝑎 ∧ 𝐹 (𝑜 ∧ 𝐺¬𝑛))
atomic a, o, n의 정의는 아래의 table을 통해 확인할 수 있다.
다음으로, 𝜙의 atomic proposition 내의 변수 값이 실행 중에 변경될 수 있는 프로그램의 위치를 식별해야 한다.
간단한 예시로, 𝑞𝑢𝑜𝑡𝑎_𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒𝑑 = 𝑡𝑟𝑢𝑒 는 Pure-FTPd에서 할당량 확인이 활성화된 프로그램 위치에 해당한다.
다른 명제에서, 𝑢𝑠𝑒𝑟_𝑑𝑖𝑟_𝑠𝑖𝑧𝑒 > 𝑢𝑠𝑒𝑟_𝑞𝑢𝑜𝑡𝑎,라고 할 때, 우리는 사용자 디렉터리에 저장하는데 사용되는 함수의 첫 번째 statement를 고려하게된다. 따라서 데이터가 사용자 디렉터리에 저장될 때마다 이러한 함수가 호출되며, statement의 평가가 진행된다.
즉, 사용자의 할당량이 초과된 경우 모두 실행에 포함된다.
명제가 𝑚𝑠𝑔_𝑞𝑢𝑜𝑡𝑎_𝑒𝑥𝑐𝑒𝑒𝑑𝑒𝑑 = 𝑡𝑟𝑢𝑒인 경우, 할당량이 초과될 때 클라이언트에 대한 응답으로 사용되는 addreply(552, MSG_QUOTA_EXCEEDED...) 함수 호출을 식별한다.각 atomic proposition의 프로그램 위치에 대한 내용은 표1에 나열되어 있다.
이들에 해당하는 code snippet은 Listings 1, 2, 3, and 4에 표시된다. 여기서 하나의 atomic proposition 당 하나의 code snippet을 표시한다.
편의를 위해, 튜플 𝑙,𝑝,𝑐𝑝 를 사용하며 여기서 𝑙은 프로그램의 위치, p는 atomic propostion, 𝑐𝑝는 atomic proposition p의 predicate를 나타낸다.
manual LTL property generation process의 끝에서 이러한 튜플을 포함하는 목록 𝐿이 출력된다.
속성 𝜙와 튜플 목록 𝐿을 유도한 후, 프로그램 P를 런타임에서 𝜙가 위반될 때 오류를 보고할 수 있는 프로그램 P'으로 변환한다.
이 프로그램 변환은 두 가지 기기화 모듈을 사용하여 수행된다.
Event Generator
프로그램 실행 중에 𝜙의 명제 값 변화를 감지하기 위해 Event Generator는 특정 프로그램 위치에 이벤트 생성 문을 삽입한다. 이를 위해 Generator는 이전 단계에서 생성된 목록 𝐿을 입력으로 사용한다. 각 튜플 𝑙,𝑝,𝑐𝑝 ∈ 𝐿에 대해 생성기는 𝑐𝑝 조건이 충족될 때 "p"와 관련된 이벤트를 생성할 수 있도록 프로그램 위치 𝑙에
if(𝑐𝑝 ) generate_event("𝑝"); 문을 삽입한다.
예를 들어, 프로그램 위치 𝑓 𝑡𝑝𝑑.𝑐, 6072는 명제 변수 𝑎 (𝑞𝑢𝑜𝑡𝑎_𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒𝑑 = 𝑡𝑟𝑢𝑒)에 해당하며, 활성화 조건은 true이다.
따라서 generator는 ftpd.c의 6072번 라인에 도달할 때마다 a와 관련된 이벤트가 생성되고 런타임에 기록된다.
다른 튜플에 대한 Instrumentation는 Listings 2,3 및 4에 나타난다.
Monitor
Monitor 모듈은 프로그램 P에 모니터를 삽입하여 프로그램 동작이 런타임에서 속성 𝜙를 준수하는지 확인한다.
구체적으로, 모니터는 실행 중에 생성된 이벤트를 수집하여 trace 𝜏을 생성한다.
그런 다음 negation of 𝜙을 Buchi automata A¬𝜙로 변환하고, A¬𝜙가 trace 𝜏를 수락하는지 확인한다.
trace가 수락되면 모니터가 실패를 보고하며, 𝜙가 P에서 유지되지 않음을 나타낸다.
Pure-FTPd 예에서 𝜙의 부정은 𝐹 (𝑎 ∧ 𝐹 (𝑜 ∧ 𝐺¬𝑛))이며 변환된 Buchi automata A¬𝜙는 아래에 나와있다.
Checking Safety Properties
Buchi automata는 trace 𝜏이 automata의 accpet state를 무한히 자주 방문할 때에만 trace를 수락한다.(위 그림의 상태 2)
safety propery의 부정(¬𝜙)의 경우, Buchi Automata A¬𝜙는 accepting 상태에 도달하는 모든 trace를 수락하므로, accepting state에 도달하는 모든 trace가 해당 위치에서 무한히 자주 반복된다.trace의 finite prefix만이 safety properties의 반례를 얻는데 관련이 있으므로, 모니터는 Buchi Automata A¬𝜙에서 accpeting state로 이끄는 trace를 확인하면 반례를 출력한다.
Checking Liveness Properties
Buchi automata of negation of 𝜙는 A¬𝜙의 accepting state를 무한히 자주 반복하는 경우에만 trace 𝜏를 accept한다. (ex. Figure1의 상태2)
예를 들어, infinite trace 𝑎, 𝑜, (𝑣) 𝜔 in which 𝑣 ≠ 𝑛 는 A¬𝜙에 의해 accept된다.
형식적으로, 이러한 trace는 𝜏 = 𝜏1 (𝜏2)^𝜔 (|𝜏2 | ≠ 0) 의 형태를 가지며, 𝜏1은 초기상태에서 시작하여 A¬𝜙의 accepting state s에 도달할 때 까지 실행된다. 𝜏2는 accepting state s에서 다시 자기 자신으로 돌아간다.
'무한히 많은 횟수'에 대한 𝜏2를 관측하는 것은 실제로 어려운데, 이는 fuzz campaign이 유한한 길이의 프로그램 실행을 방문하기 때문이다.
trace에서 루프를 감지하고, 루프가 발생할 때 실행을 종료하는 직접적인 접근 방식은 𝜏2가 m번 발생한다고 해도 𝜏2가 무한히 자주 발생함을 보장하지는 않기때문에 충분하지 않다.
이 논문에서는 atomic proposition에 관련된 이벤트가 실행 중에 발생할 때 프로그램 상태를 기록하고 관찰된 트레이스에서 상태 루프를 감지한다.
상태 루프의 실행이 𝜏2를 생성한다는 것은 상태 루프를 계속 반복하면 𝜏2가 무한히 많이 생성된다는 것을 의미한다.
결과적으로, 관찰된 trace가 무한한 𝜏1(𝜏2)^𝜔 모양의 트레이스로 확장될 수 있다고 가정한다.
다음 두 시퀀스를 실행 중에 관찰 한 경우를 고려해본다.
𝜏_𝑒는 실행 중에 발생하는 atomic proposition과 관련된 이벤트 시퀀스이며, 𝜏_𝑠는 이벤트가 발생할 때 기록되는 프로그램 상태의 시퀀스이다. 예를 들어, s_i는 이벤트 e_i가 발생할 때 기록된 프로그램 상태를 나타낸다. s_i가 s_(i+h+1)과 동일하다고 가정하면 s_i .... s_(i+h+1)은 상태 루프이며, 루프의 본문은 s_i....s_(i+h)이다.
위와 같은 입력을 수용하여 s_(i+h+1)에서 s_i로 이동하는 경우, s_i는 다시 s_i로 이동한다.
우리는 테스트 대상 시스템이 input 시퀀스를 수용하는 반응형 시스템이며, deterministic 함을 가정한다.
즉 동일한 입력은 실행 중에 항상 동일한 프로그램 동작으로 이어진다고 가정한다.
따라서 위와 같은 입력을 상태 s_i에서 반복적으로 실행함으로써 e_i e_(i+1)....e_(i+h)를 무한히 많이 생성할 수 있다.
아래와 같은 trace
는 input
를 실행함으로써 생성될 수 있다.
여기서 𝐼𝑠0 ···𝑠𝑖는 상태 s_0에서 s_i로 이어지는 입력이고, 𝐼𝑠𝑖 ···𝑠𝑖+ℎ+1는 s_(i+h+1)에서 s_i로 이어지는 입력이다.
상태 루프의 발생은 관찰된 trace를 무한한 𝜏1 (𝜏2)^𝜔 의 형태로 확장할 수 있음을 언급하였다.
이 아이디어를 활용하여, liveness property 위반을 찾을 수 있다.
실행 중에 관찰된 trace가 Buchi 오토마타 A¬𝜙가 수용하는 𝜏1 (𝜏2) ^𝜔 로 확장될 수 있는 경우, liveness property 위반이 발생하였다고 간주한다.
따라서, liveness property guided fuzzing에 대해 프로그램 P의 변환을 다음과 같이 보강한다.
(1) 실행 중 A¬𝜙의 transition label에서 이벤트가 발생할 때 현재의 프로그램 상태를 기록하는 function call을 추가한다.
record_state()라는 function call은 현재 프로그램의 상태를 가져와 실행 중에 상태에 대한 해쉬 코드를 생성한다.
(2) 프로그램의 for 및 while 루프 문의 진입점에 이벤트 생성 및 상태 기록 문을 추가하여 fuzzing 중 가능한 루프를 관찰한다. Listring 4에서 Pure-FTPd의 for 루프문에 대한 instrumentation을 확인할 수 있다.
liveness 속성을 체크하기 위한 구체적인 optimization은 Section 5에서 추가 설명을 확인할 수 있다.
Event Generator
이전 step에서 생성한 프로그램 P'은 𝜙 이 위반될 경우 failure를 보고하며, 우리는 𝜙 를 위반하는 반례를 P'을 fuzzing하여 찾아낼 수 있다.
이러한 failure 상태로 이어지게 하는 input을 우리는 counterexample이라고 생각할 수 있다.하지만, 하지만 이러한 input을 찾는 일은 매우 어려운 과제인데, 왜냐하면 특정한 이벤트가 특정한 순서로 동작하는 상황에서 execution을 생성해야 하기 때문이다.Pure-FTPd의 실행 예제에서, quota mechanism, 즉 할당량 메커니즘이 먼저 활성화 되어야 하며, 이후 user-quota 가 초과되며, 마지막으로 execution은 smg_quota_exceeded가 client에게 전송되지 않는 루프에 진입하여야한다.AFLGo와 같은 기존의 fuzzing 방식은 특정 프로그램의 위치로 fuzzing을 진행하려고 하며 특정한 순서로 여러 프로그램의 실행을 관리하지 못한다. 이를 해결하기 위한 방식이 Buchi automata guided fuzzing이다.
Buchi Automata guided fuzzing
주어진 LTL 속성 𝜙를 체크하기 위해, 오토마타의 이론적 모델은 ¬𝜙을 만족하는 모든 traces를 수용하는 Buchi automata A¬𝜙를 생성한다. A¬𝜙를 사용하여 fuzzing을 가이드 하는 과정은 다음과 같다.우선 특정한 순서로 여러 프로그램 locations를 지나는 execution를 위한 input을 생성한다.이 메커니즘은 그레이박스 fuzzer를 두 가지 방식으로 디자인 하며 보완된다.
1. Power scheduling
fuzzing 동안, power scheduling component는 미리 빌드된 control flow graph에서 가까운 seed를 선택하는 경향성을 가진다. 따라서 목표에 효율적으로 도달할 수 있으며, 이는 AFLGo의 fuzzing algorithm을 사용한다.
2. Input prefix saving
execution을 관찰하고 target에 도달할 때 소비된 input elements를 기록한다.
구체적인 접근 방식은 다음과 같다.우선 첫 번째 목표로 l1을 선택하고, l1에 도달하는 입력을 생성하는 데 중점을 둔다.동시에 execution을 관찰하고 l1에 도달하는 prefix i1을 기록한다. 두 번째 목표로 l2를 선택하고 prefix i1으로 시작하는 입력 공간을 탐색한다. 즉 l1에서 l2에 도달하는 입력을 생성한다.
sequence of program locations를 방문하는 메커니즘을 기반으로, 우리는 automata-guided fuzzing approach를 보완할 수 있다. 이 접근 방식은 프로그램 P에 Buchi automata A¬𝜙를 사용하여 실행 중에 각 trace가 A¬𝜙에서 어느 정도 진행되는지 검사한다.
accepting state로 얼마나 많은 state transition이 발생하였는지 기록하는 것이 그 예시이다.
fuzzing guide를 위하여 A¬𝜙에서 각 input이 달성한 progess를 저장하고 이를 사용하여 추가적인 progress를 만들어내는 입력을 생성한다.
이는 A¬𝜙에서 실행되는 state transition과 해당 transition으로 이어지는 prefix를 기록하는 방식으로 이루어진다.
initial state s0에서 sm으로 이동하는 trace 𝜏0와 input i0를 고려하면,
accept 된 진행 사항은 다음과 같이 표현된다.
위 튜플에서 첫 번째 요소는 s0에서 sm으로 이동하는 가장 짧은 i0의 prefix를 의미한다.
두 번째 요소는 s0...sm으로 이어지는 transition sequence를 의미한다.
이러한 process tuple은 set X에 저장되며 fuzzing guide에 사용된다.
input 생성에 있어, set X로부터 tuple을 가져오며 이것을 이용하여 추가적인 progress를 위한 input을 생성해낸다.
다음과 같은 튜플을 고려해보자.
여기서 x^s는 A¬𝜙의 state transition을 기록한다.
이 상태 전이는 input prefix인 x^i에 의해 발생한 것이다.
따라서 우리는 x^s를 사용하여 A¬𝜙에 대한 query를 진행함으로써 더 추가적인 progress를 만드는 상태 전이, 즉 A¬𝜙의 수용 상태에 가까워지는 상태 전이를 찾을 수 있다. 이 예에서는, Figure 1에서 x^s의 상태가 0이라고 가정하면 상태 0에서 상태 1로의 전이가 식별되는데, 상태 1이 수용상태 2에 더 가까워졌기 때문이다.t가 x^s의 다음의 progressvie state transition이라고 가정하면 우리는 A¬𝜙에 추가로 쿼리를 진행하여 전이 t를 발생시키는 atomic proposition을 얻을 수 있다. 이후, atomic proposition과 프로그램 위치 간의 mapping을 쿼리함으로써 해당 atomic proposition의 프로그램 위치를 식별할 수 있다.이 예시에서는 atomic proposition a가 상태0에서 상태1로의 transition을 발생시키며, 해당 atomic proposition의 위치는 table 1에 표시 된것과 마찬가지로 다음과 같다.
이러한 형태의 input을 생성하기 위해, 논문에서 제시하는 메커니즘은 program locations의 sequence를 특정한 순서로 순회한다.
A¬𝜙에서 더 추가적인 progress를 위해 l_i를 목표로 설정한다. 메커니즘은 l_i를 target으로 설정하고 prefix x^i를 prefix로 가지는 input을 계속해서 생성하는데, 이 과정을 prefix x^i로 시작하고 이후에 location l_i를 방문하는 입력을 생성할 때 까지 반복한다.
이러한 과정이 X의 tuple을 이용하여 추가적인 progress를 만드는 input을 생성하는 과정이다.
Fuzzing Algorithm
위 알고리즘은 counterexample guided fuziing의 예시를 보여준다. counterexample을 찾기 위해, algorithm은 fuzzing을 두 가지 측면에서 guide한다.
우선 해당 알고리즘은 A¬𝜙에 의해 accpet될 가능성이 높은 input을 우선한다.
구체적으로, A¬𝜙의 accpeting state와 가까운 state에 reach할 수 있는 trace of prefix of input을 우선적으로 accept한다.
line 5, line 10을 보면 알고리즘이 accpeting state에 더 가까워지는 것을 관찰한 prefix of input을 선택하고 해당 입력으로 시작되는 input을 계속해서 생성한다.
그 후 알고리즘은 A¬𝜙에서 더 추가적인 진행을 이루는 execution을 생성하는 데 중점을 둔다.
prefix of input이 주어지면 알고리즘은 A¬𝜙에서 accepting state에 더 가까워지도록 도와주는 state transiton t를 찾으며, 이를 활성화 하는 atomic propostion을 찾는데, 이는 line 6에 기술되어 있다.
이후 전이 t를 활성화하는 atomic propostion에 대해 해당하는 프로그램 위치를 식별하는데, 이는 line 7에서 기술되어 있다.
이후 program location에 도달하기 위한 inputs를 생성하고 atomic proposition과 관련된 program behavior를 발생시키기 위한 시도를 수행한다.
결과적으로 생성된 trace는 A¬𝜙에서 further progress를 발생시키게된다.
특정한 program location에 도달하기 위한 input을 생성하려면, 우리는 AFLGo에서 제시된 알고리즘을 활용하면 된다(라인 8-14에 해당한다)
이 아이디어는 미리 생성된 control flow graph에서 target에 더 가까운 seed를 파악하고, 그곳에 더 많은 power를 할당하여 생성된 입력이 목표에 도달할 확률을 높힌다.
target에 도달하는데 사용할 수 있는 time budget은 매개변수 𝑡𝑎𝑟𝑔𝑒𝑡_𝑡𝑖𝑚𝑒을 통해 구성할 수 있다.
line 5에 적혀있는 prefix selection을 수행하기 위해 알고리즘은 각 prefix tuple에 대한 fitness function을 정의하여 fitness value를 계산한다. 주어진 튜플에 대한 fitness value는 다음과 같다.
여기서 \(l_{s}\) 는 \(x^{s}_{t}\) 의 길이이며, \(l_{a}\) 는 \(x^{s}_{t}\)의 마지막 state에서 A¬𝜙의 accpeting state 까지의 가장 짧은 path의 길이를 의미한다.
공식에서 확인할 수 있듯이, prefix tuple은 \(x^{s}_{t}\) 의 last state가 A¬𝜙의 accpeting state와 가까울 수록ㅡ input prefix가 짧을수록 더 큰 fitness value를 갖는다.
이러한 prefix를 확장함으로써 fuzzing algorithm은 A¬𝜙에서 accept 할 수 있는 execution trace를 생성할 확률이 증가한다.
더 큰 fitness value를 가지는 prefix tuple은 선택에 있어 더 우선시된다.
atomic proposition selection (line6)에서, 우리는 random selection 전략을 사용한다.
tuple < \(x^{i}_{t}\), \(x^{s}_{t}\) > 을 고려하고 last state of \(x^{s}_{t}\)가 \(s_{t}\)라고 하면, 알고리즘은 \(s_{t}\)에서 A¬𝜙로 추가적인 transition을 진행할 수 있는 atomic propostion을 다음과 같이 식별한다.
\(s_{t}\) state가 accpet state가 아닌 경우, \(s_{t}\)에서 accept state로의 transition을 트리거 하는 atomic proposition 중 하나가 선택된다.
\(s_{t}\) state가 accept state인 경우, \(s_{t}\)에서 \(s_{t}\)로 이동하는 transition을 트리거하는 atomic propostion중 하나가 선택된다.
간단하게 말하면 식별된 atomic proposition 중 하나를 랜덤하게 뽑는 알고리즘을 사용하는 것이다.
선택된 proposition이 여러개의 연관된 program locations를 가질경우, 랜덤하게 하나를 선택하게 된다.
이러한 전략에서 가장 중요한 것은 테크닉을 가장 심플한 상태로 유지하는 것이다.
State Saving
Liveness property 검증에서, LTL-Fuzzer는 witnessed trace에서 상태 루프를 감지한다.
만약 상태 루프가 감지되면, LTL-Fuzzer는 현재 trace가 lasso-shaped trace, 즉 \(𝜏1(𝜏2)^{ω}\)형태로 확장될 수 있다고 가정한다.
하지만 소프트웨어의 실행은 항상 추상적이기때문에, 이러한 루프와 관련된 변수 상태에 대한 정보를 놓치게 될 수도 있으며 이는 잘못된 positives로 결과를 유도할 수 있다.
반면 루프와 관계 없는 변수들의 정보까지 캡처하는 너무 구체적인 state representation은 잘못된 negative로 결과를 유도할 수 있다.
실용성을 보장하기 위하여, LTL-Fuzzer는 application의 register와 addressable memory, 그리고 이를 32-bit의 정수로 해쉬하며 이는 state로 저장된다.
Addressable memory는 두 종류의 Object에 해당하는데 각각` global variable`과 `malloc()과 alloca()에 의해 explicit하게 할당된 객체`를 의미한다.
LTL-Fuzzer는 선택된 program location에 대해서만 프로그램 상태를 기록한다.구체적으로 말하면, 𝜙가 체크될 liveness property일때, automata A¬𝜙의 transition label과 연관된 프로그램 location만을 기록한다.
A¬𝜙의 transtion label은 atomic propostion의 subset에 해당한다.
Atomic proposition의 full set은 𝜙에서 등장하는 atomic propostion을 이용해 construct 해야하며 이 set을 각각의 프로그램의 loop header의 occurrence를 위해 도입했던 atomic propostion을 이용하여 embellish 해야한다.(Table 1의 l)
만약 transition label이 atomic propostion의 set L을 포함한다면 우리는 loop header의 발생과 관련된 atomic propostion L을 위한 state를 track하게된다.
여기서 목표는 루프 헤더를 관찰하면서 무한 루프를 빠르게 발견하는 것이다.따라서 transition label !n에 대해서는, Table 1의 atomic propostion l에 대한 프로그램 locations만을 저장해야 한다.
Section2의 예시에서, LTL-Fuzzer는 program location <ftpd.c, 4067> 에서 발생한 state를 관측했다.(Listing 4)이 state 이전에 관측된 state이며, 관측된 trace는A¬𝜙에 의해 accept 되었다.trace가 LTL property의 부정을 accpet하는 오토마타에 의해 accpet 되었으므로, 자연스럽게 LTL-Fuzzer는 LTL property의 위반을 보고 하게된다. 이러한 위반이 진짜인지 아닌지 검증하기 위해서 우리는 state loop가 실제 실행에서 반복되는지 확인할 필요가 있다.논문에서는 이를 검증하기 위해 chunk of data 가 상태 루프의 실행 도중 읽어진 것과, client에 의해 업로드된 파일의 chunk of data를 보여준다.업로드된 데이터 조각을 복사하고 experiment를 재 수행한 후, 상태 루프가 다시 반복되는 것을 확인한다.이는 witnessed trace가 \(𝜏1(𝜏2)^{ω}\)로 확장될 수 있음을 의미하며, 위반이 true임을 알 수 있다.
추가적으로 위반의 root 원인을 분석한다.이는 quota checking model에 논리적인 결함이 있음을 보여준다.Listing 5에서 볼 수 있듯, max_filesize의 assignment는 조건문에서 발생할 수 있고, max_filesize의 initial value가 -1이기 때문에 절대 수행될 수 없다.이러한 버그를 수정하려면, 검증된 Pure-FTPd를 사용하기 위해 pull request를 수행해야한다
이 부분은 조금 뜬금없는 느낌이였다...
LTL-Fuzzer Implementation
논문에서는 LTL-Fuzzer를 AFL 위에 구축된 open source tool로 구현하며, 이는 instrumentor과 fuzzer로 이루어져 있다.
Instrumentation Module
AFL은 clang을 위한 특별한 compiler pass로 이루어지는데, 이는 모든 분기 명령을 계측한다(instrument).
이 컴파일러를 확장하면, 우리는 프로그램을 3개의 level로 instrument할 수 있으며 3개의 level은 다음과 같다.
: specific locations, basic blocks, applicaion
Specific Locations
LTL-Fuzzer는 test가 발생할 수 있는 property와 연관된 프로그램 location의 list를 가져온다.
각 주어진 프로그램 location에서, instrumentation module은 두 개의 components를 주입하며, 각 component는 event generator와 state recorder이다.
Event generator의 경우 주어진 condition이 런타임에 만족될 경우 이벤트를 발생 시키는 코드 조각을 의미한다.
State recorder의 경우 프로그램 상태의 스냅샷을 지닌 컴포넌트와 주어진 프로그램 location이 실행 중 도달되었을 때의 state에 대한 해쉬 코드의 생성을 수행하는 component에 해당한다.
Basic Blocks
LTL-Fuzzer는 Section 3에서 설명한 것처럼, input이 얼마나 target에 가까웠는지에 대한 feedback을 바탕으로 fuzzing을 guide 한다. 런타임동안, LTL-Fuzzer는 CFG(control flow graph)에서 각 basic bloack에서 target 까지의 거리를 요청한다.
The instrumentor는 런타임동안 각 basic block에서의 함수 호출을 관측한다.
function call은 주어진 property와 연관된 program locations와 각 block간의 distance를 저장하는 테이블에 대해 쿼리를 진행한다.
이러한 distance 계산은 AFLGo를 활용한 distance calculator component에 의해 수행된다.
Applications
instrumentation model은 monitor를 프로그램에 인젝션한다.
fuzzing 동안, monitor는 instrumented event generator에 의해 발생한 이벤트를 수집하고 execution trace를 생성한다.
property check를 위해, monitor는 Spot Libraries를 활용하여 negation of LTL property로부터 Buchi Automata를 생성하고 traces들을 검증한다.
instrumentation module은 또한 input의 실행을 관측하는 program 내부의 observer를 instrument한다.
이는 주어진 suitable execution trace prefix를 이를 생성하는 input event sequence와 매핑하며, 따라서 fuzzing동안 prefix의 occurrence는 observer에 의해 감지될 수 있다.
fuzzing process는 이후 설명될 `suitable event`와 추가적으로 prefix를 확장한다.
Fuzzer
위 그림은 Fuzzer component의 architecture를 보여준다.
크게 prefix controller와 fuzz engine, 두 개의 모듈로 나누어져 있는 것을 확인할 수 있다.
LTL-Fuzzer는 automata에서 transition을 발생시킨 execution trace의 input prefix를 저장하고 추가적인 exploration을 위해 재사용한다.(섹션 3에서 설명되었음)
런타임에서, prefix controller는 3개의 태스크를 수행한다.
1. monitor가 프로그램이 테스트 중인 상황에서 instrument 함으로써 보고된 prefix를 수집하고 pool에 저장한다.
2. 추가적인 exploration을 위해 Algorithm 1에 따라 pool에서 prefix를 선택한다.
3. 선택된 prefix를 기반으로 target program location을 식별한다.
Fuzz engine은 변형된 AFL을 사용해서 구현되며, 주어진 input prefix로 시작하는 input을 생성한다.
타겟에 도달하기 위하여, fuzzer는 AFLGo에서 개발된 power scheduling component를 direct fuzzing와 통합시킨다.
LTL-Fuzzer에서 input prefix의 실행 이후 target에 도달하기 위해 execution을 direct한다.
따라서, fuzz engine은 input prefix의 실행 도중은 coverage 데이터 등의 피드백을 수집하지 않으며 실행이 종료된 이후의 피드백만을 수집한다.
Evaluation
논문의 실험에서는, 다음 질문에 대한 답을 얻고자 하는 시도를 수행한다.
1. Effectiveness: LTL-Fuzzer는 LTL 속성 위반을 얼마나 효율적으로 찾아낼 수 있는가?
2. Comparison: LTL-Fuzzer는 다른 state-of-the-art validation tool과 비교하여 어떤 차이가 있는가?
3. Usefulness: LTL-Fuzzer는 공개된 LTL 속성 위반을 실제 시스템에서 찾는데 얼마나 실용적인가?
위 Table 2는 측정을 위해 사용한 프로그램들이 나열되어 있다. 6개의 널리 사용되는 네트워크 프로토콜을 구현한 7개의 오픈소스 소프트웨어 프로젝트에 해당한다.
Experiment Setup
LTL-Fuzzer을 set of LTL properties를 위반값이 이미 알려져 있는 subject program에서 실행시키며 효율성을 체크한다.
얼마나 많은 숫자의 LTL 속성 위반을 체크하는지 그 수를 확인한다.
이후 다른 tool들과 비교한다.
state-of-the-art 테크닉과 관련하여, model checking, runtime verification과 directed fuziing domains등의 최근에 잘 알려진 테크닉을 고려한다.
다음과 같은 techniques를 LTL Fuzzer와의 비교를 위해 사용한다.
1. AFLGo
2. \(AFL_{LTL}\)
3. L+NuSMV
'개인학습' 카테고리의 다른 글
OAuth (0) | 2023.10.23 |
---|---|
MVC 패턴 (1) | 2023.09.14 |
(TIL) Model Checking (0) | 2023.08.22 |