Introduction

이전에 Angr와 Symbolic Execution을 이용한 연구를 진행한 적이 있었습니다.
그 때 알게된 내용과 추가적으로 알게된 내용을 정리해보고자 합니다 😁

p.s. Angr가 워낙 방대하고 다룰 내용이 많아서 시리즈로 진행할 것 같습니다!

Angr는 Symbolic Execution(동적 기호실행)과 바이너리에 대한 다양한 정적 분석 수행 기능을 갖춘 다목적 바이너리 분석 플랫폼입니다.
보안 연구, 취약점 분석, 역공학 등에 유용하게 사용되며, 아직까지 활발하게 contribute되고 있는 프로젝트입니다.
Angr (Github)
Angr (official documentation - Introduction)

Goals

바이너리를 프로그래밍 방식으로 분석하기 위해서는 아래 과제들을 해결해야하며, Angr의 장점은 이를 수행할 수 있는 기능들을 전부 가지고 있다는 것 입니다:)

1. 바이너리를을 로드합니다.
2. 바이너리를 중간 표현으로 변환합니다.
3. 정적/동적 분석을 수행합니다.
    3.1. 부분 또는 전체 프로그램의 정적 분석 (i.e. 제어 흐름 그래프, 종속성 분석, 프로그램 슬라이싱)
    3.2. 상태 공간에 대한 동적 분석 (i.e. 기호실행, 경로탐색)

정적 분석: 프로그램을 실행하지 않고 코드를 분석하는 기술
동적 분석: 프로그램을 실행하여 코드를 분석하는 기술

바이너리 로드
Angr는 다양한 파일 포맷과 아키텍처를 지원합니다.

중간 표현(Intermediate Representation, IR)
소스 코드를 표현하기 위해 컴파일러 또는 가상 시스템에서 내부적으로 사용하는 데이터 구조 또는 코드
Angr는 바이너리를 IR로 변환하여, 바이너리의 기계어 명령어를 보다 추상적인 형태로 분석할 수 있게 합니다.
이를 통해 복잡한 바이너리 코드를 더 쉽게 분석할 수 있습니다.

제어 흐름 그래프(Control Flow Graph, CFG)
프로그램이 실행 중에 횡단할 수 있는 모든 경로를 그래프 표기법을 사용하여 나타낸 것
프로그램의 구조를 파악할 수 있고, 특정 경로의 “비도달성”을 판단할 수 있는 장점이 있습니다.

종속성 분석(Dependency Analysis)
프로그램 내의 요소(변수, 함수 등) 간의 의존 관계를 분석하는 것
민감한 데이터나 기능에 접근할 수 있는 경로를 파악할 수 있어, 취약한 함수를 실제 공격으로 연결하는 데 편리합니다.

프로그램 슬라이싱(Program Slicing)
프로그램 내의 한 지점으로부터 특정 변수에 직, 간접적으로 영향을 주는 모든 문장들을 추출하는 기법
분석자의 입장에서 보면, 취약한 함수를 발견했을 때 공격 가능성을 분석하기 매우 유용한 기법입니다.

i.e. 10번째 줄의 system(x)에 영향을 미치는 모든 문장들을 가져오기

기호 실행(Symbolic Execution)
입력값을 구체적인 값 대신 기호로 대체하여 프로그램의 실행 경로를 분석하는 방법
모든 가능한 실행 경로를 탐색하고, 각 경로에서 발생할 수 있는 다양한 상태를 추적할 수 있습니다.
광범위한 자동화 취약점 분석에 유용하게 사용할 수 있습니다.

경로 탐색(Path Exploration)
프로그램의 다양한 실행 경로를 탐색하는 과정
기호 실행(Symbolic Execution)과 구체적 실행(Concrete Execution)을 따로 혹은 조합해 수행할 수 있습니다.
의도한 프로그램의 특정 상태에 도달할 수 있는 가능성을 파악하는 데 편리합니다.

Installation

Angr는 python 3.8+ 용 라이브러리로, 사용을 위해선 Python을 설치해야 합니다.

Installing from PyPI**

root:/$ pip install angr

Installing from Source**

