BARF : 바이너리 분석 및 리버스 엔지니어링 프레임워크

바이너리 코드 분석은 소프트웨어 보안, 프로그램 분석, 리버스 엔지니어링 등 컴퓨터 과학 및 소프트웨어 공학 분야의 여러 영역에서 중요한 활동입니다. 수동 바이너리 분석은 어렵고 시간이 많이 소요되는 작업이며, 이를 자동화하거나 인간 분석가를 지원하는 소프트웨어 도구들이 있습니다. 그러나 이러한 도구 대부분은 기술적 및 상업적 제한이 있어 학계 및 실무 커뮤니티의 많은 부분이 접근 및 사용에 제약을 받습니다. BARF는 정보 보안 분야에서 일반적인 다양한 바이너리 코드 분석 작업을 지원하는 것을 목표로 하는 오픈소스 바이너리 분석 프레임워크입니다. 이는 여러 아키텍처의 명령어 리프팅, 중간 표현으로의 바이너리 변환, 코드 분석 플러그인을 위한 확장 가능한 프레임워크, 디버거, SMT 솔버 및 계측 도구와 같은 외부 도구와의 상호 운용을 지원하는 스크립트 가능한 플랫폼입니다. 이 프레임워크는 주로 인간 지원 분석을 위해 설계되었지만 완전히 자동화될 수도 있습니다.

BARF 프로젝트는 BARF와 관련 도구 및 패키지를 포함합니다. 현재까지 프로젝트는 다음 항목으로 구성되어 있습니다.

BARF : 멀티플랫폼 오픈소스 바이너리 분석 및 리버스 엔지니어링 프레임워크
PyAsmJIT : Intel x86_64 및 ARM 아키텍처를 위한 JIT
BARF 기반 도구:
- BARFgadgets : 바이너리 프로그램 내에서 ROP 가젯을 검색, 분류 및 검증할 수 있습니다.
- BARFcfg : 바이너리 프로그램 함수의 제어 흐름 그래프를 복구할 수 있습니다.
- BARFcg : 바이너리 프로그램 함수의 호출 그래프를 복구할 수 있습니다.

자세한 내용은 다음을 참조하십시오.

BARF: 멀티플랫폼 오픈소스 바이너리 분석 및 리버스 엔지니어링 프레임워크 (백서) [en]
BARFing Gadgets (ekoparty2014 발표) [es]

현재 상태:

최신 릴리스	v0.6.0
URL	https://github.com/programa-stic/barf-project/releases/tag/v0.6.0
변경 로그	https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md

모든 패키지는 Ubuntu 16.04 (x86_64)에서 테스트되었습니다.

BARF

BARF는 바이너리 분석 및 리버스 엔지니어링을 위한 Python 패키지입니다. 다음을 수행할 수 있습니다.

다양한 형식(ELF, PE 등)의 바이너리 프로그램 로드,
32비트 및 64비트 Intel x86 아키텍처 지원,
32비트 ARM 아키텍처 지원,
중간 언어(REIL)로 동작하므로 모든 분석 알고리즘이 아키텍처에 독립적임,
Z3 및 CVC4 SMT 솔버와 통합되어 코드 조각을 수식으로 표현하고 제약 조건을 확인할 수 있습니다.

현재 개발 중입니다.

설치

BARF는 다음 SMT 솔버에 의존합니다.

Z3 : Microsoft Research에서 개발 중인 고성능 정리 증명기.
CVC4 : 만족 가능성 모듈로 이론(SMT) 문제를 위한 효율적인 오픈소스 자동 정리 증명기.

다음 명령어는 시스템에 BARF를 설치합니다.

$ sudo python setup.py install

로컬에 설치할 수도 있습니다.

$ sudo python setup.py install --user

참고

작동하려면 하나의 SMT 솔버만 있으면 됩니다. Z3와 CVC4 중 선택하거나 둘 다 설치할 수 있습니다.
일부 테스트를 실행하려면 먼저 PyAsmJIT를 설치해야 합니다: sudo pip install pyasmjit
Graphviz를 설치해야 할 수도 있습니다: sudo apt-get install graphviz

빠른 시작

다음은 바이너리 파일을 열고 각 명령어를 중간 언어(REIL)로 변환하여 출력하는 매우 간단한 예제입니다.

from barf import BARF

# Open binary file.
barf = BARF("examples/misc/samples/bin/branch4.x86")

# Print assembly instruction.
for addr, asm_instr, reil_instrs in barf.translate():
    print("{:#x} {}".format(addr, asm_instr))

    # Print REIL translation.
    for reil_instr in reil_instrs:
        print("\t{}".format(reil_instr))

CFG를 복구하여 .dot 파일로 저장할 수도 있습니다.

# Recover CFG.
cfg = barf.recover_cfg()

# Save CFG to a .dot file.
cfg.save("branch4.x86_cfg")

