GAMBA は、混合ブール演算（MBA）式を簡略化するためのツールです。 GAMBA は General Advanced Mixed Boolean Arithmetic simplifier の略です。 線形代数に基づく簡略化器 SiMBA を使用して、非線形の入力 MBA に含まれる線形部分式を反復的に簡略化します。全体として、その中核となる要素は以下のとおりです。
GAMBA は次の 論文 に基づいています。発表で使用された スライド も参照してください。
@inproceedings{gamba2023,
author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
title = {Simplification of General Mixed Boolean-Arithmetic Expressions: {GAMBA}},
address = {Delft, The Netherlands},
year = {2023},
month = jul,
publisher = {IEEE},
pages = {427--438},
doi = {10.1109/EuroSPW59978.2023.00053},
howpublished = {https://arxiv.org/abs/2305.06763},
booktitle = {Proceedings of the 2nd Workshop on Robust Malware Analysis, WORMA'23,
co-located with the 8th IEEE European Symposium on Security and Privacy}
}
2つの主要なプログラムが提供されています:
simplify_general.py は、一般的な MBA の簡略化用simplify.py は、線形 MBA の簡略化用さらに、論文に記載された結果を再現するためのテストスクリプトも提供されています。
単一の式 expr を簡略化するには、次のコマンドを使用します:
python3 src/simplify_general.py "expr"
または、複数の式を一度に簡略化することもできます。例:
python3 src/simplify_general.py "x+x" "y*y" "a&a"
実際には、オプションではない各コマンドライン引数は簡略化する式と見なされます。引用符を省略すると、意図しない動作を引き起こす可能性があることに注意してください。簡略化結果は、次のようにコマンドラインに出力されます:
*** Expression x+x
*** ... simplified to 2*x
*** Expression y*y
*** ... simplified to y**2
*** Expression a
*** ... simplified to a
オプション -z を使用すると、簡略化結果が Z3 を使用して元の式と意味的に等価であることが最終的に検証されます。アルゴリズムが正しく動作する限り、コマンドライン出力には影響しません:
python3 src/simplify_general.py "x+x" -z
アルゴリズムが誤った結果を出力した場合は、次のエラーが発生します:
*** Expression x+x
Error in simplification! Simplified expression is not equivalent to original one!
さらに、特定のビット数までのすべての可能な入力を用いた結果の数値検証を実行できます。これは、オプション -v を使用し、その後に使用する入力の最大ビット数を指定することで有効になります:
python3 src/simplify_general.py "x+x" -v 3
誤った結果の場合も、出力は次のようになることがあります:
*** Expression x+x
*** ... verify via evaluation ... [ ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2
GAMBA の出力式に現れる定数は、当然ながら変数だけでなく定数に使用されるビット数にも依存します。この数はデフォルトで $64$ であり、オプション -b で設定できます:
python3 src/simplify_general.py "-x" -b 32
デフォルトでは、出力に現れる定数は、可能な限りゼロに近い表現で報告されます。つまり、上記の例では、-1 という数値のままになります:
*** Expression -x
*** ... simplified to -x
この動作は変更できます: オプション -m を使用すると、定数のモジュロ削減が有効になります:
python3 src/simplify_general.py "-x" -b 32 -m
この場合、ビット数 $b$ に対して、定数は常に $0$ 以上 $2^b-1$ 以下になります。したがって、上記の呼び出しは次の出力になります:
*** Expression -x
*** ... simplified to 4294967295*x
ファイル src/simplify.py は src/simplify_general.py によって利用されることを意図していますが、単独で実行することもできます。利用可能な設定を確認するには、コマンドラインオプション -h を使用してください。
ファイル experiments/tests.py を使用して、論文に記載された実験を再現できます。デフォルトでは、6つのデータセットに対して GAMBA を実行します:
python3 experiments/tests.py
または、オプション --linear または -l を使用して、代わりに SiMBA を実行するように指示することもできます。その場合、SiMBA は線形のグラウンドトゥルースを持つ MBA に対してのみ実行されます:
python3 experiments/tests.py --linear
数値チェックまたは Z3 を使用したチェックは、それぞれオプション --check (-c) または --z3 (-z) で有効にできます。
式は、簡略化または検証の成否に応じて分類されます:
experiments/tests.py で使用するデータセットは、ディレクトリ experiments/datasets/ にあります。
-d 0 を使用; https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv から（いくつかの修正を適用）-d 1 を使用; https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt から（1000個の線形式）-d 2 を使用; https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt および https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt から（それぞれ500個の式。非多項式の式にはいくつかの修正を適用）-d 3 を使用; MBA-Flatten の dataset/dataset_syntia.txt から-d 4 を使用; MBA-Flatten の dataset/pldi_dataset_linear_MBA.txt、dataset/pldi_dataset_poly_MBA.txt、dataset/pldi_dataset_nonpoly_MBA.txt の最初の1000式から-d 5 を使用; https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json からさらに、以下のボーナスデータセットがディレクトリ experiments/datasets/bonus/ に提供されています（出版物では取り上げられていません）:
-d 6 を使用; https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data から、LOKI 論文によって単純なグラウンドトゥルース式（$x+y$, $x-y$, $x\&y$, $x|y$, $x^y$）用に生成された25000個のMBA（深さ5まで）変数の数は理論上無制限ですが、もちろん実行時間は変数の数に応じて増加します。変数の表記に強い制限はありません。変数は文字で始まる必要があり、文字、数字、アンダースコアを含めることができます。例えば、次の変数名はすべて問題ありません:
次の演算子がサポートされており、Python での優先順位順に並んでいます:
入力式では空白を使用できます。例えば、式 "x+y" は "x + y" と書くこともできます。
演算子の優先順位を尊重し、必要に応じて括弧を使用してください！ 例えば、式 $1 + (x|y)$ と $1 + x|y$ は、$+$ が $|$ よりも優先順位が高いため、等価ではありません。後者は線形 MBA ですらないことに注意してください。
SMTソルバー Z3 は、簡略化された式のオプション検証を使用する場合に simplify_general.py と simplify.py によって必要とされます。このオプションを使用しない場合、Z3 がインストールされていなくてもエラーは発生しません。
Z3 のインストール:
sudo apt-get install python3-z3科学計算パッケージ NumPy は怠惰のため必要ですが、動作にはそれほど必須ではありません。 注: numpy.quantile には少なくともバージョン 1.15.0 が必要です。
NumPy のインストール:
sudo apt-get install python3-numpyCopyright (c) 2023 Denuvo GmbH、GPLv3 の下で公開されています。