SiMBA

SiMBA est un outil pour la simplification d'expressions mixtes booléennes-arithmétiques linéaires (MBA). Comme MBA-Blast et MBA-Solver, il utilise une approche entièrement algébrique basée sur l'idée qu'un MBA linéaire est entièrement déterminé par ses valeurs sur l'ensemble des zéros et des uns, mais en exploitant les nouvelles perspectives qu'une transformation vers l'espace 1-bit n'est pas nécessaire pour cela.

Il est basé sur l'article suivant :

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

Trouvez les diapositives et un enregistrement vidéo de la présentation. Également disponible via ACM.

Contenu

Deux programmes principaux (Python 3) sont fournis :

• simplify.py pour la simplification de MBA linéaires individuels
• simplify_dataset.py pour la simplification d'un ensemble de MBA linéaires contenus dans un fichier et leur vérification via une comparaison avec des expressions plus simples correspondantes également contenues dans ce fichier

De plus, le programme check_linear_mba.py peut être utilisé pour vérifier si les expressions représentent des MBA linéaires.

Utilisation

Simplification d'expressions individuelles

Pour simplifier une expression unique expr, utilisez

python3 src/simplify.py "expr"

Alternativement, plusieurs expressions peuvent être simplifiées en une seule fois, par exemple :

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

En fait, chaque argument de ligne de commande qui n'est pas une option est considéré comme une expression à simplifier. Notez que l'omission des guillemets peut entraîner un comportement indésirable. Les résultats de la simplification sont affichés dans la ligne de commande comme suit :

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

Par défaut, aucune vérification n'est effectuée pour savoir si l'expression d'entrée est un MBA linéaire. Cette vérification peut être activée optionnellement via l'option -l :

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

Puisque $x*x$ n'est pas un MBA linéaire, la sortie suivante apparaîtrait dans ce cas :

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

Si l'option -z est utilisée, les résultats de simplification sont finalement vérifiés comme étant égaux aux expressions originales en utilisant Z3. Cela n'affecte pas la sortie de la ligne de commande tant que l'algorithme fonctionne correctement et que l'expression d'entrée est un MBA linéaire :

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

Cela déclencherait l'erreur suivante :

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

Puisque les constantes apparaissant dans les expressions de sortie de SiMBA sont toujours non négatives, elles peuvent dépendre du nombre de bits utilisé pour les constantes ainsi que les variables. Ce nombre est $64$ par défaut et peut être défini via l'option -b :

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

Pour un nombre $b$ de bits, les constantes apparaissant dans la sortie se situent toujours entre $0$ et $2^b-1$. Ainsi, l'appel ci-dessus produirait la sortie suivante :

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

Simplification et vérification d'expressions à partir d'un fichier

Pour simplifier des expressions stockées dans un fichier avec le chemin path_to_file, utilisez

python3 src/simplify_dataset.py -f path_to_file

C'est-à-dire que le fichier doit être spécifié via l'option -f. Chaque ligne du fichier doit contenir une expression complexe ainsi qu'une expression plus simple équivalente, séparées par une virgule, par exemple :

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

Pour chaque ligne, l'expression complexe et l'expression simple sont simplifiées et finalement comparées. La raison de simplifier la seconde est de rendre les résultats de vérification indépendants des espaces, de l'ordre des facteurs ou des termes, etc.

Comme avec simplify.py, une vérification de linéarité ainsi qu'une vérification de simplification correcte peuvent être activées en utilisant les options -l et -z, respectivement, et le nombre de bits peut être spécifié via l'option -b. Si l'on souhaite exécuter SiMBA sur seulement un certain nombre maximum d'expressions contenues dans le fichier spécifié, ce nombre maximum peut être spécifié via l'option -r :

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

Si some_file.txt contenait les expressions listées ci-dessus, seules les deux premières seraient simplifiées :

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

Dans tous les cas, la sortie donne des informations sur

• le nombre total d'expressions dans l'entrée,
• le nombre d'expressions qui ont pu être vérifiées comme équivalentes à l'expression simple correspondante en utilisant Z3 après simplification (sauf si le résultat de la simplification a déjà exactement la même représentation sous forme de chaîne),
• le nombre d'expressions qui sont simplifiées exactement à la même expression que l'expression simple correspondante, et
• le temps d'exécution moyen en secondes.

