mrphrazer/msynthMixed Boolean-Arithmetic (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 ビットにダウンキャストする切り捨て演算子
ビットベクトル演算: 加算、減算、乗算、否定 (単項マイナス)、ビット単位の and/or/xor/not、および論理左シフト
また一部のテーブルでは、定数 0x0、0x1、0x2、0x80、0xff、0x800、0xffff、0x8000_0000、0xffff_ffff、0x8000_0000_0000_0000、0xffff_ffff_ffff_ffff
database に含まれるサンプルデータベースには、3 つの変数と定数 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) までお問い合わせください。