SiMBAは、線形混合ブール算術式（MBA）の簡約のためのツールです。MBA-BlastやMBA-Solverと同様に、線形MBAがゼロと一の集合上の値によって完全に決定されるという考えに基づく完全に代数的なアプローチを使用していますが、そのためには1ビット空間への変換が不要であるという新しい洞察を活用しています。
これは以下の論文に基づいています：
@inproceedings{simba2022,
author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
title = {Efficient deobfuscation of linear mixed Boolean-arithmetic expressions},
year = {2022},
month = nov,
address = {Los Angeles, CA, USA},
date = {November 7 - 11, 2022},
booktitle = {Proceedings of the CheckMATE 2022 workshop, co-located with the ACM Conference on Computer and Communication Security, CCS'22},
pages = {19--28},
doi = {10.1145/3560831.3564256},
publisher = {ACM},
howpublished = {\url{https://arxiv.org/abs/2209.06335}}
}
プレゼンテーションのスライドとビデオ録画はこちらからご覧いただけます。また、ACMからも入手できます。
2つの主要なプログラム（Python 3）が提供されています：
simplify.pysimplify_dataset.pyさらに、check_linear_mba.py プログラムを使用して、式が線形MBAを表すかどうかを確認できます。
単一の式 expr を簡約するには、次を使用します。
python3 src/simplify.py "expr"
あるいは、複数の式を一度に簡約することもできます。例：
python3 src/simplify.py "x+x" "a&a"
実際、オプションではない各コマンドライン引数は、簡約対象の式と見なされます。引用符を省略すると、意図しない動作を引き起こす可能性があることに注意してください。簡約結果は、次のようにコマンドラインに出力されます：
*** Expression x+x
*** ... simplified to 2*x
*** Expression a
*** ... simplified to a
デフォルトでは、入力式が線形MBAであるかどうかのチェックは実行されません。このチェックは、オプション -l を使用して任意に有効にできます：
python3 src/simplify.py "x*x" -l
$x*x$ は線形MBAではないため、この場合には次の出力が表示されます：
*** Expression x*x
Error: Input expression may be no linear MBA: x*x
オプション -z を使用すると、簡約結果が Z3 を使用して元の式と等しいかどうか最終的に検証されます。アルゴリズムが正しく動作し、入力式が線形MBAである限り、コマンドライン出力には影響しません：
python3 src/simplify.py "x*x" -z
これにより、次のエラーが発生します：
*** Expression x*x
Error in simplification! Simplified expression is not equivalent to original one!
SiMBAの出力式に現れる定数は常に非負であるため、それらは定数および変数に使用されるビット数に依存する可能性があります。この数はデフォルトで $64$ であり、オプション -b を使用して設定できます：
python3 src/simplify.py "-x" -b 32
$b$ ビットの場合、出力に現れる定数は常に $0$ から $2^b-1$ の範囲にあります。したがって、上記の呼び出しでは次の出力が得られます：
*** Expression -x
*** ... simplified to 4294967295*x
パス path_to_file のファイルに格納された式を簡約するには、次を使用します：
python3 src/simplify_dataset.py -f path_to_file
つまり、ファイルはオプション -f を使用して指定する必要があります。ファイルの各行には、複雑な式とそれと等価なより単純な式をカンマで区切って含める必要があります。例：
(x&y)+(x|y), x+y (x|y)-(~x&y)-(x&~y), x&y -(a|~b)+(~b)+(a&~b)+b, a^b 2*(s&~t)+2*(s^t)-(s|t)+2*~(s^t)-~t-~(s&t), s
各行について、複雑な式と単純な式の両方が簡約され、最終的に比較されます。後者（単純な式）を簡約する理由は、検証結果を空白、因子や加数の順序などに依存しないようにするためです。
simplify.py と同様に、線形性チェックと正しい簡約のチェックは、それぞれオプション -l と -z を使用して有効にでき、ビット数はオプション -b を使用して指定できます。指定されたファイルに含まれる式のうち、特定の最大数に対してのみSiMBAを実行したい場合は、この最大数をオプション -r で指定できます：
python3 src/simplify_dataset.py -f some_file.txt -r 2
some_file.txt に上記の式が含まれている場合、最初の2つのみが簡約されます：
Simplify expressions from data/some_file.txt ...
* total count: 2
* verified: 2
* equal: 2
* average duration: 0.00014788552653044462
いずれの場合も、出力は次の情報を提供します：
Z3を使用した正しい簡約の任意の検証は実行時間に加算されることに注意してください。一方、複雑な式とより単純な式のペアの簡約結果の比較は実行時間に加算されません。
デフォルトでは、簡約結果は出力されず、これらの統計のみが表示されます。前者に関する情報が必要な場合は、オプション -v を使用できます：
python3 src/simplify_dataset.py -f some_file.txt -v
すると、次の出力が表示されます：
Simplify expressions from data/some_file.txt ...
*** 1 groundtruth x+y, simplified x+y => equal: True, verified: True
*** 2 groundtruth x&y, simplified x&y => equal: True, verified: True
*** 3 groundtruth a^b, simplified a^b => equal: True, verified: True
*** 4 groundtruth s, simplified s => equal: True, verified: True
* total count: 4
* verified: 4
* equal: 4
* average duration: 0.00016793253598734736
もう1つのオプション -e は、$b$ をビット数として、$1$ から $2^b-1$ の範囲のランダムな整数 $a,b$ によるアフィン関数 $f(x) = ax+b$ ですべての式の出力をエンコードする機能を提供します：
python3 src/simplify_dataset.py -f some_file.txt -v -e
もちろん、同じ関数が同じ行の式のペアに適用されます。これにより、次のような出力が得られます：
Simplify expressions from data/some_file.txt ...
*** 1 groundtruth 10623056950310032687+5038261596809828791*x+5038261596809828791*y, simplified 10623056950310032687+5038261596809828791*x+5038261596809828791*y => equal: True, verified: True
*** 2 groundtruth 15181401701264988765+3962868592131193124*(x&y), simplified 15181401701264988765+3962868592131193124*(x&y) => equal: True, verified: True
*** 3 groundtruth 6812440940417974076+11894131080657788315*(a^b), simplified 6812440940417974076+11894131080657788315*(a^b) => equal: True, verified: True
*** 4 groundtruth 4558303267887122851+10271005790757592209*s, simplified 4558303267887122851+10271005790757592209*s => equal: True, verified: True
* total count: 4
* verified: 4
* equal: 4
* average duration: 0.00019435951253399253
論文に記載された実験の一部を再現するには、data/ ディレクトリに含まれる任意のデータセットファイルを使用できます。次の各関数 $e_1,\ldots, e_5$ について、$2$、$3$、または $4$ 変数を使用した $1,000$ 個の等価な線形MBAのデータセットが提供されています：
$e_1$ については、$5$ から $7$ 変数の追加データセットも提供されています。これらのMBAは、2007年にZhouらによって記述され、論文でも説明されている方法に基づくアルゴリズムを使用して生成されています。
これらのデータセットは $b=64$ ビット用に生成されていることに注意してください。異なるビット数の場合、$e_i$ との等価性は保証されません。
さらなる実験の再現については、それぞれ MBA-Solverリポジトリ と NeuReduceリポジトリ が提供するデータセットを参照してください。
check_linear_mba.py ファイルは簡約器によって使用されますが、独自のインターフェースも提供します。例：
python3 src/check_linear_mba.py "x+x" "x*x"
コマンドライン引数で渡されたすべての式をチェックします。この場合、次の出力が得られます：
*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid
変数の数は理論上無制限ですが、もちろん実行時間は変数の数に応じて増加します。変数の表記に関する厳しい制限はありません。変数は文字で始まる必要があり、文字、数字、アンダースコアを含めることができます。たとえば、次の変数名はすべて有効です：
次の演算子がサポートされており、Pythonでの優先順位の順に並んでいます：
入力式には空白を使用できます。たとえば、式 "x+y" は "x + y" と書くこともできます。
演算子の優先順位を尊重し、必要に応じて括弧を使用してください！ たとえば、$+$ は $|$ よりも優先順位が高いため、$1 + (x|y)$ と $1 + x|y$ は等価ではありません。後者は線形MBAですらないことに注意してください。
SMTソルバー Z3 が必要です
simplify_dataset.py では、簡約された式が対応する単純な式と等価であることを検証するために必要です。simplify.py では、簡約式の任意検証を使用する場合に必要です。このオプションを使用しない場合、Z3がインストールされていなくてもエラーは発生しません。Z3のインストール：
sudo apt-get install python3-z3Copyright (c) 2022 Denuvo GmbH、GPLv3 の下で公開されています。