An Overview of Symbolic Execution
symbex라고도 불리는 기호 실행(symbolic execution)은 프로그램 상태와 관련한 메타데이터 정보를 추적해 프로그램 상태(program state)가 어떻게 변화되며 다른 프로그램 상태에 어떻게 도달할 수 있는지 추론할 수 있다. 기호 실행은 프로그램의 상태를 논리적인 수식으로 표현해 프로그램 동작에 대해 결과를 추론한다.
기호 실행은 효과적인 기법이지만 규모 가변성(scalability) 문제가 있기 때문에 사용 시 주의해야 한다.
Symbolic vs. Concrete Execution
기호 실행(symbex)은 대상 프로그램을 실행하거나 에뮬레이션 할 때 구체적인 값(concrete value) 대신 기호로 표현된 값(symbolic value)를 사용한다.
(앞으로도 언급하는 변수란 바이너리 분석의 관점에서는 레지스터나 메모리 위치까지도 포함한다.)
기호 실행은 구체적인 값을 변수에 할당하지 않고, 일부 혹은 전체 변수를 해당 변수가 취할 수 있는 가능성을 포괄한 수식 형태로 표현한다. 이 수식은 대상 기호에 적용되는 연산이나 변수값의 제한 범위가 포함되는데, 기호 실행은 프로그램의 실행에 맞게 명시적 기호들의 논리적 수식을 계산하는 방식으로 동작한다.
대부분의 기호 실행은 오염 분석이 오염 정보를 메타데이터로 관리하듯이 구체적인 값을 포함한 기호와 수식을 메타데이터 형태로 관리한다.
이때 기호로 표현된 값과 그에 관한 수식을 기호적 상태(symbolic state)라고 한다.
The Symbolic State
symbex 엔진은 기호 값에 대해 기호 표현식(symbolic expression)의 집합과 경로 제약 조건(path constraint) 두 가지 수식을 계산한다. 그리고 각 변수를 기호 표현식과 연계해 관리한다.
경로 제약 조건과 기호 표현식 그리고 이들의 상관관계를 기호적 상태(symbolic state)라고 한다.
값이 자연수일 때(), 라는 기호 값이 있다고 하자.
- 기호 표현식(symbolic expression)
자연수 에 대해(), 기호 표현식 는 기호 값 또는 몇 개의 기호 표현식에 대한 수학적 조합을 말한다(예: ).
모든 기호 표현식의 집합을 기호 표현식 목록(symbolic expression store)이라고 하며 로 표기하겠다(변수들 역시 로 표현할 수 있다).
- 경로 제약 조건(path constraint)
경로 제약 조건은 조건 분기(branch)로 인해 기호 표현식에 적용되는 제한 사항을 뜻하며, 로 표기하겠다.
예를 들어 if(x < 5)와 if(y >= 4) 조건이 발생했고, 변수 x, y를 각각 기호 표현식에서 과 로 표현한다고 하자. 그러면 경로 제약 조건을 계산하는 공식은 다.
경로 제약 조건을 branch constraint라고도 표현하는데, 여기서는 구분을 위해 개별적인 조건 분기를 말할 때만 branch constraint라고 하겠다.
Symbolically Executing an Example Program
다음 예제의 pseudocode를 살펴보자.
- Pseudocode example to illustrate symbolic execution
x = int(argv[0]) // ➊
y = int(argv[1])
z = x + y // ➋
if(x >= 5) // ➌
foo(x, y, z)
y=y+z
if(y < x)
baz(x, y, z)
else
qux(x, y, z)
else // ➍
bar(x, y, z)사용자가 어떤 값을 입력했을 때 코드 흐름이 foo 함수 및 bar 함수에 도달하는지 찾고자 한다.
다음은 주어진 예제 코드에 대해 가능한 경로에 도달하기 위해 어떻게 기호적 상태를 변화시켜 가는지 나타낸 그림이다.
- Path constraints and symbolic state for all paths in the example function
그림에서 경로 제약 조건 가 동어의 반복인 으로 초기화되어 있다. 이는 조건 분기와 제약 조건이 없기 때문이다. 기호 표현식 목록 도 공집합으로 초기화되어 있다.
그리고 사용자로부터 x와 y 값을 입력받는다➊. 그러면 symbex 엔진이 값과 값에 대해 각각 과 라는 기호 표현식을 생성한다. 이는 구체적인 값으로 표현될 수 있는 제한 없는 기호 값(unconstrained symbolic value)으로 나타낸 것이며 각각 x, y에 연계된다.
이후 z = x + y 연산이 수행되면➋, symbex 엔진은 값을 로 표기한다.
symbex 엔진이 if(x >= 5)가 참인 경우를 먼저 진행한다고 해보자➌. 이를 위해 에 을 추가해야 하고, 그 결과 foo 함수를 호출하게 된다. 이제 foo 함수를 호출하는 조건을 찾았으므로 기호 표현식과 branch constraint를 만족하는 구체적인 와 값을 찾아야 한다.
현재 와 값은 각각 기호 표현식으로 및 로 연계되어 있고, branch constraint는 하나만 존재한다. 이때 가능한 foo 함수를 호출할 수 있는 해답(solution) 중 하나로 가 있다. 이때 경로 제약 조건상 값과 관련된 기호 표현식이 없었으므로 는 어떤 값이든 상관 없다.
이렇게 찾아낸 solution을 모델(model)이라고 한다. 제약 조건 풀이기(constraint solver)를 사용하면 제약 조건 및 기호 표현식을 만족하는 기호 값을 찾아 모델을 계산할 수 있다.
이번에는 bar 함수에 도달하는 방법을 찾기 위해 if(x >= 5) 분기에서 else 방향으로 진행해 보자➍. 이를 위해 경로 제약 조건을 에서 로 변경한 뒤에 constraint solver에게 새로운 모델을 요구해야 한다. 가능한 해답 중 하나로 이 있다.
어떤 경우에는 constraint solver가 해답을 제시하지 못할 수도 있는데, 이는 해당 경로로 진행이 불가능하다는 뜻이다.
Variants and Limitations of Symbolic Execution
다음 그림은 기호 실행 구현에서 중요한 설계 원리들을 요소별로 구분한 것이다.
트리(tree) 구조에서 한 층(level)은 각 요소의 차원(dimension)을 의미한다.
각각의 설계 원리와 장단점을 성능, 한계, 완전성 측면에서 살펴보자.
Static Symbolic Execution (SSE)
정적 기호 실행(SSE, Static Symbolic Execution)은 프로그램의 부분(part)을 에뮬레이팅해 명령어가 수행될 때의 기호 값들의 상태 변화와 전파(propagation)를 살펴보는 기법이다.
탐색할 경로를 선택할 때에는 모든 경로를 전부 탐색하거나 휴리스틱 알고리즘을 기반으로 임의의 경로를 탐색하는 방법이 있다.
- SSE의 장점
SSE는 CPU 상에서 구동할 수 없는 프로그램도 분석할 수 있다. 또한 특정 함수와 같이 바이너리의 일부분을 분석할 때 상대적으로 쉽다는 이점이 있다.
- SSE의 단점
SSE의 단점은 규모 가변성 문제를 해결하기 힘들다는 것이다. 발생 가능한 분기에 대한 모든 경로를 탐색하는 것이 항상 가능하지는 않다. 또한 휴리스틱 방식으로 분기를 제한하더라도 흥미로운 모든 경로를 탐색하는 것은 어렵다.
게다가 SSE만으로 정확한 모델을 찾는 것이 불가능할 때도 있다. 특히 대상 프로그램의 외부 컴포넌트인 라이브러리나 커널 등에서 제어 흐름이 발생하는 경우 그러하다(시스템 콜, 라이브러리 함수 호출, 시그널 수신, 환경 변수 사용 등).
다음은 이런 문제를 해결하기 위한 방법들이다. 다만 이 역시 단점을 감수해야 한다.
- 효과 모델링(effect modeling)
시스템 콜이나 라이브러리 함수 호출 등과 같은 외부 요인을 효과적으로 모델링 할 수 있는 방법으로 외부 요인이 해당 기호 상태에 어떤 영향을 미쳤는지 정보를 종합해(summary) 나열한다. (여기서의 모델은 constraint solver가 반환하는 soulution을 뜻하는 모델과는 관련이 없다.)
성능 측면에서 효과 모델링은 상대적으로 저렴한 방법론이다. 하지만 네트워크 통신, 파일 시스템 호출, 다중 프로세서 등 발생 가능한 모든 환경적 요인들을 고려하는 모델을 만드는 것은 어렵다. 게다가 다른 종류의 운영체제나 커널에서 시뮬레이션하는 경우 모델을 수정해야 한다.
따라서 이런 방식은 불완전하거나 부정확하다.
- 외부 요소에 대한 직접 처리(direct external interactions)
symbex 엔진이 외부 요소의 변화를 직접 관리하는 방법이다. 예를 들어 시스템 콜을 직접 처리하고 그에 따른 결과를 기호적 상태에 반영하는 방식이다.
이는 단순하지만 외부 요소들이 동시에 발생하는 경우 처리가 어렵다는 단점이 있다. 예를 들어 한 파일에 병렬적으로 작업을 처리하는 여러 경로가 있을 경우 적절한 처리를 해주지 않으면 동시성(consistency) 문제가 발생할 수 있다.
이를 해결하기 위해 전체 시스템 상태를 복제한 뒤에 각 경로를 탐색하는 방법도 있지만 이는 메모리 관점에서 비효율적이다.
또한 외부 컴포넌트에 전달하기 위한 concrete value를 찾기 위해 constraint solver를 호출하는 비용도 고려해야 한다.
이런 치명적인 단점들 때문에 최근 연구에서는 동적 기호 실행이 중점적이다.
Dynamic Symbolic Execution (Concolic Execution)
동적 기호 실행(DSE, Dynamic Symbolic Execution)은 구체적인 값을 포함해 기호적 상태를 유지한 채로 특정 값을 대입하는 방법이다. 즉 concrete state를 사용해 symbolic state를 메타데이터로 유지한 채로 실행하는데, 이는 오염 분석 기법에서 오염 정보를 관리하는 것과 유사한다.
이 때문에 DSE는 구체적 값(concrete)과 기호 값(symbolic)을 합성한 concolic execution(concrete symbolic execition)이라고 불린다.
DSE는 concrete value에 따라 한 번에 한 개의 경로만 탐색할 수 있다. 다른 경로를 탐색하기 위해서 위 예제와 같이 경로 제약 조건을 뒤집고(flip), 이를 constraint solver에 대입하여 다른 분기로 향할 수 있는 concrete value를 계산할 수 있다.
- DSE의 장점
병렬 실행을 위해 여러 개의 상태를 유지할 필요가 없으므로 규모 가변성이 뛰어나고 동시성(consistency) 문제도 고려할 필요가 없다. 또한 외부 컴포넌트와의 상호작용은 구체적인 값을 특정할 수 있으므로 문제가 되지 않는다.
목적에 따라 원하는 값만 기호화해 처리하므로 계산해야 할 제약 조건이 상대적으로 적다. 덕분에 constraint solver를 사용할 때 부담이 적다.
- DSE의 단점
초기에 특정된 입력값에 의해 한정되는 코드 커버리지(code coverage) 문제가 주된 단점이다. 초기에 주어진 경로에 분기가 많다면 유의미한 경로에 도달하는 데 오래 걸릴 수 있다. 실행 시점에서 DSE 엔진을 활성화/비활성화할 수 있도록 구현하더라도 프로그램의 일부만을 기호 실행으로 분석하는 것은 쉽지 않다.
Online vs. Offline Symbolic Execution
이는 symbex 엔진이 여러 경로를 병렬로 탐색하도록 구현할지에 대한 고려 사항이다. 여러 경로를 탐색할 수 있는 경우 온라인(online) 방식, 한 번에 한 개의 경로만 탐색할 수 있는 경우 오프라인(offline) 방식이라고 한다.
예를 들어 전통적인 SSE 방식은 분기를 만날 때마다 인스턴스를 복제해 병렬적으로 탐색하는 온라인 방식을 사용했고, DSE는 보통 구체적인 값을 특정해 한 번에 한 개의 경로만을 탐색한다. 물론 오프라인 방식의 SSE나 온라인 방식의 DSE도 존재한다.
온라인 방식의 장점은 같은 명령어를 여러 번 다시 수행할 필요가 없다는 것이다. 오프라인 방식은 프로그램을 재시작하는 경우 동일한 명령어일지라도 다시 수행해야만 한다.
반면 병렬 처리를 위해 모든 기호 상태 정보를 관리하는 것은 메모리 관점에서 비효율적이다.
온라인 방식은 메모리 문제를 해결하기 위해 기록 시 복제(copy on write)라는 최적화 방식을 사용한다. 이는 프로그램 상태에서 동일한 부분은 병합하고 분기가 발생할 때에만 분할하는 방법이다. 특히 쓰기 작업이 발생할 때 병합된 상태의 복사본을 생성하는 방식으로 동작한다.
Symbolic State
다음은 프로그램 상태 중 어떤 부분을 기호로 표현할 것이며 어떤 부분을 구체적인 값으로 특정할지에 대한 고려 사항이다. 또한 기호 값에 대한 메모리 접근을 처리하는 방식도 관건이다.
대부분의 SSE 및 DSE 엔진은 기호적 상태를 임의로 생략한다. 여러 상태 정보 중 일부만 기호로 사용하고 나머지는 구체적인 값으로 사용하는 것이 경로 제약 조건 및 기호 표현식에 대한 복잡도와 메모리를 크게 감소시킬 수 있기 때문이다. 이런 방식은 제약 조건식 풀이가 쉬워지기 때문에 속도 측면에서도 이점이 있다. 하지만 어떤 값을 기호 값 또는 구체적인 값으로 사용할지 판단하는 것이 항상 자명한 것은 아니라는 점이 문제다.
또 다른 중요한 관점 하나는 기호적인 메모리 접근(symbolic memory accesses)을 표현하는 방식이다. 포인터 변수 역시 기호로 표현될 수 있는데, 그 값은 concrete가 아니라 부분적으로 결정되지 않았음을 의미한다. 이런 경우 메모리에서 load 하거나 store 할 때 기호로 된 메모리 주소를 사용하게 되는 문제가 발생할 수도 있다.
다음은 이런 문제를 해결하기 위한 방법들이다. 대부분의 symbex 엔진은 이 기법들을 혼합해 적용한다.
- 전역 기호 메모리(fully symbolic memory)
전역 기호 메모리 방식은 가능한 모든 메모리 LD/ST 동작에 대해 모델을 찾고자 한다. 이를 위해 하나의 상태를 복사해 가능한 모든 결과에 대응시킬 수 있다.
예를 들어, a라는 배열에서 값을 읽을 때 기호로 표현된 라는 인덱스에 접근한다고 해보자. 이때 라는 제약 조건이 존재한다면 상태 값은 인(a[0]를 읽으려는 경우) 경우, 인 경우 등등 다섯 가지 경우의 수로 나뉠 수 있다.
또는 몇몇 constraint solver가 제공하는 if-then-else 표현식을 사용하는 방법이 있다. 그러면 동일한 배열에서 발생하는 메모리 접근은 인 경우 a[i]의 기호 표현식으로 치환되는 조건부 제약 조건(conditional constraint)으로 모델링 된다.
전역 기호 메모리 방식은 메모리 공간에 대한 제한이 없는 경우 상태의 가짓수가 폭발적으로 많아지거나(state explosion) 제약 조건이 복잡해지는 문제가 있다. 게다가 이런 문제는 구체적인 메모리 경계 정보를 알기 힘든 바이너리 수준에서 더욱 심각해진다.
- 주소 구체화(address concretization)
fully symbolic memory의 state explosion 문제를 회피하기 위해 특정되지 않은(unbounded) 기호 주소를 concrete라고 간주할 수 있다.
DSE 엔진은 구체적인 메모리 주소 값을 사용할 수 있다. 반면 SSE 엔진은 주소 값을 위해 휴리스틱 방법을 사용해야 한다.
하지만 프로그램의 모든 경우의 수를 전부 다룰 수는 없고, 이 때문에 일부 결과를 놓칠 수 있다는 단점이 있다.
Path Coverage
마지막은 프로그램의 경로 중 어떤 경로를 탐색할지 결정하는 문제다.
고전적인 방식의 기호 실행은 모든 경로를 탐색하도록 했는데, 그로 인해 그 경로에 대한 경우의 수가 폭발적으로 증가하는 경로 폭발(path explosion) 문제가 발생했다. 무한 루프나 재귀 호출이 존재한다면 가능한 경로의 수가 무한대가 되므로 적절한 처리 방식이 필요하다.
SSE에서 이를 해결하기 위해 휴리스틱 방법으로 어떤 경로를 탐색할지 결정한다.
대표적인 휴리스틱 기법으로는 깊이 우선 탐색(DFS, Depth-First Search)이 있다. 경로 하나를 선택한 후 이를 완전히 탐색한 뒤 다음 경로를 향하는 방법인데, 이는 흥미로운 코드가 중첩된 코드 중 가장 깊은 곳에 있다는 가정을 기반으로 한다.
또는 너비 우선 탐색(BFS, Breath-First Search)도 대안이 될 수 있다. 이는 모든 경로를 병렬적으로 탐색하므로, 깊은 코드에 도달할 때까지 많은 시간이 필요하다.
DSE는 한 번에 하나의 경로만을 탐색할 수 있지만 path explosion을 해결하기 위해 휴리스틱 알고리즘을 추가하거나 모든 경로를 탐색할 수도 있다.
DSE에서 여러 경로를 탐색하는 가장 간단한 방식은 branch constraint를 뒤집는(flip) 것이다. 더 정교한 방식으로는 프로그램 상태의 스냅샷을 생성해 탐색 이후 다시 복원하는 방법이 있다.
Increasing the Scalability of Symbolic Execution
Simplifying Constraints
기호 실행에서 계산 비용이 가장 많이 드는 작업 중 하나는 constraint solving이다. 따라서 조건 자체를 단순화하고 solver의 사용을 최소화하는 것이 중요하다.
- 기호로 표현할 변수의 개수 제한하기(Limiting the number of symbolic variables)
먼저 간단히 symbolic variable의 개수를 줄이고 나머지 프로그램 상태들을 구체적인 값으로 특정하는 방법이 있다. 이때 concrete로 특정할 상태 값을 적절하게 정하는 것이 중요하다.
예를 들어 너무 많은 대상을 concrete로 특정하는 경우 현실 시간 안에 해를 찾을 수 없을 것이고, 반대로 특정해야 할 대상을 놓친다면 원하는 결과를 도출할 수 없게 될 것이다.
결국 분석 시 목표로 하는 상황에 직접적으로 영향을 미치는 부분만을 선별해 기호화하는 것이 중요하다.
이를 위해 DSE 도구들은 일종의 전처리 과정을 수행해 오염 분석이나 퍼징(fuzzing) 등의 기법을 먼저 적용해 필요한 정보를 미리 찾아내는 방식을 사용한다. 이렇게 상대적으로 자원 소모가 적은 DTA나 퍼징 기법 등을 이용하면 기호로 표현된 제약 조건의 복잡도를 낮춰준다.
- 기호로 표현할 연산의 수 제한하기(Limiting the number of symbolic operations)
또 다른 방법은 관련이 있는 명령어에만 기호 실행을 적용하는 것이다.
예를 들어 rax 레지스터를 이용한 간접 호출로 인해 발생할 수 있는 취약점을 탐지하고 싶다고 하자. 그러면 rax 레지스터를 처리하는 명령어를 골라내기 위해 backward slice를 계산하고, 슬라이스 내의 명령어들만을 기호로 처리하면 된다.
- 기호 메모리 공간 단순화하기(Simplifying symbolic memory)
full symbolic memory를 사용할 때 구체적인 경계 설정이 제공되지 않은 경우 가능한 상태의 수와 제약 조건의 수가 많아져서 경로 폭발 문제가 발생할 수 있다. 이는 제약 조건식에서 일부를 concretizing하여 복잡도를 낮추는 방식으로 문제를 해결하려 할 수 있다.
Triton과 같은 symbex 엔진은 메모리 접근에 대한 가정을 단순화하는 방식을 사용하기도 한다.
Avoiding the Constraint Solver
constraint solver의 필요성 자체를 최소화하는 방법이 있다.
전처리 과정을 통해 유의미한 경로와 입력값을 찾은 후에 이를 symbex 엔진으로 탐색하면, 해당 입력에 영향을 받는 명령어를 찾을 수 있다. 그러면 흥미롭지 않은 경로나 명령어에 대한 constraint solver의 계산이 불필요해진다.
symbex 엔진과 constraint solver는 이전에 확인한 (하위) 수식의 결과를 cache 할 수 있으므로 동일한 수식을 두 번 풀 필요가 없다.
Summary
symbex에는 조정할 수 있는 많은 요소가 있고 목표에 따라 최적의 구성이 달라진다.
예를 들어, Triton과 angr는 바이너리 수준의 symbex 엔진이며 애플리케이션 수준의 SSE와 DSE를 제공한다.
S2E는 바이너리에 대해 동작하는데 전체 시스템에 가상머신 기술을 적용하기 때문에 커널, 드라이버 등에 대해서도 기호 실행을 수행할 수 있다.
KLEE는 고전적인 SSE 기능을 제공하는데, 바이너리 코드가 아닌 LLVM bitcode에 대해서 온라인 방식으로 수행한다. 특히 path coverage를 위해 다수의 휴리스틱 알고리즘을 지원한다.
참고 및 인용
[1] https://practicalbinaryanalysis.com/
[2] http://www.acornpub.co.kr/book/binary-analysis
[3] https://hexterisk.github.io/blog/posts/
Uploaded by Notion2Tistory v1.1.0