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