barf project
1.0.0
이진 코드의 분석은 소프트웨어 보안 및 프로그램 분석에서 리버스 엔지니어링에 이르는 컴퓨터 과학 및 소프트웨어 엔지니어링 분야의 많은 영역에서 중요한 활동입니다. 수동 바이너리 분석은 어렵고 시간이 많이 걸리는 작업이며 인간 분석가를 자동화하거나 지원하려는 소프트웨어 도구가 있습니다. 그러나 이러한 도구의 대부분은 학업 및 실무자 커뮤니티의 상당 부분에 의해 액세스 및 사용을 제한하는 몇 가지 기술 및 상업적 제한 사항이 있습니다. BARF 는 정보 보안 분야에서 공통적 인 광범위한 이진 코드 분석 작업을 지원하는 오픈 소스 바이너리 분석 프레임 워크입니다. 여러 아키텍처에서 이진 번역에서 중간 표현으로의 이진 번역, 코드 분석 플러그인을위한 확장 가능한 프레임 워크 및 디버거, SMT 솔버 및 계측 도구와 같은 외부 도구와의 상호 작용을 지원하는 스크립트 가능한 플랫폼입니다. 이 프레임 워크는 주로 인간 보조 분석을 위해 설계되었지만 완전히 자동화 할 수 있습니다.
BARF 프로젝트 에는 BARF 및 관련 도구 및 패키지가 포함됩니다. 지금까지 프로젝트는 다음 항목으로 구성됩니다.
자세한 내용은 다음을 참조하십시오.
현재 상태 :
| 최신 릴리스 | 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 |
모든 패키지는 우분투 16.04 (x86_64)에서 테스트되었습니다.
BARF 는 바이너리 분석 및 역 엔지니어링을위한 파이썬 패키지입니다. 그것은 할 수 있습니다 :
ELF , PE 등)으로로드합니다.현재 개발 중 입니다.
Barf는 다음 SMT 솔버에 따라 다릅니다.
다음 명령은 시스템에 BARF를 설치합니다.
$ sudo python setup.py install로컬로 설치할 수도 있습니다.
$ sudo python setup.py install --usersudo pip install pyasmjitsudo 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!" )예제 디렉토리에서 이러한 예와 더 많은 예를 볼 수 있습니다.
프레임 워크는 코어 , 아치 및 분석의 세 가지 주요 구성 요소로 나뉩니다.
이 구성 요소에는 필수 모듈이 포함됩니다.
REIL : Reil 언어에 대한 정의를 제공합니다. 또한 에뮬레이터 와 파서를 구현합니다.SMT : Z3 및 CVC4 SMT 솔버와 인터페이스하는 수단을 제공합니다. 또한 REIL 명령을 SMT 표현식으로 변환하는 기능을 제공합니다.BI : 바이너리 인터페이스 모듈은 처리를 위해 이진 파일을로드 할 책임이 있습니다 (Pefile 및 PyelfTools를 사용합니다.) 각 지원되는 아키텍처는 다음 모듈을 포함하는 하위 구성 요소로 제공됩니다.
Architecture : 아키텍처, 즉 레지스터, 메모리 주소 크기를 설명합니다.Translator : 각 지원 된 지시에 따라 번역기를 Reil에게 제공합니다.Disassembler : 분해 기능을 제공합니다 (캡 스톤을 사용합니다.)Parser : 명령어를 문자열에서 객체 양식으로 변환합니다. 지금 까지이 구성 요소는 모듈로 구성됩니다 : 제어 흐름 그래프 , Call Graph 및 Code Analyzer . 첫 번째 두 개는 각각 CFG 및 CG 복구에 대한 기능을 제공합니다. 후자는 SMT 솔버 관련 기능에 대한 높은 수준의 인터페이스입니다.
BARFgadgets 는 Barf에 구축 된 Python 스크립트로 바이너리 프로그램 내에서 ROP 기기를 검색 하고 분류 하고 확인할 수 있습니다. 검색 단계는 이진 내부에서 모든 ret , jmp 및 call -엔드 가젯을 찾습니다. 분류 단계는 다음 유형에 따라 이전에 발견 된 가제트를 분류합니다.
이것은 지시 에뮬레이션을 통해 이루어집니다. 마지막으로, 검증 단계는 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 는 바프에 구축 된 파이썬 스크립트로 바이너리 프로그램의 제어 흐름 그래프를 복구 할 수 있습니다.
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 는 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은 x86_64/ARM 어셈블리 코드 생성 및 실행을위한 Python 패키지입니다.
이 패키지는 x86_64/arm에서 reil로 BARF 명령어 변환을 테스트하기 위해 개발되었습니다. 주요 아이디어는 코드 조각을 기본적으로 실행할 수 있다는 것입니다. 그런 다음 동일한 단편을 Reil로 번역하고 Reil VM에서 실행됩니다. 마지막으로, 최종 컨텍스트 (기본 실행을 통해 얻은 것과 에뮬레이션에서 얻은 것)는 차이점을 비교합니다.
자세한 내용은 Pyasmjit을 참조하십시오.
BSD 2-Clause 라이센스. 자세한 내용은 라이센스를 참조하십시오.
