SiMBA

SiMBA ist ein Werkzeug zur Vereinfachung linearer gemischter Boolesch-arithmetischer Ausdrücke (MBAs). Wie MBA-Blast und MBA-Solver verwendet es einen vollständig algebraischen Ansatz, der auf der Idee basiert, dass ein linearer MBA durch seine Werte auf der Menge der Nullen und Einsen vollständig bestimmt ist, nutzt dabei aber die neuen Erkenntnisse, dass eine Transformation in den 1-Bit-Raum hierfür nicht notwendig ist.

Es basiert auf folgendem Paper:

@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}}
}

Die Folien und eine Videoaufzeichnung der Präsentation finden Sie hier. Ebenfalls verfügbar über ACM.

Inhalt

Es werden zwei Hauptprogramme (Python 3) bereitgestellt:

• simplify.py zur Vereinfachung einzelner linearer MBAs
• simplify_dataset.py zur Vereinfachung einer Menge von linearen MBAs, die in einer Datei enthalten sind, und deren Verifikation durch einen Vergleich mit entsprechenden einfacheren Ausdrücken, die ebenfalls in dieser Datei enthalten sind

Zusätzlich kann das Programm check_linear_mba.py verwendet werden, um zu prüfen, ob Ausdrücke lineare MBAs darstellen.

Verwendung

Vereinfachen einzelner Ausdrücke

Um einen einzelnen Ausdruck expr zu vereinfachen, verwenden Sie

python3 src/simplify.py "expr"

Alternativ können mehrere Ausdrücke auf einmal vereinfacht werden, z. B.:

python3 src/simplify.py "x+x" "a&a"

Tatsächlich wird jedes Befehlszeilenargument, das keine Option ist, als 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 in der Befehlszeile ausgegeben:

*** Expression x+x
*** ... simplified to 2*x
*** Expression a
*** ... simplified to a

Standardmäßig wird nicht geprüft, ob der Eingabeausdruck ein linearer MBA ist. Diese Prüfung kann optional über die Option -l aktiviert werden:

python3 src/simplify.py "x*x" -l

Da $x*x$ kein linearer MBA ist, würde in diesem Fall die folgende Ausgabe erscheinen:

*** Expression x*x
Error: Input expression may be no linear MBA: x*x

Wenn die Option -z verwendet wird, werden die Vereinfachungsergebnisse abschließend mit Z3 auf Gleichheit mit den ursprünglichen Ausdrücken überprüft. Dies hat keinen Einfluss auf die Befehlszeilenausgabe, solange der Algorithmus korrekt arbeitet und der Eingabeausdruck ein linearer MBA ist:

python3 src/simplify.py "x*x" -z

Dies würde den folgenden Fehler auslösen:

*** Expression x*x
Error in simplification! Simplified expression is not equivalent to original one!

Da die in SiMBAs Ausgabeausdrücken vorkommenden Konstanten immer nichtnegativ sind, können sie 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.py "-x" -b 32

Für eine Anzahl $b$ von Bits liegen die in der Ausgabe vorkommenden Konstanten immer zwischen $0$ und $2^b-1$. Daher würde der obige Aufruf die folgende Ausgabe ergeben:

*** Expression -x
*** ... simplified to 4294967295*x

Vereinfachen und Verifizieren von Ausdrücken aus einer Datei

Um in einer Datei mit dem Pfad path_to_file gespeicherte Ausdrücke zu vereinfachen, verwenden Sie

python3 src/simplify_dataset.py -f path_to_file

Das heißt, die Datei muss mit der Option -f angegeben werden. Jede Zeile der Datei muss einen komplexen Ausdruck sowie einen äquivalenten einfacheren Ausdruck enthalten, getrennt durch ein Komma, z. B.:

example-expressions.txt:

(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

Für jede Zeile werden sowohl der komplexe als auch der einfache Ausdruck vereinfacht und schließlich verglichen. Der Grund für die Vereinfachung des letzteren ist, die Verifikationsergebnisse unabhängig von Leerzeichen, der Reihenfolge von Faktoren oder Summanden usw. zu machen.

Wie bei simplify.py können eine Linearitätsprüfung sowie eine Prüfung auf korrekte Vereinfachung über die Optionen -l bzw. -z aktiviert werden, und die Anzahl der Bits kann mit der Option -b festgelegt werden. Wenn SiMBA nur auf eine bestimmte Höchstzahl von Ausdrücken in der angegebenen Datei angewendet werden soll, kann diese Höchstzahl über die Option -r festgelegt werden:

python3 src/simplify_dataset.py -f some_file.txt -r 2

Wenn some_file.txt die oben aufgeführten Ausdrücke enthalten würde, würden nur die ersten beiden davon vereinfacht:

Simplify expressions from data/some_file.txt ...
  * total count: 2
  * verified: 2
  * equal: 2
  * average duration: 0.00014788552653044462

In jedem Fall gibt die Ausgabe Auskunft über

• die Gesamtzahl der Ausdrücke in der Eingabe,
• die Anzahl der Ausdrücke, die nach der Vereinfachung mit Z3 als äquivalent zu dem entsprechenden einfacheren Ausdruck verifiziert werden konnten (sofern das Vereinfachungsergebnis nicht bereits exakt dieselbe Zeichenkettendarstellung hat),
• die Anzahl der Ausdrücke, die zu genau demselben Ausdruck wie der entsprechende einfache Ausdruck vereinfacht werden, und
• die durchschnittliche Laufzeit in Sekunden.

Bitte beachten Sie, dass eine optionale Verifikation einer korrekten Vereinfachung mit Z3 zur Laufzeit beiträgt, während dies für den Vergleich der Vereinfachungsergebnisse der Paare aus einem komplexen und einem einfacheren Ausdruck nicht der Fall ist.

Standardmäßig werden die Vereinfachungsergebnisse nicht ausgegeben, sondern nur diese Statistiken dargestellt. Wenn Informationen über ersteres gewünscht sind, kann die Option -v verwendet werden:

python3 src/simplify_dataset.py -f some_file.txt -v

Die folgende Ausgabe würde dann angezeigt:

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

Eine weitere Option -e bietet die Möglichkeit, die Ausgaben aller Ausdrücke durch affine Funktionen $f(x) = ax+b$ mit zufälligen ganzen Zahlen $a,b$ zwischen $1$ und $2^b-1$ zu kodieren, wobei $b$ die Anzahl der Bits ist:

python3 src/simplify_dataset.py -f some_file.txt -v -e

Natürlich wird dieselbe Funktion auf ein Ausdruckspaar in derselben Zeile angewendet. Dies würde eine Ausgabe ähnlich der folgenden ergeben:

Simplify expressions from data/some_file.txt ...