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/.