SMT 솔버를 사용하여 코드에 대한 제약 조건을 확인할 수 있습니다. 예를 들어, 다음 코드가 있다고 가정해 보겠습니다.

 80483ed:       55                      push   ebp
 80483ee:       89 e5                   mov    ebp,esp
 80483f0:       83 ec 10                sub    esp,0x10
 80483f3:       8b 45 f8                mov    eax,DWORD PTR [ebp-0x8]
 80483f6:       8b 55 f4                mov    edx,DWORD PTR [ebp-0xc]
 80483f9:       01 d0                   add    eax,edx
 80483fb:       83 c0 05                add    eax,0x5
 80483fe:       89 45 fc                mov    DWORD PTR [ebp-0x4],eax
 8048401:       8b 45 fc                mov    eax,DWORD PTR [ebp-0x4]
 8048404:       c9                      leave
 8048405:       c3                      ret

코드를 실행한 후 eax 레지스터에서 특정 값을 얻기 위해 메모리 위치 ebp-0x4, ebp-0x8 및 ebp-0xc에 어떤 값을 할당해야 하는지 알고 싶다고 가정해 보겠습니다.

먼저, 분석기 구성 요소에 명령어를 추가합니다.

from barf import BARF

# Open ELF file
barf = BARF("examples/misc/samples/bin/constraint1.x86")

# Add instructions to analyze.
for addr, asm_instr, reil_instrs in barf.translate(0x80483ed, 0x8048401):
    for reil_instr in reil_instrs:
        barf.code_analyzer.add_instruction(reil_instr)

그런 다음, 각 관심 변수에 대한 표현식을 생성하고 원하는 제약 조건을 추가합니다.

ebp = barf.code_analyzer.get_register_expr("ebp", mode="post")

# Preconditions: set range for variable a and b
a = barf.code_analyzer.get_memory_expr(ebp-0x8, 4, mode="pre")
b = barf.code_analyzer.get_memory_expr(ebp-0xc, 4, mode="pre")

for constr in [a >= 2, a <= 100, b >= 2, b <= 100]:
    barf.code_analyzer.add_constraint(constr)

# Postconditions: set desired value for the result
c = barf.code_analyzer.get_memory_expr(ebp-0x4, 4, mode="post")

for constr in [c >= 26, c <= 28]:
    barf.code_analyzer.add_constraint(constr)

마지막으로, 설정한 제약 조건이 해결 가능한지 확인합니다.

if barf.code_analyzer.check() == 'sat':
    print("[+] Satisfiable! Possible assignments:")

    # Get concrete value for expressions
    a_val = barf.code_analyzer.get_expr_value(a)
    b_val = barf.code_analyzer.get_expr_value(b)
    c_val = barf.code_analyzer.get_expr_value(c)

    # Print values
    print("- a: {0:#010x} ({0})".format(a_val))
    print("- b: {0:#010x} ({0})".format(b_val))
    print("- c: {0:#010x} ({0})".format(c_val))

    assert a_val + b_val + 5 == c_val
else:
    print("[-] Unsatisfiable!")

이 예제 및 더 많은 예제는 examples 디렉토리에서 확인할 수 있습니다.

개요

프레임워크는 코어(core), 아키텍처(arch) 및 **분석(analysis)**의 세 가지 주요 구성 요소로 나뉩니다.

코어(Core)

이 구성 요소는 다음과 같은 필수 모듈을 포함합니다.

REIL: REIL 언어에 대한 정의를 제공합니다. 또한 에뮬레이터와 파서를 구현합니다.
SMT: Z3 및 CVC4 SMT 솔버와의 인터페이스를 제공합니다. 또한 REIL 명령어를 SMT 표현식으로 변환하는 기능을 제공합니다.
BI: 바이너리 인터페이스 모듈은 처리를 위해 바이너리 파일을 로드하는 역할을 합니다(PEFile 및 PyELFTools 사용).

아키텍처(Arch)

지원되는 각 아키텍처는 다음 모듈을 포함하는 하위 구성 요소로 제공됩니다.

Architecture: 아키텍처(레지스터, 메모리 주소 크기 등)를 설명합니다.
Translator: 지원되는 각 명령어에 대한 REIL 변환기를 제공합니다.
Disassembler: 디스어셈블 기능을 제공합니다(Capstone 사용).
Parser: 명령어를 문자열에서 객체 형태로 변환합니다.

분석(Analysis)

현재 이 구성 요소는 제어 흐름 그래프(CFG), 호출 그래프(CG) 및 코드 분석기(Code Analyzer) 모듈로 구성됩니다. 처음 두 개는 각각 CFG 및 CG 복구 기능을 제공합니다. 마지막 모듈은 SMT 솔버 관련 기능에 대한 고수준 인터페이스입니다.

도구

BARFgadgets

BARFgadgets는 BARF를 기반으로 구축된 Python 스크립트로, 바이너리 프로그램 내에서 ROP 가젯을 검색, 분류 및 검증할 수 있습니다. 검색 단계는 바이너리 내에서 ret, jmp 및 call로 끝나는 모든 가젯을 찾습니다. 분류 단계는 이전에 발견된 가젯을 다음 유형에 따라 분류합니다.