Veuillez noter qu'une vérification optionnelle d'une simplification correcte à l'aide de Z3 contribue au temps d'exécution, tandis que ce n'est pas le cas pour la comparaison des résultats de simplification des paires constituées d'une expression complexe et d'une expression plus simple.

Par défaut, les résultats de simplification ne sont pas imprimés, seules ces statistiques sont présentées. Si des informations sur les premiers sont souhaitées, l'option -v peut être utilisée :

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

La sortie suivante serait alors affichée :

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

Une autre option -e offre la possibilité d'encoder les sorties de toutes les expressions par des fonctions affines $f(x) = ax+b$ avec des entiers aléatoires $a,b$ compris entre $1$ et $2^b-1$ si $b$ est le nombre de bits :

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

Bien sûr, la même fonction est appliquée à une paire d'expressions dans la même ligne. Cela donnerait une sortie similaire à la suivante :

Simplify expressions from data/some_file.txt ...

    *** 1 groundtruth 10623056950310032687+5038261596809828791*x+5038261596809828791*y, simplified 10623056950310032687+5038261596809828791*x+5038261596809828791*y => equal: True, verified: True
    *** 2 groundtruth 15181401701264988765+3962868592131193124*(x&y), simplified 15181401701264988765+3962868592131193124*(x&y) => equal: True, verified: True
    *** 3 groundtruth 6812440940417974076+11894131080657788315*(a^b), simplified 6812440940417974076+11894131080657788315*(a^b) => equal: True, verified: True
    *** 4 groundtruth 4558303267887122851+10271005790757592209*s, simplified 4558303267887122851+10271005790757592209*s => equal: True, verified: True

  * total count: 4
  * verified: 4
  * equal: 4
  * average duration: 0.00019435951253399253

Reproductibilité

Pour une reproduction d'une partie des expériences énoncées dans l'article, on peut utiliser n'importe quel fichier de jeu de données contenu dans le répertoire data/. Pour chacune des fonctions suivantes $e_1,\ldots, e_5$, des jeux de données de $1,000$ MBA linéaires équivalents utilisant $2$, $3$ ou $4$ variables sont fournis :

• $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$

Pour $e_1$, des jeux de données supplémentaires pour $5$ à $7$ variables sont fournis. Ces MBA ont été générés en utilisant un algorithme basé sur la méthode décrite par Zhou et al. en 2007 et décrite dans l'article.

Veuillez noter que ces jeux de données ont été générés pour $b=64$ bits. Pour un nombre de bits différent, leur équivalence aux $e_i$ ne peut être garantie.

Pour la reproduction d'autres expériences, nous renvoyons aux jeux de données fournis par le dépôt MBA-Solver et le dépôt NeuReduce, respectivement.

Vérification de la linéarité

Le fichier check_linear_mba.py est utilisé par le simplificateur, mais il fournit également sa propre interface, par exemple :

python3 src/check_linear_mba.py "x+x" "x*x"

Il vérifie toutes les expressions qui sont passées via les arguments de la ligne de commande. Dans ce cas, cela produirait la sortie suivante :

*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid

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 forte 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 conviendraient tous :

• $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 leur précédence en Python :

• $\mathord{\sim}$, $-$ : négation au niveau du bit et moins unaire
• $*$ : produit
• $+$, $-$ : somme et différence
• & : conjonction
• $\mathbin{^\wedge}$ : disjonction exclusive
• $|$ : disjonction inclusive

Les espaces peuvent être utilisés dans les expressions d'entrée. Par exemple, l'expression "x+y" peut être écrite alternativement "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 la dernière n'est même pas un MBA linéaire.

Dépendances

Le solveur SMT Z3 est requis

• par simplify_dataset.py où les expressions simplifiées sont vérifiées comme équivalentes aux expressions simples correspondantes, et
• par simplify.py si la vérification optionnelle des expressions simplifiées est utilisée. Si cette option n'est pas utilisée, aucune erreur n'est déclenchée même si Z3 n'est pas installé.

Installation de Z3 :

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

Licence

Copyright (c) 2022 Denuvo GmbH, publié sous GPLv3.

Contact

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