root:/$ sudo apt-get install python3-dev build-essential
root:/$ pip install -r requirements.txt

Getting Started

Angr는 여러 하위 프로젝트들이 존재하며, Angr와 상호작용하며 사용됩니다.
빠른 이해를 위해 Angr Core에 들어가기 앞서 CLE와 Claripy를 짚고 넘어가도록 하겠습니다.

CLE

바이너리 및 관련 라이브러리를 로드하고 프로세스 메모리를 추상화하는 작업을 돕는 라이브러리입니다.

p.s. 개인적인 견해로, Decompiler API(i.e. Binary Ninja API, IDApython, …)와 비슷한 역할을 하는 것 같습니다.

Loader

CLE의 핵심 클래스로, 바이너리에서 가상 주소 공간으로의 표현(representation)을 처리합니다.
이를 통해 바이너리의 함수(function), 데이터(data), 심볼(symbol), 섹션(section), 세그먼트(segment) 등에 접근할 수 있습니다.

import cle

loader = cle.Loader('test')
# <Loaded prob, maps [0x400000:0x807fff]>

loader.min_addr
# 4194304

loader.max_addr
# 8421375

loader.all_objects
# [<ELF Object chall, maps [0x400000:0x40676f]>, <ExternObject Object cle##externs, maps [0x500000:0x500040]>, <ExternObject Object cle##externs, maps [0x600000:0x607fff]>, <ELFTLSObjectV2 Object cle##tls, maps [0x700000:0x71500f]>, <KernelObject Object cle##kernel, maps [0x800000:0x807fff]>]

loader.main_object
# <ELF Object chall, maps [0x400000:0x4041a7]>

loader.shared_objects
# OrderedDict([('chall', <ELF Object chall, maps [0x400000:0x4041a7]>), ('extern-address space', <ExternObject Object cle##externs, maps [0x600000:0x607fff]>), ('cle##tls', <ELFTLSObjectV2 Object cle##tls, maps [0x700000:0x71500f]>)])

loader.extern_object
# <ExternObject Object cle##externs, maps [0x500000:0x500040]>

loader.kernel_object
# <KernelObject Object cle##kernel, maps [0x800000:0x807fff]>

Backend

CLE는 특정 파일 형식(ELF, PE, ...)들을 처리하기 위해 Backend라는 기능을 제공합니다.
즉, 각 바이너리 객체는 Loader Backend(cle.backend 의 하위 클래스)에 의해 로드됩니다.
CLE는 대부분의 경우에 자동으로 맞는 형식(Backend)을 찾아주므로, 따로 지정할 필요가 없습니다.

지원되는 Backend 종류는 다음과 같습니다.

또한 다음과 같은 속성들을 이용해 빠르게 분석을 수행할 수 있습니다.
이하 설명은 전부 각각의 객체 클래스에 적용됩니다. (i.e. cle.backend.elf.elf.ELF)

obj = loader.main_object
# <ELF Object chall, maps [0x400000:0x40676f]>

obj.entry
# 4198720

obj.min_addr
# 4194304

obj.max_addr
# 4220783

obj.segments
# <Regions: [<ELFSegment flags=0x4, relro=0x0, vaddr=0x400000, memsize=0x7d8, filesize=0x7d8, offset=0x0>, ... <ELFSegment flags=0x6, relro=0x0, vaddr=0x404000, memsize=0x2770, filesize=0x10, offset=0x3000>]>

obj.sections
# <Regions: [<Unnamed | offset 0x0, vaddr 0x400000, size 0x0>, <.interp | offset 0x318, vaddr 0x400318, size 0x1c>, ... <.shstrtab | offset 0x303b, vaddr 0x400000, size 0x10a>]>

obj.plt["getc"]
# 4198704

obj.reverse_plt[0x401130]
# 'getc'

loader.main_object.execstack
# False

loader.main_object.pic
# True

loader.main_object.imports
# {'__libc_start_main': <cle.backends.elf.relocation.amd64.R_X86_64_GLOB_DAT object at 0x7fb18cf51600>, '_ITM_deregisterTMCloneTable': <cle.backends.elf.relocation.amd64.R_X86_64_GLOB_DAT object at 0x7fb18cf516c0>, ... 'getc': <cle.backends.elf.relocation.amd64.R_X86_64_JUMP_SLOT object at 0x7fb18cf519c0>}

