Qsynthesis

QSynthesis는 비트벡터 표현식의 I/O 기반 프로그램 합성을 수행하기 위한 Python3 API입니다. 코드 난독화 해제를 용이하게 하는 것을 목표로 합니다. 이 알고리즘은 블랙박스 I/O 기반 합성과 화이트박스 AST 검색을 결합한 그레이박스 접근 방식으로, 하위 표현식을 합성합니다 (루트 노드를 합성할 수 없는 경우).

이 알고리즘은 원래 BAR 학술 워크숍에서 설명되었습니다:

• QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation (사용된 벤치마크는 여기에서 확인 가능)

이 코드는 다음 Black Hat 발표의 일부로 공개되었습니다:

• Greybox Program Synthesis: A New Approach to Attack Dataflow Obfuscation

면책 조항: 이 프레임워크는 실험적이며, 실험 목적으로만 사용되어야 합니다. 주로 이 분야의 연구를 촉진하는 것을 목표로 합니다.

문서

설치, 예제 및 API 문서는 전용 문서에서 확인할 수 있습니다: Documentation

기능

핵심 합성은 전체 프레임워크가 구축된 Triton 심볼릭 엔진을 기반으로 합니다. 다음과 같은 기능을 제공합니다:

• 비트벡터 표현식의 합성
• SMT를 통한 합성된 표현식의 의미적 동등성 검사 기능
• 상수 합성 기능 (표현식이 상수를 인코딩하는 경우)
• 학습 메커니즘을 통한 오라클(사전 계산된 테이블)의 지속적 개선 기능
• 합성된 표현식을 다시 어셈블리로 재조립하는 기능
• 합성 사용을 용이하게 하기 위해 REST API를 통해 오라클을 제공하는 기능
• 합성 통합을 제공하는 IDA 플러그인

빠른 시작

설치

작동하려면 먼저 Triton이 설치되어 있어야 합니다: 설치 문서. Triton은 가상환경에 자동으로 설치되지 않으므로, venv에 복사하거나 venv 구성 시 --system-site-packages를 사용하십시오.

그런 다음:

$ git clone https://github.com/quarkslab/qsynthesis.git
$ cd qsynthesis
$ pip3 install '.[all]'

[all]은 모든 의존성을 설치합니다 (경량 설치에 대해서는 문서를 참조하십시오).

테이블 생성

합성 알고리즘은 문법 *(변수와 연산자의 집합)*에서 파생된 오라클 테이블을 생성해야 합니다. Qsynthesis 설치 시 테이블을 조작할 수 있는 유틸리티 qsynthesis-table-manager가 제공됩니다. 다음 명령은 64비트 변수 3개, 16개 입력 벡터를 사용하는 5개 연산자로 테이블을 생성합니다. 생성은 500만 항목으로 제한합니다.

$ qsynthesis-table-manager generate -bs 64 --var-num 3 --input-num 16 --random-level 5 --ops AND,NEG,MUL,XOR,NOT --watchdog 80 --limit 5000000 my_oracle_table
Generate Table
Watchdog value: 80.0
Depth 2 (size:3) (Time:0m0.23120s)
Depth 3 (size:21) (Time:0m0.23198s)
Depth 4 (size:574) (Time:0m0.26068s)
Depth 5 (size:400858) (Time:0m21.23231s)
Threshold reached, generation interrupted
Stop required
Depth 5 (size:5000002) (Time:4m52.56009s) [RAM:9.52Gb]

참고: 생성 과정은 RAM을 소모하며, --watchdog은 생성이 중단되는 RAM 비율을 설정할 수 있게 합니다.

비트벡터 표현식 합성

그런 다음 다음과 같이 겉보기에 난독화된 표현식을 단순화할 수 있습니다:

from qsynthesis import SimpleSymExec, TopDownSynthesizer, InputOutputOracleLevelDB

blob = b'UH\x89\xe5H\x89}\xf8H\x89u\xf0H\x89U\xe8H\x89M\xe0L\x89E\xd8H\x8bE' \
       b'\xe0H\xf7\xd0H\x0bE\xf8H\x89\xc2H\x8bE\xe0H\x01\xd0H\x8dH\x01H\x8b' \
       b'E\xf8H+E\xe8H\x8bU\xe8H\xf7\xd2H\x0bU\xf8H\x01\xd2H)\xd0H\x83\xe8' \
       b'\x02H!\xc1H\x8bE\xe0H\xf7\xd0H\x0bE\xf8H\x89\xc2H\x8bE\xe0H\x01\xd0' \
       b'H\x8dp\x01H\x8bE\xf8H+E\xe8H\x8bU\xe8H\xf7\xd2H\x0bU\xf8H\x01\xd2' \
       b'H)\xd0H\x83\xe8\x02H\t\xf0H)\xc1H\x89\xc8H\x83\xe8\x01]\xc3'

# Perform symbolic execution of the instructions
symexec = SimpleSymExec("x86_64")
symexec.initialize_register('rip', 0x40B160)  # arbitrary address
symexec.initialize_register('rsp', 0x800000)  # arbitrary stack
symexec.execute_blob(blob, 0x40B160)
rax = symexec.get_register_ast("rax")  # retrieve rax register expressions

# Load lookup tables
ltm = InputOutputOracleLevelDB.load("my_oracle_table")

# Perform Synthesis of the expression
synthesizer = TopDownSynthesizer(ltm)
synt_rax, simp = synthesizer.synthesize(rax)

print(f"expression: {rax.pp_str}")
print(f"synthesized expression: {synt_rax.pp_str} [{simp}]")

제한 사항

• 합성 정확도는 사전 계산된 테이블의 완전성에 의해 제한됨
• 테이블 생성은 RAM 소비에 의해 제한됨
• 재조립은 메모리 변수를 포함할 수 없으며, 대상은 반드시 레지스터이고 아키텍처는 llvmlite에 의존함 (따라서 대부분 x86_64)
• 코드는 비활성화된 트레이스 기반 합성을 참조함 (기반 프레임워크가 아직 오픈소스가 아니기 때문)

저자

• Robin David (@RobinDavid), Quarkslab

기여자

이 연구에 기여한 분들께 큰 감사를 드립니다:

• Luigi Coniglio
• Jonathan Salwan