binsec/xyntiaXyntia, the black-box deobfuscator
Debian系システムでは、次のコマンドを実行してください：
sudo apt install libgmp3-dev gcc-multilib gdb python3 python3-pip python3-venv openjdk-17-jdk libgmp-dev pkg-config opam
また、Ghidra をインストールし、Ghidraのインストールディレクトリを指定してGHIDRA環境変数を設定する必要があります。
export GHIDRA=<ghidra-directory>
xyntiaをインストールする最も簡単な方法は、opamスイッチを作成することです。これにより、xyntiaとその依存関係が自動的にインストールされます：
$ cd <xyntia-directory>
$ opam switch create . 4.14.1 -y # or any version >= 4.14.1
$ eval $(opam env)
xyntiaのヘルプは xyntia -help で確認できます。以下では、xyntiaの2つの使用方法について説明します。
サンプリングファイルから関数を合成するには、次のコマンドを実行します：
$ xyntia [-ops <grammar>] [-time <time>] [-heur <heur>] <file.json>
ここで、grammar は探索空間を定義するために使用される文法の略称（下記参照）、heur は使用される探索ヒューリスティックの略称（下記参照）、time は合成の時間予算（秒）、file はサンプリングファイルのパスです。
サンプリングファイルは、Syntiaのランダムサンプリングモジュールによって生成される形式である必要があります。examples/samples/example.json ファイルは、サンプリングファイルの例です。
xyntiaにバイナリの出力をサンプリングさせ、それらを合成するには、次のコマンドを使用します：
$ xyntia [-ops <grammar>] [-time <time>] [-heur <heur>] -bin <binary-file> -config <config-file>
ここで、binary-file は解析対象のバイナリへのパスであり、config-file はどの出力をサンプリングし、どのようにサンプリングするかを指定するスクリプトファイルです。
config-file で使用されるスクリプト言語は、Binsecスクリプト言語 の拡張です。次の新しい宣言と命令が追加されています：
sample N [ reg_1, ..., reg_n ]：各出力に対してN個のサンプルを生成することを指定します。対象のレジスタ出力のリストを設定できます。この場合、これらの出力のみがサンプリングされ、それ以外の場合は検出されたすべての出力がサンプリングされます。set domain VAR [MIN, MAX]：VAR入力のサンプリングドメインを指定します。VARはレジスタまたは任意のDBA変数にできますが、メモリセルにはできません。メモリセルのドメインを指定するには、この例 を参照してください。prune constant outputs：サンプリングされた出力のセットから、すべての定数出力（つまり、入力変数を含まない出力）を削除します。set optimal sampling：Xyntiaの論文で説明されているサンプリング戦略を使用します。例えば、add関数の eax 出力を合成するには、次のコマンドを実行します：
$ cd examples/bin && make && cd -
$ xyntia -bin examples/bin/add -config examples/bin/add.ini
この場合、add.ini ファイルは次のようになります：
要約： 対象の式に定数値が含まれると予想される場合。
詳細： プログラム合成には根本的な限界があります。すなわち、任意の定数値と大きな式の処理です。これらの限界を回避するために、Xyntiaは探索をより適切に導き、候補解を（任意の定数値を含む可能性のある）対象の式へ一段階で高める 推論規則 を備えています。 したがって、対象の式に定数値が含まれる可能性が高い場合は、推論規則を使用してください。
より深く理解するには、私たちの論文 [3] をお読みください：
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, ACM Conference on Computer and Communications Security 2025
推論規則を使用するには、オプション -infrules <val> を設定する必要があります。ここで、<val> は次のいずれかです：
r1, r2, ..., rk）。各規則は、以下で説明する特定のケースを処理することを目的としています。他のシンセサイザーとXyntiaを簡単に比較したり、それらを難読化解除タスクに適用したりするために、標準のSyGUS形式で合成問題を抽出する方法を提供しています。これを行うには、-sygus オプションを使用するだけです。
例えば、バイナリコードからSyGUS問題を抽出するには、次のコマンドを実行します：
$ xyntia -bin <binary-file> -config <config-file> -sygus
[1] で紹介されている実験を再現するためのすべてのデータセットとスクリプトを提供しています。特に、Syntia の論文 [2] のB1データセット（共有してくださった Tim Blazytko に感謝します）、私たちのB2データセット、およびブラックボックス難読化解除対策の評価に使用されたデータセットが含まれています。
インストールを容易にするために、Pythonの依存関係を簡単にインストールできる requirements.txt も提供しています。
Python環境を作成して有効化するには、次のコマンドを実行します（任意）：
$ python3 -m venv <name-virtualenv> # create a virtual environment for python3
$ source <name-virtualenv>/bin/activate # active the virtual environment
次に、依存関係をインストールします：
$ pip install -r requirements.txt
[1] で使用されたデータセットは、./datasets ディレクトリにあります。
指定したタイムアウト（例：1秒）でデータセット（例：B2）に対してXyntiaを実行するには、次のコマンドを実行します：
$ python3 ./scripts/bench/bench.py --dataset datasets/b2 --out results --parallel -- xyntia -check -time 1
オプションとその意味は、--help オプションで確認できます。
また、GhidraまたはGDBでコード実行をトレースし、実行された各コードブロックを抽出してサンプリングおよび合成する ./scripts/utils/all_from_trace.sh も提供しています。
マニュアルは ./scripts/utils/all_from_trace.sh --help で確認でき、次のように実行できます：
$ XYNTIA="xyntia <options>" # the xyntia command to use
$ ./scripts/utils/all_from_trace.sh --outdir <resdir> --all -- binary arg1 arg2 ...
以下に例を示します：
$ cd examples/bin && make && cd -
$ ./scripts/utils/all_from_trace.sh --outdir <resdir> --all -- ./examples/bin/add
[1] Menguy, G., Bardin, S., Bonichon, R., & Lima, C. D. S. (2021, November). Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security.
[2] Blazytko, T., Contag, M., Aschermann, C., & Holz, T. (2017). Syntia: Synthesizing the semantics of obfuscated code. In 26th USENIX Security Symposium (USENIX Security 17).
[3] Attias, V., Bellec, N., Menguy, G., Bardin, S., Marion, J. (2025, October). Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security.
$ cat examples/bin/add.ini
starting from <add>
set sample output stdout
explore all
hook <add:last> with
sample 100 eax
halt
end
starting from 命令はリバースウィンドウの開始を指定します。hook 命令はリバースウィンドウの終了を指定します（注：<add:last> は add 関数の最後のバイトを表します。add の最後の命令が ret であり、そのオペコードがわずか1バイト長であるため、これが機能します）。
スクリプトの他の例は、sampler/examples ディレクトリにあります。
シンボリック式を直接サンプリングすることも可能です。例は sampler/examples/expr.ini にあります。サンプリングするには、次のコマンドを使用します：
# The <() is here to replace the binary path. Indeed, in this case we do not need any binary (only an empty file)
xyntia -bin <() -config sampler/examples/expr.ini
| 文法 | 略称 |
|---|
| 混合ブール演算（MBA） | mba |
| MBA+Division | expr |
| MBA+Division+Mod+Shift | full |
| MBA+Shift | mba_shift |
| MBA+If then else | mba_ite |
| ヒューリスティック | 略称 |
|---|
| 反復局所探索 | ils |
| 山登り法 | hc |
| ランダムウォーク | rw |
| 焼きなまし法 | sa |
| メトロポリス・ヘイスティングス | mh |
| 推論規則 | 式の種類 |
|---|
| $\diamond \in { +, *, \oplus, >>u, <<, ror }$ | $e \diamond c$ |
| maskotf | $(e \land c_1) \lor c_2$ |
| affine | $(c_1 * e) + c_2$ |
| poly2 | $(c_1 * e^2) + (c_2 * e) + c_3$ |
ここで、
eは文法からの式であり、c, c1, c2, c3は任意の定数値です。
mba（+, maskotf, <<, *, ^ と同じ）と all（+, maskotf, <<, >>u, *, ^, ror, poly2, affine と同じ）のいずれかのキーワード。Snapchatアプリの難読化された式の例を提供しています。これにXyntiaを適用するには、次のコマンドを実行します：
$ xyntia -bin samplers/examples/snapchat -config samplers/examples/snapchat.ini -infrules all