Symbol & Relocations

CLE를 사용하는 동안 Symbol(기호, 이하 Symbol)을 이용하여 작업할 수 있습니다.
기호를 이용하는 가장 쉬운 방법은 이름/주소를 받고 Symbol을 반환하는 함수를 사용하는 것 입니다.

i.e. find_symbol(“getc”)

Symbol for Debug Informations

Symbol을 사용해 디버깅에 필요한 여러 정보를 얻을 수 있습니다.
Symbol 객체를 통해 주소를 나타내는 방법이 3가지가 있습니다.
전역 공간에서의 주소, 바이너리에서의 상대 주소, 객체 기반의 상대 주소

# find_symbol
sym = loader.find_symbol("getc")
# <Symbol "getc" in cle##externs at 0x500040>

sym.name
# 'getc'

sym.owner
# <ExternObject Object cle##externs, maps [0x500000:0x500040]>

sym.rebased_addr
# 5242944

sym.linked_addr
# 32

sym.relative_addr
# 32

Symbol for Dynamic Linking

Symbol을 이용해 동적 연결에 대한 정보를 얻을 수 있습니다.

sym.is_export
# True

sym.is_import
# False

sym.resolvedby
# <Symbol "getc" in libc.so.6 at 0x500040>

Claripy

Claripy는 Angr의 Solver Engine으로, Claripy ASTs는 Concrete/Symbolic한 표현과 상호작용하는 방법을 정의합니다.
Claripy AST는 Claripy가 지원하는 수학적 구성 간의 차이를 추상화하여 트리처럼 나타냅니다.
* AST(Abstract Syntax Tree)

AST

AST는 “해당 연산의 출력이 제공되면, 입력은 어떤 값인가?” 라는 질문을 SMT Solver 형식으로 변환합니다.
예를 들어, 다음과 같은 연산식에서 x를 표현하는 것이 SMT Solver의 역할입니다.

\(sequence: x + y = 1, result: 3\)
\(x = 2 - y\)

x = claripy.BVS("x", 64)
seq = x + 10

x.op
# 'BVS'

seq.op
# '__add__'

seq.args
# (<BV64 x_0_64>, <BV64 0xa>)

BV(Bit-Vector)

Bit-Vector로, 크기(Bit size)와 함께 Symbolic 또는 concrete(with value)하게 설정할 수 있습니다.
Symbolic: Bit-Vector의 값이 정해지지 않고, 변수와 같이 기호로 표현
Concrete: Bit-Vector의 값이 구체적인 숫자로 정해져서 표현

BV는 사용하지 않으며(deprecated), 대신 BVV, BVS를 사용합니다.

Q. BV(Bit-Vector)를 사용하는 이유
일반적으로 python의 정수형은 overflow/underflow가 발생하지 않습니다.
만일 이 python의 정수형으로 시뮬레이션을 진행하면, 변수 크기에 제한이 없으므로 아무 오류 없이 끝없이 작아지거나 커지는 현상이 생기게 됩니다.
(또한 해당 변수의 크기가 int, char, 등으로 다를 수 있는 점도 연산 시 고려가 불가능합니다)

따라서 이 문제를 해결하기 위해 BV를 사용합니다.

BVS(Bit-Vector Symbolic)

Symbolic한 Bit-Vector를 생성하는 함수

# 32bit symbolic bit-vector "x"
claripy.BVS("x", 32)
# <BV32 x_1_32>

BVV(Bit-Vector Value)

Concrete한 Bit-Vector를 생성하는 함수

# 32bit concrete bit-vector of "0xdeadbeef"
claripy.BVV(0xdeadbeef, 32)
# <BV32 0xdeadbeef>

비트 확장(Bit Extend)