No-Operation (NOP),
레지스터 이동,
상수 로드,
산술/논리 연산,
메모리 로드,
메모리 저장,
산술/논리 로드,
산술/논리 저장,
정의되지 않음.

이는 명령어 에뮬레이션을 통해 수행됩니다. 마지막으로, 검증 단계는 SMT 솔버를 사용하여 두 번째 단계에서 각 가젯에 할당된 의미를 확인합니다.

usage: BARFgadgets [-h] [--version] [--bdepth BDEPTH] [--idepth IDEPTH] [-u]
                   [-c] [-v] [-o OUTPUT] [-t] [--sort {addr,depth}] [--color]
                   [--show-binary] [--show-classification] [--show-invalid]
                   [--summary SUMMARY] [-r {8,16,32,64}]
                   filename

Tool for finding, classifying and verifying ROP gadgets.

positional arguments:
  filename              Binary file name.

optional arguments:
  -h, --help            show this help message and exit
  --version             Display version.
  --bdepth BDEPTH       Gadget depth in number of bytes.
  --idepth IDEPTH       Gadget depth in number of instructions.
  -u, --unique          Remove duplicate gadgets (in all steps).
  -c, --classify        Run gadgets classification.
  -v, --verify          Run gadgets verification (includes classification).
  -o OUTPUT, --output OUTPUT
                        Save output to file.
  -t, --time            Print time of each processing step.
  --sort {addr,depth}   Sort gadgets by address or depth (number of
                        instructions) in ascending order.
  --color               Format gadgets with ANSI color sequences, for output
                        in a 256-color terminal or console.
  --show-binary         Show binary code for each gadget.
  --show-classification
                        Show classification for each gadget.
  --show-invalid        Show invalid gadget, i.e., gadgets that were
                        classified but did not pass the verification process.
  --summary SUMMARY     Save summary to file.
  -r {8,16,32,64}       Filter verified gadgets by operands register size.

자세한 내용은 README를 참조하십시오.

BARFcfg

BARFcfg는 BARF를 기반으로 구축된 Python 스크립트로, 바이너리 프로그램의 제어 흐름 그래프를 복구할 수 있습니다.

usage: BARFcfg [-h] [-s SYMBOL_FILE] [-f {txt,pdf,png,dot}] [-t]
               [-d OUTPUT_DIR] [-b] [--show-reil]
               [--immediate-format {hex,dec}] [-a | -r RECOVER]
               filename

Tool for recovering CFG of a binary.

positional arguments:
  filename              Binary file name.

optional arguments:
  -h, --help            show this help message and exit
  -s SYMBOL_FILE, --symbol-file SYMBOL_FILE
                        Load symbols from file.
  -f {txt,pdf,png,dot}, --format {txt,pdf,png,dot}
                        Output format.
  -t, --time            Print process time.
  -d OUTPUT_DIR, --output-dir OUTPUT_DIR
                        Output directory.
  -b, --brief           Brief output.
  --show-reil           Show REIL translation.
  --immediate-format {hex,dec}
                        Output format.
  -a, --recover-all     Recover all functions.
  -r RECOVER, --recover RECOVER
                        Recover specified functions by address (comma
                        separated).

BARFcg

BARFcg는 BARF를 기반으로 구축된 Python 스크립트로, 바이너리 프로그램의 호출 그래프를 복구할 수 있습니다.

usage: BARFcg [-h] [-s SYMBOL_FILE] [-f {pdf,png,dot}] [-t] [-a | -r RECOVER]
              filename

Tool for recovering CG of a binary.

positional arguments:
  filename              Binary file name.

optional arguments:
  -h, --help            show this help message and exit
  -s SYMBOL_FILE, --symbol-file SYMBOL_FILE
                        Load symbols from file.
  -f {pdf,png,dot}, --format {pdf,png,dot}
                        Output format.
  -t, --time            Print process time.
  -a, --recover-all     Recover all functions.
  -r RECOVER, --recover RECOVER
                        Recover specified functions by address (comma
                        separated).

PyAsmJIT

PyAsmJIT는 x86_64/ARM 어셈블리 코드 생성 및 실행을 위한 Python 패키지입니다.

이 패키지는 x86_64/ARM에서 REIL로의 BARF 명령어 변환을 테스트하기 위해 개발되었습니다. 주요 아이디어는 코드 조각을 네이티브로 실행할 수 있게 하는 것입니다. 그런 다음 동일한 조각을 REIL로 변환하여 REIL VM에서 실행합니다. 마지막으로, (네이티브 실행을 통해 얻은) 최종 컨텍스트와 (에뮬레이션을 통해 얻은) 컨텍스트를 비교하여 차이점을 확인합니다.

자세한 내용은 PyAsmJIT를 참조하십시오.

라이선스

BSD 2-Clause License. 자세한 내용은 LICENSE를 참조하십시오.

barf-project

인기