GAMBA

GAMBA est un outil de simplification d'expressions mixtes booléennes-arithmétiques (MBA). GAMBA est l'acronyme de General Advanced Mixed Boolean Arithmetic simplifier. Il utilise le simplificateur algébrique linéaire SiMBA pour simplifier itérativement les sous-expressions linéaires d'une MBA d'entrée potentiellement non linéaire. Globalement, ses composants essentiels sont les suivants :

• Utilisation d'arbres de syntaxe abstraite (AST)
• Isolation des sous-expressions linéaires par application de transformations (triviales et plus sophistiquées)
• Refactorisation afin d'augmenter les chances de construire des sous-expressions linéaires pouvant être simplifiées
• Simplification des sous-expressions linéaires à l'aide de SiMBA
• Logique de substitution pour se débarrasser temporairement de constantes non triviales et d'opérations arithmétiques dans les opérations bit à bit

GAMBA est basé sur l'article suivant, voir aussi les diapositives utilisées pour la présentation :

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

Contenu

Deux programmes principaux sont fournis :

• simplify_general.py pour la simplification des MBA générales
• simplify.py pour la simplification des MBA linéaires

De plus, un script de test est fourni pour reproduire les résultats présentés dans l'article.

Utilisation

Simplification d'expressions générales individuelles

Afin de simplifier une expression unique expr, utilisez :

python3 src/simplify_general.py "expr"

Alternativement, plusieurs expressions peuvent être simplifiées en même temps, par exemple :

python3 src/simplify_general.py "x+x" "y*y" "a&a"

En fait, chaque argument de la ligne de commande qui n'est pas une option est considéré comme une expression à simplifier. Notez que l'omission des guillemets peut conduire à un comportement indésirable. Les résultats de simplification sont affichés sur la ligne de commande comme indiqué ci-dessous :

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

Si l'option -z est utilisée, les résultats de simplification sont ensuite vérifiés comme sémantiquement équivalents aux expressions d'origine à l'aide de Z3. Cela n'affecte pas la sortie de la ligne de commande tant que l'algorithme fonctionne correctement :

python3 src/simplify_general.py "x+x" -z

Si l'algorithme produisait un résultat incorrect, l'erreur suivante serait déclenchée :

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

De plus, une validation numérique des résultats avec toutes les entrées possibles jusqu'à un nombre de bits spécifique peut être effectuée. Cette validation est activée avec l'option -v, suivie d'un nombre maximal de bits pour les entrées utilisées :

python3 src/simplify_general.py "x+x" -v 3

Là encore, en cas de résultat incorrect, la sortie peut ressembler à ce qui suit :

