denuvosoftwaresolutions/gambaVereinfachung allgemeiner gemischter boolesch-arithmetischer Ausdrücke: GAMBA
GAMBA ist ein Werkzeug zur Vereinfachung gemischter boolesch-arithmetischer Ausdrücke (MBAs). GAMBA ist die Kurzform für „General Advanced Mixed Boolean Arithmetic Simplifier“. Es verwendet den linear-algebraischen Simplifier SiMBA, um lineare Teilausdrücke eines potenziell nichtlinearen Eingabe-MBA iterativ zu vereinfachen. Insgesamt sind seine Kernbestandteile die folgenden:
GAMBA basiert auf dem folgenden Paper; siehe auch die für die Präsentation verwendeten Folien:
@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}
}
Es werden zwei Hauptprogramme bereitgestellt:
simplify_general.py zur Vereinfachung allgemeiner MBAssimplify.py zur Vereinfachung linearer MBAsDarüber hinaus wird ein Testskript bereitgestellt, um die in der Arbeit angegebenen Ergebnisse zu reproduzieren.
Um einen einzelnen Ausdruck expr zu vereinfachen, verwenden Sie
python3 src/simplify_general.py "expr"
Alternativ können mehrere Ausdrücke gleichzeitig vereinfacht werden, z. B.:
python3 src/simplify_general.py "x+x" "y*y" "a&a"
Tatsächlich wird jedes Kommandozeilenargument, das keine Option ist, als ein zu vereinfachender Ausdruck betrachtet. Beachten Sie, dass das Weglassen der Anführungszeichen zu unerwünschtem Verhalten führen kann. Die Vereinfachungsergebnisse werden wie im Folgenden gezeigt auf der Kommandozeile ausgegeben:
*** Expression x+x
*** ... simplified to 2*x
*** Expression y*y
*** ... simplified to y**2
*** Expression a
*** ... simplified to a
Wenn die Option -z verwendet wird, werden die Vereinfachungsergebnisse abschließend mithilfe von Z3 daraufhin überprüft, ob sie semantisch äquivalent zu den ursprünglichen Ausdrücken sind. Dies hat keine Auswirkung auf die Kommandozeilenausgabe, solange der Algorithmus korrekt arbeitet:
python3 src/simplify_general.py "x+x" -z
Falls der Algorithmus ein falsches Ergebnis ausgeben würde, würde der folgende Fehler ausgelöst:
*** Expression x+x
Error in simplification! Simplified expression is not equivalent to original one!
Zusätzlich kann eine numerische Validierung der Ergebnisse mit allen möglichen Eingaben bis zu einer bestimmten Bitanzahl durchgeführt werden. Dies wird mit der Option -v aktiviert, gefolgt von einer maximalen Bitanzahl der verwendeten Eingaben:
python3 src/simplify_general.py "x+x" -v 3
Auch im Falle eines falschen Ergebnisses könnte die Ausgabe wie folgt aussehen:
*** Expression x+x
*** ... verify via evaluation ... [ ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2
Die in den GAMBA-Ausgabeausdrücken auftretenden Konstanten können offensichtlich von der Anzahl der Bits abhängen, die für Konstanten sowie Variablen verwendet werden. Diese Anzahl beträgt standardmäßig $64$ und kann mit der Option -b festgelegt werden:
python3 src/simplify_general.py "-x" -b 32
Standardmäßig werden die in der Ausgabe auftretenden Konstanten in der Darstellung angegeben, die so nahe wie möglich an Null liegt. Das heißt, im obigen Fall würde die Zahl -1 erhalten bleiben:
*** Expression -x
*** ... simplified to -x
Dieses Verhalten kann geändert werden: Mit der Option -m wird eine Modulo-Reduktion von Konstanten aktiviert:
python3 src/simplify_general.py "-x" -b 32 -m
Dann liegen die Konstanten für eine Anzahl $b$ von Bits immer zwischen $0$ und $2^b-1$. Daher würde der obige Aufruf die folgende Ausgabe ergeben:
*** Expression -x
*** ... simplified to 4294967295*x
Die Datei src/simplify.py ist dazu gedacht, von src/simplify_general.py genutzt zu werden, kann aber auch isoliert ausgeführt werden. Verwenden Sie die Kommandozeilenoption -h, um die verfügbaren Einstellungen zu sehen.
Die Datei experiments/tests.py kann verwendet werden, um die in der Arbeit angegebenen Experimente zu reproduzieren. Standardmäßig führt es GAMBA auf 6 Datensätzen aus:
python3 experiments/tests.py
Alternativ kann es angewiesen werden, stattdessen SiMBA auszuführen, und zwar mit der Option --linear oder -l. In diesem Fall wird SiMBA nur auf MBAs mit linearen Grundwahrheiten ausgeführt:
python3 experiments/tests.py --linear
Numerische Prüfungen oder Prüfungen mit Z3 können über die Optionen --check (-c) bzw. --z3 (-z) aktiviert werden.
Die Ausdrücke werden je nach Erfolg der Vereinfachung oder Verifikation kategorisiert:
Datensätze zur Verwendung mit experiments/tests.py finden Sie im Verzeichnis experiments/datasets/.
-d 0; von https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (mit einigen Korrekturen)-d 1; von https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 lineare Ausdrücke)-d 2; von https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt und https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt (je 500 Ausdrücke; mit einigen Korrekturen für nichtpolynomiale Ausdrücke)-d 3; von MBA-Flatten, dataset/dataset_syntia.txt-d 4; von MBA-Flatten, die ersten 1000 Ausdrücke aus dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt-d 5; von https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.jsonZusätzlich werden die folgenden Bonus-Datensätze im Verzeichnis experiments/datasets/bonus/ bereitgestellt (nicht in der Veröffentlichung abgedeckt):
-d 6; von https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBAs, die von der LOKI-Arbeit für einfache Grundwahrheiten-Ausdrücke ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$) bis zu einer Tiefe von 5 erzeugt wurdenDie Anzahl der Variablen ist theoretisch unbegrenzt, aber natürlich steigt die Laufzeit mit der Variablenanzahl. Es gibt keine strenge Einschränkung bei der Schreibweise von Variablen. Sie müssen mit einem Buchstaben beginnen und können Buchstaben, Zahlen und Unterstriche enthalten. Z. B. wären die folgenden Variablennamen alle in Ordnung:
Die folgenden Operatoren werden unterstützt, geordnet nach ihrer Priorität in Python:
In den Eingabeausdrücken kann Leerraum verwendet werden. Z. B. kann der Ausdruck "x+y" alternativ als "x + y" geschrieben werden.
Bitte beachten Sie die Priorität der Operatoren und verwenden Sie bei Bedarf Klammern! Z. B. sind die Ausdrücke $1 + (x|y)$ und $1 + x|y$ nicht äquivalent, da $+$ eine höhere Priorität als $|$ hat. Beachten Sie, dass Letzterer nicht einmal ein lineares MBA ist.
Der SMT-Löser Z3 wird von simplify_general.py und simplify.py benötigt, wenn die optionale Verifikation vereinfachter Ausdrücke verwendet wird. Wenn diese Option nicht verwendet wird, wird kein Fehler ausgelöst, selbst wenn Z3 nicht installiert ist.
Z3 installieren:
sudo apt-get install python3-z3Das wissenschaftliche Rechenpaket NumPy wird aus Bequemlichkeit benötigt, ist aber für den Betrieb nicht wirklich wesentlich. Hinweis: Für numpy.quantile wird mindestens Version 1.15.0 benötigt.
NumPy installieren:
sudo apt-get install python3-numpyCopyright (c) 2023 Denuvo GmbH, veröffentlicht unter GPLv3.