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

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

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:

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

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

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:

Dies würde den folgenden Fehler auslösen:

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:

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:

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

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:

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:

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

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:

Die folgende Ausgabe würde dann angezeigt:

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:

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

Reproduzierbarkeit

Zur Reproduktion eines Teils der im Paper beschriebenen Experimente kann eine der im Verzeichnis data/ enthaltenen Datensatzdateien verwendet werden. Für jede der folgenden Funktionen $e_1,\ldots, e_5$ werden Datensätze mit $1,000$ äquivalenten linearen MBAs mit $2$, $3$ oder $4$ Variablen bereitgestellt:

• $e_1(x,y) = x+y$
• $e_2 = 49,374$
• $e_3(x) = 3,735,936,685, x + 49,374$
• $e_4(x,y) = 3,735,936,685, (x\mathbin{^\wedge}y) + 49,374$
• $e_5(x) = 3,735,936,685\cdot \mathord{\sim} x$

Für $e_1$ werden zusätzliche Datensätze für $5$ bis $7$ Variablen bereitgestellt. Diese MBAs wurden mit einem Algorithmus erzeugt, der auf der von Zhou et al. im Jahr 2007 beschriebenen Methode basiert und im Paper beschrieben ist.

Bitte beachten Sie, dass diese Datensätze für $b=64$ Bits erzeugt wurden. Für andere Bitanzahlen kann ihre Äquivalenz zu den $e_i$ nicht garantiert werden.

Für die Reproduktion weiterer Experimente verweisen wir auf die Datensätze des MBA-Solver-Repositorys bzw. des NeuReduce-Repositorys.

Linearitätsprüfung

Die Datei check_linear_mba.py wird vom Vereinfacher verwendet, bietet aber auch eine eigene Schnittstelle, z. B.:

Sie prüft alle Ausdrücke, die über Befehlszeilenargumente übergeben werden. In diesem Fall würde das die folgende Ausgabe ergeben:

Format von MBAs

Die Anzahl der Variablen ist theoretisch unbegrenzt, aber natürlich erhöht sich die Laufzeit mit der Anzahl der Variablen. Es gibt keine strenge Einschränkung für die Notation 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 zulässig:

• $a$, $b$, $c$, ..., $x$, $y$, $z$, ...
• $v0$, $v1$, $v2$, ...
• $v_0$, $v_1$, $v_2$, ...
• $X0$, $X1$, $X2$, ...
• $var0$, $var1$, $var2$, ...
• $var1a$, $var1b$, $var1c$, ...
• ...

Die folgenden Operatoren werden unterstützt, geordnet nach ihrer Priorität in Python:

• $\mathord{\sim}$, $-$: bitweise Negation und unäres Minus
• $*$: Produkt
• $+$, $-$: Summe und Differenz
• &: Konjunktion
• $\mathbin{^\wedge}$: exklusive Disjunktion
• $|$: inklusive Disjunktion

Leerzeichen können in den Eingabeausdrücken 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 linearer MBA ist.

Abhängigkeiten

Der SMT-Löser Z3 wird benötigt

• von simplify_dataset.py, wo vereinfachte Ausdrücke als äquivalent zu entsprechenden einfachen Ausdrücken verifiziert werden, und
• von simplify.py, 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.

Installieren von Z3:

• aus dem GitHub-Repository: https://github.com/Z3Prover/z3, oder
• unter Debian: sudo apt-get install python3-z3

Lizenz

Copyright (c) 2022 Denuvo GmbH, veröffentlicht unter GPLv3.

Kontakt

• Benjamin Reichenwallner: benjamin(dot)reichenwallner(at)denuvo(dot)com
• Peter Meerwald-Stadler: peter(dot)meerwald(at)denuvo(dot)com