0. 요약
MAYHEM이란
실행가능한 바이너리 프로그램들에서 익스플로잇 가능한 버그를 자동으로 찾는 새로운 시스템이다.
MAYHEM에 의해 보고된 모든 버그들은 working shell-spawning 익스플로잇을 동반한다. working 익스플로잇은 soundness(재현가능성)을 보장하고 메이헴이 발견한 버그들은 보안상 치명적이고 실행가능(actionable)하다.
우리는 MAYHEM을 사용하여 Linux와 Windows 프로그램 모두에서 29개의 익스플로잇 가능한 취약점을 찾아 입증했으며, 그 중 2개는 이전에 알려지지않은 취약점 이었다.
MAYHEM(바이너리 레벨 익스플로잇 자동생성)의 과제
MAYHEM은 디버깅 정보없이 바이너리 코드 그 자체를 대상으로 작동한다.
바이너리 레벨에서 익스플로잇 생성을 가능하게 하기위해, MAYHEM이 기술적으로 극복해야할 두가지 핵심과제가 있다. 메모리 소모없이 실행경로를 능동적으로(actively) 관리하고, load나 store 주소가 사용자 입력에 따라 달라지는 symbolic 메모리 인덱스에 대한 추론이 필요하다.
과제 해결을 위한 두가지 기술제안
이를 위해, 우리는 두가지 새로운 기술을 제안한다. :
1) hybrid symbolic execution : 온라인과 오프라인(concolic) 실행을 결합하여 두 기술의 이점을 극대화하기 위한 하이브리드 기호 실행 (메모리 소모 방지)
2) index-based memory modeling : 인덱스 기반 메모리 모델링 : MAYHEM이 바이너리 수준에서 심볼릭 메모리에 대해 효율적으로 추론할 수 있도록 하는 기술. (심볼릭 메모리 인덱스 추론)
1. 서론
MAYHEM의 목표와 등장배경
익스플로잇 가능한 버그는 보안상 치명적인 위험을 유발할 수 있기 때문에, 버그를 찾을때의 핵심은 단순히 버그가 있냐 없냐가 아니라 찾은 버그가 익스플로잇 가능한지 여부이다.
이 문서에서는 바이너리(즉, 실행 가능한) 프로그램에서 익스플로잇 가능한 버그를 자동으로 찾는 시스템인 MAYHEM을 제시한다.
MAYHEM의 동작
MAYHEM은 보고하는 각 버그에 대해 작동 중인 controlhijack 익스플로잇을 생성하므로 각 버그 report가 실행 가능하고 중요한 버그임(bug report is actionable and security-critical)을 보장한다.
MAYHEM은 우리의 이전 연구인 AEG에서 소개한 기본원리에 근거해서 익스플로잇을 감지하고 생성한다.
high-level에서 MAYHEM은 잠재적으로 취약할 가능성이 있는 프로그램의 포인트에 있는 추가적인 constraints를 이용해 심볼릭 익스큐션을 보강함으로써 익스플로잇 가능한 경로를 찾는다.
제약 조건에는 instruction pointer를 리디렉션(IP를 맘대로 조작)할 수 있는지 여부, 공격 코드를 메모리에 배치할 수 있는지 여부, 궁극적으로 공격자의 코드를 실행할 수 있는지 여부와 같은 세부 정보가 포함된다. 해당 정보들을 토대로 resulting formula를 구성하고 resulting formula가 만족되면, 익스플로잇이 가능하다.
MAYHEM의 4가지 디자인 원칙(design principle)
익스플로잇 생성(익스플로잇 재너레이션)의 가장 중요한 과제는 익스플로잇 가능한 경로를 찾기위해 어플리케이션의 state space를 충분히 탐색하는 것이다.
이 문제를 해결하기 위해 MAYHEM의 디자인은 4가지 주요 원칙을 기반으로 한다.
- 시스템은 주어진 리소스(특히 메모리)를 초과하지 않고 임의의 시간 동안(이상적으로는 "영구적으로" 실행) 진행될 수 있어야 한다.
- 성능을 최대화하기 위해 시스템은 작업을 반복하지 않아야 하며
- 시스템은 작업(work)을 버리지 않아야 한다. 시스템의 이전 분석 결과는 이어지는 다음번 실행에서 다시금 사용할 수 있어야 한다.
- 시스템은 load 또는 store 주소가 사용자 입력에 의존하는 심볼릭 메모리에 대해 추론할 수 있어야 한다.
기존 기술의 한계
Principle #1은 복잡한 어플리케이션을 실행하는 데 필요하다. 중요한 용도로 사용되는 프로그램들은 대부분 잠재적으로 탐색할 수 있는 무한한 수의 경로가 포함되어 있기 때문이다.
최근의 심볼릭 익스큐션에 대한 접근법. 예를들면 CUTE [26], BitBlaze [5], KLEE [9], SAGE [13], McVeto [27], AEG [2], S2E [28], and others [3], [21]와 같은 것들은 위의 디자인 포인트를 만족하지 않는다.
온라인 오프라인 executor 모두 principle #1-#3를 만족하지 못한다. 추가로 대부분의 심볼릭 익스큐션 엔진은 심볼릭 메모리에 대해 추론하지 않으므로 principle #4를 충족하지 않는다.
*Symbolic executor
- 개념적으로, 현재 executor들은 두가지 주요한 범주로 나눌 수 있다.
- 하나는 오프라인 executor이다. 오프라인 익스큐터는 하나의 실행경로를 구체적으로(concretely)실행한 다음 기호(symbolically)를 이용해서 실행한다. 오프라인 executor는 trace-based 또는 concolic executor라고 부르기도 한다.
- 나머지 또 한가지는 온라인 executor이다. 온라인 executor는 한번의 시스템 실행에서 실행가능한 모든 경로를 실행하려고 시도한다.
offline symbolic execution의 한계
오프라인 심볼릭 익스큐터는 한번에 하나의 실행경로를 추론한다. Principle #1은 탐색할 새로운 경로를 반복적으로 선택함으로써 충족된다.
또한 시스템의 모든 실행은 다른 실행들과 독립적이기때문에 이전 실행의 결과를 즉시 재사용할 수 있다. 때문에 principle #3를 만족할 수 있다.
하지만, 오프라인은 principle #2를 만족하지 못한다. 시스템을 매번실행할때마다 처음부터 프로그램을 다시시작해야한다.
개념적으로, 모든 실행 추적(execution trace)에 대해 동일한 명령을 반복적으로 실행해야한다. 우리의 실험결과는 이러한 재실행이 매우 부담될 수 있음(expensive)을 보여준다.
online symbolic execution의 한계
온라인 심볼릭 익스큐션은 각 분기 포인트마다 포크한다.
이전의 인스트럭션들은 절대로 다시 실행되지않는다, 그러나 계속되는 forking은 메모리에 부담을 주어 분기수가 증가할수록 실행엔진이 느려진다. ⇒ principle #2 만족
결과로 더이상 진행되지않고 그러므로 principles #1과 #3를 만족시킬 수 없다. KLEE와 같은 몇가지 온라인 익스큐터는 메모리 사용에 의해 느려지는 것을 방지하기위해 forking을 중단한다.
이런 익스큐터는 principle #1을 만족하지만 principle #3는 만족하지 못할때가 있다. (흥미있는 경로가 제거될 가능성이 있다.)
하이브리드 익스큐션 제안
MAYHEM은 온라인과 오프라인 심볼릭 익스큐션 실행을 번걸아가면서 실행하는 하이브리드 볼릭 익스큐션을 도입하여 두가지의 장점(principle #1 #3)을 결합한다.
하이브리드 익스큐션은 OS에서의 메모리 메니저처럼 작동한다. 메모리 메니저와 다른 점은 심볼릭 실행 엔진을 효율적으로 교체(swap out)하도록 설계되었다는 점 뿐이다.
메모리가 부족하면 하이브리드 엔진은 실행중인 익스큐터를 선택하고 현재 실행 상태를 경로 공식(path formula)을 저장한다.
수식(formula)를 복원하고 이전 실행상태까지 프로그램을 구체적으로 실행(concretely running)한 다음 스레드가 복원된다.
경로공식을 캐싱하면 오프라인에서의 병목현상인 instruction의 심볼릭 재실행을 방지하면서 온라인 실행보다 메모리를 더 효율적으로 관리할 수 있다.
MAYHEM은 또한 심볼릭 메모리에 대해 효율적으로 추론하는 기술을 제안한다. load 또는 store 주소가 입력에 의존할 때 심볼릭 메모리 액세스가 발생힌다.
심볼릭 포인터는 바이너리 수준에서 매우 일반적이며 이에 대해 추론할 수 있어야 controlhijack 익스플로잇을 생성할 수 있다.
인덱스기반 메모리모델(index-based memory modeling) 제안
사실, 우리의 실험에 따르면 생성된 익스플로잇의 40%는 구체화 제약(concretization constraints)으로 인해 불가능했을 것이다(§VIII). 이 문제를 극복하기 위해 MAYHEM은 가능한 한 인덱스의 제약을 피하기 위해 인덱스 기반 메모리 모델(γV)을 사용한다.
결과는 고무적이다. 새로운 연구를 위한 충분한 여지가 있지만, MAYHEM은 현재 29개의 다른 프로그램에 대한 버퍼 오버플로, 함수 포인터 덮어쓰기 및 형식 문자열 취약점과 같은 여러 보안 취약점에 대한 익스플로잇을 생성한다.
전반적인 기여(Overall Contributions)
전반적으로 MAYHEM은 다음과 같은 기여를 하고 있다.
- 하이브리드 익스큐션. (Hybrid execution) 우리는 속도와 메모리 요구 사항 간의 더 나은 균형을 찾을 수 있도록 하는 하이브리드 기호 실행이라고 하는 기호 실행을 위한 새로운 체계를 도입합니다. 하이브리드 실행을 통해 MAYHEM은 기존 접근 방식보다 빠르게 여러 경로를 탐색할 수 있습니다(§IV 참조).
- 인덱스 기반 메모리 모델링. (ndex-based memory modeling) 이진 수준에서 심볼릭 인덱스를 처리하기 위한 실용적인 접근 방식으로 인덱스 기반 메모리 모델을 제안합니다. (§V 참조).
- 바이너리 전용 익스플로잇 생성. (Binary-only exploit generation) 우리는 작동하는 컨트롤 하이재킹 익스플로잇을 결과로 내어 익스플로잇 가능성을 보여주는 최초의 엔드 투 엔드 바이너리 전용 익스플로잇 가능한 버그 찾기 시스템을 제시합니다.