*** Expression x+x
*** ... verify via evaluation ... [                    ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2

Les constantes apparaissant dans les expressions de sortie de GAMBA peuvent évidemment dépendre du nombre de bits utilisé pour les constantes ainsi que pour les variables. Ce nombre est $64$ par défaut et peut être défini à l'aide de l'option -b :

python3 src/simplify_general.py "-x" -b 32

Par défaut, les constantes apparaissant dans la sortie sont affichées dans la représentation la plus proche possible de zéro. C'est-à-dire que, dans le cas ci-dessus, le nombre -1 serait conservé :

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

Ce comportement peut être modifié : l'utilisation de l'option -m active une réduction modulo des constantes :

python3 src/simplify_general.py "-x" -b 32 -m

Alors, pour un nombre $b$ de bits, les constantes se situent toujours entre $0$ et $2^b-1$. Par conséquent, l'appel ci-dessus produirait la sortie suivante :

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

Simplification d'expressions linéaires individuelles

Le fichier src/simplify.py est destiné à être utilisé par src/simplify_general.py, mais peut également être exécuté de manière isolée. Utilisez l'option de ligne de commande -h pour voir les paramètres disponibles.

Reproduction des expériences

Le fichier experiments/tests.py peut être utilisé pour reproduire les expériences présentées dans l'article. Par défaut, il exécute GAMBA sur 6 jeux de données :

python3 experiments/tests.py

Alternativement, on peut lui demander d'exécuter SiMBA à la place en utilisant l'option --linear ou -l. Dans ce cas, SiMBA n'est exécuté que sur les MBA dont les vérités terrain sont linéaires :

python3 experiments/tests.py --linear

Des vérifications numériques ou des vérifications à l'aide de Z3 peuvent être activées via les options --check (-c) ou --z3 (-z), respectivement.

Les expressions sont classées en fonction du succès de la simplification ou de la vérification :

• ok : expressions qui sont simplifiées exactement au même résultat que les vérités terrain correspondantes
• okz : expressions dont l'équivalence avec les vérités terrain peut être vérifiée à l'aide de l'algorithme (en simplifiant l'expression moins l'expression de vérité terrain à 0)
• z3 : expressions dont l'équivalence avec les vérités terrain peut être vérifiée à l'aide de Z3
• to : expressions pour lesquelles l'algorithme a atteint un délai d'attente (timeout)
• ng : expressions pour lesquelles la simplification et la vérification n'ont pas abouti
• nc : expressions pour lesquelles l'algorithme, dans le cas où SiMBA est utilisé, n'a pas été exécuté car les vérités terrain ne sont pas linéaires
• err : expressions pour lesquelles une erreur s'est produite

Jeux de données

Les jeux de données à utiliser avec experiments/tests.py se trouvent dans le répertoire experiments/datasets/.

• neureduce.txt : utilisez l'option -d 0 ; provient de https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (avec quelques corrections appliquées)
• mba_obf_linear.txt : utilisez l'option -d 1 ; provient de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 expressions linéaires)
• mba_obf_nonlinear.txt : utilisez l'option -d 2 ; provient de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt et de https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt (500 expressions chacun ; avec quelques corrections pour les expressions non polynomiales)
• syntia.txt : utilisez l'option -d 3 ; provient de MBA-Flatten, dataset/dataset_syntia.txt
• mba_flatten.txt : utilisez l'option -d 4 ; provient de MBA-Flatten, les 1000 premières expressions de dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt
• qsynth_ea.txt : utilisez l'option -d 5 ; provient de https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json

De plus, les jeux de données bonus suivants sont fournis dans le répertoire experiments/datasets/bonus/ (non couverts par la publication) :

• loki_tiny.txt : utilisez l'option -d 6 ; provient de https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBA générées par l'article LOKI pour des expressions de vérité terrain simples ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$), jusqu'à une profondeur de 5

Format des MBA

Le nombre de variables est en théorie illimité, mais bien sûr le temps d'exécution augmente avec le nombre de variables. Il n'y a pas de restriction stricte sur la notation des variables. Elles doivent commencer par une lettre et peuvent contenir des lettres, des chiffres et des underscores. Par exemple, les noms de variables suivants seraient tous valides :

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

Les opérateurs suivants sont pris en charge, classés par précédence en Python :

• $**$ : exponentiation
• $\mathord{\sim}$, $-$ : négation bit à bit et moins unaire
• $*$ : produit
• $+$, $-$ : somme et différence
• << : décalage à gauche
• & : conjonction
• $\mathbin{^\wedge}$ : disjonction exclusive
• $|$ : disjonction inclusive

Des espaces peuvent être utilisés dans les expressions d'entrée. Par exemple, l'expression "x+y" peut également être écrite "x + y".

Veuillez respecter la précédence des opérateurs et utilisez des parenthèses si nécessaire ! Par exemple, les expressions $1 + (x|y)$ et $1 + x|y$ ne sont pas équivalentes car $+$ a une précédence plus élevée que $|$. Notez que cette dernière n'est même pas une MBA linéaire.

Dépendances

Z3

Le solveur SMT Z3 est requis par simplify_general.py et simplify.py si la vérification facultative des expressions simplifiées est utilisée. Si cette option n'est pas utilisée, aucune erreur n'est levée, même si Z3 n'est pas installé.

Installation de Z3 :

• depuis le dépôt GitHub : https://github.com/Z3Prover/z3
• sur Debian : sudo apt-get install python3-z3

NumPy

Le paquet de calcul scientifique NumPy est requis par paresse, mais n'est pas vraiment essentiel au fonctionnement. Remarque : numpy.quantile nécessite au moins la version 1.15.0.

Installation de NumPy :

• depuis le dépôt GitHub : https://github.com/numpy/numpy.git
• sur Debian : sudo apt-get install python3-numpy

Licence

Copyright (c) 2023 Denuvo GmbH, distribué sous GPLv3.

Contact

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