크기가 다른 Bit-Vector들을 연산할 경우 오류가 발생하기 때문에, 제로(zero)/부호(sign) 확장을 사용해서 크기를 맞춰주어야 합니다.
zero_extend는 Bit-Vector의 왼쪽에 주어진 숫자만큼 zero bit를 채워줍니다.
sign_extend는 Bit-Vector의 왼쪽에 주어진 숫자만큼 최상위 비트의 값을 채워줍니다

simgr.solver.BVV(0x100, 32)
simgr.solver.BVV(0x100, 64)

a
# <BV32 0x100>

b
# <BV64 0x100>

a + b
# claripy.errors.ClaripyOperationError: args length must all be equal

두 Bit-Vector의 크기가 달라 오류가 발생하는 모습

a
# <BV32 0x100>

a.zero_extend(32)
# <BV64 0x100>

a.zero_extend(32) + b
# <BV64 0x200>

a
# <BV32 0x100>

a.sign_extend(32)
# <BV64 0x100>

a.sign_extend(32) + b
# <BV64 0x200>

제로(zero)/부호(sign) 확장을 사용해 연산이 가능해진 모습

FP(Floating Point)

IEEE754 floating point number(부동소수점 숫자)를 표현하기 위해 사용하며, BackendConcrete, BackendZ3 에서 지원합니다.

FPS(Floating Point Symbolic)

Symbolic한 floating point number(부동소수점 숫자)를 생성하는 함수

# symbolic floating point "x"
claripy.FPS('x', claripy.fp.FSORT_FLOAT)
# <FP32 FPS(FP_x_6_32, FLOAT)>

FPV(Floating Point Value)

Concrete한 floating point number(부동소수점 숫자)를 생성하는 함수

# floating point value of 3.2
claripy.FPV(3.2, claripy.fp.FSORT_DOUBLE)
# <FP64 FPV(3.2, DOUBLE)>

Bool

Boolean 연산을 수행하는 데 사용하며, BackendConcrete, BackendVSA , BackendZ3 에서 지원합니다.

x = claripy.BVS('x', 32)
y = claripy.BVS('y', 32)

cmp = x == y
cmp
# <Bool x_7_32 == y_8_32>

Solver

Claripy Solver를 사용해 연산을 수행할 수 있습니다.
Bit-Vector를 이용해 제약조건을 추가하고, 해를 하나 혹은 여러 개 출력하거나 해가 존재하는 지 확인할 수 있습니다.

s = claripy.Solver()
# <claripy.solvers.Solver object at 0x7fd930d21510>

add

연산식에 제약 조건을 추가하는 함수

x = claripy.BVS("x", 64)

s.add(x > 100)
# (<Bool x_0_64 > 0x64>,)

s.add(x < 105)
# (<Bool x_0_64 < 0x69>,)

satisfiable

해당 state가 만족가능한지(명제가 만족가능한지)를 판단하는 함수

s.satisfiable()
# True

# if x = x + 1
s.add(x==x+1)
# (<Bool x_0_64 == x_0_64 + 0x1>,)

s.satisfiable()
# False

eval

표현식 expr에 대해 최대 n개의 해를 반환합니다.
Bit-Vector를 python으로 바꾸는 역할(즉, 해를 구하는 역할)을 합니다.

s.eval(x, 1)
# (101, )

# 최대 n이라 해가 5개 미만이더라도 오류는 나지 않습니다.
s.eval(x, 5)
# (101, 102, 103, 104)

min / max

표현식 해의 최소/최대 개수를 출력하는 함수

s.min(x)
# 101

s.max(x)
# 104

Conclusion

이번 포스트에서는 Angr의 개념, Claripy와 CLE를 간단하게 정리하였습니다.
다음 포스트엔 Angr Core를 공부하고, 직접 사용해보려고 합니다.

References

• Control-flow graph - Wikipedia
• IR(Intermediate Representation) - Lazenca
• Program Slicing - Wikipedia
• 최준우, 김요셉, 최철순, 이정민, 안우현. (2011-11-25). 바이너리 실행파일을 위한 정적 프로그램 슬라이서의 설계 및 구현. 한국정보과학회 학술발표논문집, 서울.
• Symbolic Execution - Wikipedia
• angr official documentation
• angr - (2) Claripy
• System/Linux/Angr 정리