mrphrazer/msynth코드 난독화 해제 프레임워크로, 혼합 불리언-산술(MBA) 표현식을 단순화합니다
작성자: Tim Blazytko 및 Moritz Schloegel
msynth는 Mixed Boolean-Arithmetic (MBA) 표현식을 단순화하기 위한 코드 디오브푸스케이션 프레임워크입니다. 미리 계산된 단순화 오라클이 주어지면, 추상 구문 트리(AST)로 표현된 복잡한 표현식을 순회하며 다양한 대수적 및 의미론적 단순화 기법을 사용하여 하위 트리를 단순화하려고 시도합니다. 또는 확률적 프로그램 합성을 통해 표현식을 단순화하려고 시도합니다.
msynth는 Miasm을 기반으로 구축되었으며 다음 논문에서 영감을 받았습니다.
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" - Robin David, Luigi Coniglio, Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" - Tim Blazytko, Moritz Contag, Cornelius Aschermann, Thorsten Holz (USENIX Security 2017),
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" - Grégoire Menguy, Sébastien Bardin, Richard Bonichon, Cauim de Souza de Lima (CCS 2021),
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" - Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin, Jean-Yves Marion (CCS 2025),
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" - Benjamin Reichenwallner, Peter Meerwald-Stadler (CheckMATE 2022),
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" - Benjamin Reichenwallner, Peter Meerwald-Stadler (WORMA 2023).
Miasm의 심볼릭 실행 엔진과 함께 사용하여 난독화된 코드의 복잡한 표현식을 단순화하거나, MBA 단순화를 실험해 볼 수 있는 독립 실행형 도구로 사용할 수 있습니다.
original: {((((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & (RDX[0:32] ^ 0xFFFFFFFF)) + -(((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) | (((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32])) + ({RDI[0:32] & ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32] 0 32, 0x0 32 64} * 0x2 + {((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & RSI[0:32]) + (((RDI + {(RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32] 0 32, 0x0 32 64} + 0x1)[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + (RDI[0:32] ^ ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32]) + ((RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32]) + (RDI + RDX + 0x1)[0:32] 0 32, 0x0 32 64})[0:32]) * 0x2 0 32, 0x0 32 64}
simplified: {(-RDX[0:32] + ((RDI[0:32] + RDX[0:32] + RSI[0:32]) << 0x1)) * 0x2 0 32, 0x0 32 64}
msynth를 설치하려면 다음 단계를 따르세요:
git clone https://github.com/mrphrazer/msynth.git
cd msynth
# optionally: use a virtual environment
python -m venv msynth-env
source msynth-env/bin/activate
# install dependencies
pip install -r requirements.txt
# install msynth
pip install .
# unzip database
unzip -d database -q database/3_variables_constants_7_nodes.txt.zip
기존 환경을 업데이트할 때는 고정된 Miasm 커밋을 반영하기 위해 의존성을 재설치하세요. 서로 다른 Miasm 커밋이 동일한 패키지 버전을 보고할 수 있으므로, 일반 설치로는 이전 커밋이 그대로 남을 수 있습니다:
python -m pip install --force-reinstall -r requirements.txt
오라클을 생성하려면 다수의 표현식을 포함하는 단순화 조회 테이블(또는 데이터베이스)이 필요합니다. 우리는 다음과 같은 사양에 따라 8, 16, 32, 64비트 크기의 표현식을 열거적 탐색을 통해 사전 계산했습니다:
최대 5개의 변수 p0, p1, p2, p3, p4
변수를 (필요한 경우) 32, 16, 8비트로 축소하기 위한 절단(truncation) 연산자,
비트 벡터 연산인 덧셈, 뺄셈, 곱셈, 부정(단항 마이너스), 비트 AND/OR/XOR/NOT, 논리 왼쪽 시프트,
그리고 일부 테이블의 경우 상수 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000, 0xffff_ffff_ffff_ffff.
database에 포함된 예제 데이터베이스는 세 개의 변수와 상수 0x0, 0x1, 0x2를 사용하여 최대 7개 노드로 생성된 모든 1,293,020개의 조합을 포함합니다 (예: ((p0 + p1) * (p2 ^ 0x2)) 또는 ((p0 - p2) << (p1 + p2))). 더 큰 사전 계산된 데이터베이스는 여기에서 찾을 수 있습니다 (압축 해제 시 약 31GB). 표현식을 사전 계산하는 코드는 이 저장소에 포함되어 있지 않습니다. 향후 공개할 계획입니다.
사전 계산된 조회 테이블의 대안으로, msynth는 확률적 프로그램 합성을 통한 표현식 단순화를 지원합니다. 주어진 복잡한 산술 표현식에 대해, msynth는 동일한 입출력 동작을 공유하는 더 짧은 표현식을 학습할 수 있습니다. 현재는 독립 실행형 컴포넌트로 구현되어 있습니다. 그러나 향후 두 단순화 접근 방식을 결합할 계획입니다.
합성 경로는 기본적으로 위에 링크된 CCS 2025 논문에 따라 Search Modulo Inference Rules (Smir)를 사용합니다. Smir는 임의 상수, 마스크, 상수 시프트 및 회전, 아핀 표현식, 유계 다항식 표현식과 같이 합성하기 어려운 패턴에 대해 인접 후보를 도출하여 로컬 검색을 보강합니다.
먼저, 사전 계산된 단순화 데이터베이스를 입력으로 사용하고 포함된 표현식들을 동등 클래스로 클러스터링하는 단순화 오라클을 생성해 보겠습니다.
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.pickle
msynth - INFO: Computing oracle for 30 variables and 50 samples.
Using library at 'database/3_variables_constants_7_nodes.txt'
msynth - INFO: Writing oracle to oracle.pickle
msynth - INFO: Done in 632.84 seconds
사전 계산된 단순화 데이터베이스의 크기에 따라, 컴퓨터 성능에 따라 몇 분에서 몇 시간이 걸릴 수 있습니다. 또는 미리 계산된 oracle.pickle을 사용할 수 있습니다.
선택적으로 --sqlite 플래그를 사용하여 SQLite 형식으로 오라클을 생성할 수 있으며, 이는 지연 로딩과 훨씬 빠른 시작 시간을 가능하게 합니다:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
이후 직렬화된 오라클을 사용하여 복잡한 표현식을 단순화할 수 있습니다:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)
또는 프로그램 합성을 통해 복잡한 표현식을 단순화하고 동일한 입출력 동작을 가진 표현식을 학습할 수 있습니다:
from msynth import Synthesizer
# initialize synthesizer
synthesizer = Synthesizer()
# simplify via program synthesis
simplified = synthesizer.simplify(expression)
표현식 단순화를 Miasm의 심볼릭 실행 엔진과 결합하는 것도 가능합니다:
$ python scripts/symbolic_simplification.py samples/mba_challenge 0x1290 oracle.pickle
[snip]
before: {({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32] 0 32, 0x0 32 64}
simplified: {RDI[0:32] + RSI[0:32] 0 32, 0x0 32 64}
[snip]
더 많은 사용 예시는 scripts 디렉토리에서 찾을 수 있습니다.
더 많은 정보를 원하시면 Tim Blazytko (@mr_phrazer) 또는 Moritz Schloegel (@m_u00d8)에게 연락하세요.