[논문 리뷰] All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution / Part 2. Forward Symbolic Execution

저번에 이어서 오늘은 All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution 의 두번째 파트인 Forward Symbolic Execution에 대한 정리이다. 줄여서 FSE로 쓰도록 하겠다.

 

FSE는 프로그램의 실행 흐름에 대해 논리식을 만들어가면서, 여러 종류의 입력에 대한 프로그램의 행동들을 추론할 수 있게 해준다. 

 

가장 naive 한 형태의 fuzzing이 아래 예시에서 어떻게 동작할 지 생각해보자.

출처: https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf

 

x가 32 bit integer 라고 가정한다면, if 분기문의 조건인 x-5 == 14를 만족할 확률은 2의 32승분의 1로 매우 작다.

 

이를 매번 랜덤한 입력을 바꾸어 가면서, 해당 분기를 true로 만족시켜 crash를 발생시킬 확률은 정말 낮다.

 

하지만 FSE는 이를 크게 두 개의 input classes로 구분하여 나타낸다. true branch로 가는 입력과 false branch로 가는 입력으로 말이다.

 

FSE의 가장 큰 특징은 사용자 입력 함수의 반환 값을 concrete 한 값이 아니라, 하나의 symbol로 처리한다는 것이다.

이러한 symbol은 어떠한 값도 가질 수 있는 일종의 변수(프로그램에서 선언된 변수랑은 다른 개념)로 생각하면 된다.

 

이러한 symbolic variables의 값은 처음에는 임의의 값이었다가, if 문을 만나면서 점점 값이 constrained 된다. (좁혀진다.)

 

아래 예시를 보자.

 

 

여기서, path predicate Π 기호에 집중하자.

 

처음에 사용자 입력으로 받은 값의 symbolic variable을 s라고 하면, 처음 if 분기를 만났을 때, 해당 조건문이 true 일 때의 path predicate과 false 일 때의 path predicate을 위와 같이 두 개의 classes로 구분하여 나타낼 수 있다. 

 

결국에는 프로그램이 실햄됨에 따라 더 많은 조건문을 만나면서, symbolic variable s가 가질 수 있는 값은 좁혀질 것이다. 

 

이러한 s가 가질 수 있는 값에 조건을 path predicate이 담고 있다.

 

Forward Symbolic Execution Challenges and Opportunities

 

FSE의 Challenges로 세 가지를 예로 들고 있다.

 

1) Symbolic Memory 

 

Symbolic Jump도 논문에서는 따로 소개하는데, 둘이 비슷해서 Symbolic Memory만 정리하도록 하겠다.

 

메모리 참조를 할 때, 참조하는 주소가 concrete 한 값이 아닌 symbolic variable일 때 어떻게 할 것인지에 대한 문제이다. 

실제로 이러한 문제는 빈번히 일어나는데, 예를 들어, 사용자 입력이 table lookups 할 때 index로 활용되는 경우이다.

 

이러한 symbolic memory address problem은 aliasing issue로 이어질 수 있는데, alias는 두 개의 memory operation이 서로 같은 주소를 참조할 때 일어날 수 있다. 

addr1이 addr2와 같은 주소를 가리키고 있다면, 이 둘은 aliased 되었다고 한다. 문제가 뭐냐면, 가장 안 좋은 예시로, 이 둘 간의 관계가 어떨 때는 aliased, 어떨 때는 아닐 수도 있어서, 굉장히 프로그램의 행동을 분석하기 어려워질 수 있다는 것이다.

 

해결 방안으로 세 가지 정도를 제시하고 있다.

 

1-a) Make unsound assumptions for removing symbolic addresses from programs.

한 가지 예로, 선택적으로 모든 메모리 주소에다가 이름을 붙이는 것이다. 

1-b) SMT Solver 한테 맡기기

SMT Solver에 생성된 식을 넘겨 해당 식을 만족하는 값들을 찾아내는 것이다.

SMT Solver으로부터 정확한 결과값을 얻기 위해서는 메모리 업데이트마다 이름을 부여해야 한다.

 

 

처음 프로그램의 메모리 이름을 mem0라고 하면, store(addr1, v)를 하게 되면 해당 메모리의 이름을 mem1으로 하는 것이다.

 

1-c) Alias Analysis

직접 해당 참조가 같은 주소를 가리키고 있는지 정적 혹은 오프라인 분석으로 해석하는 것이다. 

 

2) System Calls

 

read와 같이 사용자 혹은 파일로부터 입력을 받는 system call 같은 경우에는 단순히 symbolic variables를 return 한다는 것 외에도 side effects까지 고려해야 한다. (파일 내에서 읽고 있는 pointer의 위치가 매 read()마다 달라진다.)

 

결국 이러한 system call 함수들에 대한 side-effects를 따로 정리하거나 (make summaries) concrete execution에서 return 된 값을 그대로 사용하거나 하는 것이 있다.(may not be sound)

 

3) Path Selection

퍼포먼스와 직결되는 중요한 Challenge이다. 

처음 든 예시에서 T-Cond와 F-Cond 중에 어디를 선택하느냐에 따라서 후에 crash를 더 찾아낼 것인지 말 것인지 큰 영향을 받게 된다.

 

그 이유 중 하나는 infinite loop에 빠지게 되면, 다른 branch를 볼 수도 없게 될 것이기 때문에 어떤 path로 갈 지 선택하는 것은 상당히 중요한 문제이다. (loops-handling)

 

그래서 보통 FSE는 stuck 되는 것을 방지하기 위해서 loops에 대해서 상한선을 정해놓는다. 

 

이러한 Path Selection Problem에 대한 네가지 접근들을 소개한다.

 

3-a) DFS 

보통 DFS의 cyclic path에 대해서 Max Depth를 지정하여 infinite loop에 빠지는 것을 방지한다.

 

3-b) Concolic Testing

후에 포스팅에서 다룰 concolic testing이다. concrete + symbolic 이라고 생각하면 되는데, symbolic execution이 concrete execution 보다 너무 느리기 때문에 이 둘은 적절히 결합하여 성능을 개선하는 것이다. concrete execution으로 프로그램 실행의 trace를 모으고, fse가 이와 동일한 경로를 따라가면서 새로운 input을 만들어낼 수 있다. (해당 조건을 단순히 negate 하는 식으로)

 

3-c) Random Paths

shallow state에 가중치를 부여하여 random path selection을 진행하도록 하여 infinite loop에 빠지는 것을 방지한다.

 

3-d) Heuristics 

e.g. distance from the current point of execution to uncovered states 

 

 

---

 

이로써, All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution 논문에 대한 정리가 끝이 났다. 

 

논문 리뷰 포스팅을 시작하게 된 이유는

 

교수님께서 논문 정리를 공부 초반에 해두면, 나중에 해당 내용을 참조할 때 굳이 논문을 다시 읽을 필요가 없어서 도움이 된다고 하셨다.

 

이왕이면 정리한 내용만 봤을 때, 바로 논문의 내용을 떠올릴 수 있을 정도로 정리를 해두라고 하셔서 블로그에 정리를 한다.

 

뭔가 개인 노트 앱에 정리를 하다보면, 정말 나만 알아볼 수 있는 언어로 정리해서 나중에 다시 봤을 때 이해하기 힘든 경우가 많다.

 

그리고 이 분야가 아직 한글로 된 자료가 많지 않아서, 정리해두면 나중에 한글로 된 좋은 참고 자료로 활용될 수 있을 것 같아서 public 하게 남겨둔다.

 

Reference:

https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf

 

※ Any feedbacks and corrections are welcome. Feel free to comment down below.