SiMBA

SiMBA es una herramienta para la simplificación de expresiones booleanas-aritméticas mixtas lineales (MBA). Al igual que MBA-Blast y MBA-Solver, utiliza un enfoque completamente algebraico basado en la idea de que un MBA lineal está completamente determinado por sus valores en el conjunto de ceros y unos, pero aprovechando los nuevos conocimientos de que una transformación al espacio de 1 bit no es necesaria para ello.

Se basa en el siguiente artículo:

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

Encuentre las diapositivas y una grabación de video de la presentación. También disponible a través de ACM.

Contenido

Se proporcionan dos programas principales (Python 3):

• simplify.py para la simplificación de MBAs lineales individuales
• simplify_dataset.py para la simplificación de un conjunto de MBAs lineales contenidos en un archivo y su verificación mediante una comparación con expresiones más simples correspondientes también contenidas en este archivo

Adicionalmente, el programa check_linear_mba.py puede utilizarse para comprobar si las expresiones representan MBAs lineales.

Uso

Simplificación de expresiones individuales

Para simplificar una única expresión expr, utilice

python3 src/simplify.py "expr"

Alternativamente, se pueden simplificar varias expresiones a la vez, por ejemplo:

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

De hecho, cada argumento de línea de comandos que no sea una opción se considera una expresión a simplificar. Tenga en cuenta que omitir las comillas puede implicar un comportamiento no deseado. Los resultados de la simplificación se imprimen en la línea de comandos como se muestra a continuación:

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

Por defecto no se realiza ninguna comprobación de si la expresión de entrada es un MBA lineal. Esta comprobación se puede habilitar opcionalmente mediante la opción -l:

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

Dado que $x*x$ no es un MBA lineal, la siguiente salida aparecería en este caso:

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

Si se utiliza la opción -z, los resultados de la simplificación se verifican finalmente como iguales a las expresiones originales mediante Z3. Esto no afecta la salida de la línea de comandos siempre que el algoritmo funcione correctamente y la expresión de entrada sea un MBA lineal:

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

Esto provocaría el siguiente error:

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

Debido a que las constantes que aparecen en las expresiones de salida de SiMBA son siempre no negativas, pueden depender del número de bits utilizado tanto para las constantes como para las variables. Este número es $64$ por defecto y se puede establecer mediante la opción -b:

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

Para un número $b$ de bits, las constantes que aparecen en la salida siempre se encuentran entre $0$ y $2^b-1$. Por lo tanto, la llamada anterior produciría la siguiente salida:

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

Simplificación y verificación de expresiones desde un archivo

Para simplificar expresiones almacenadas en un archivo con ruta path_to_file, utilice

python3 src/simplify_dataset.py -f path_to_file

Es decir, el archivo debe especificarse mediante la opción -f. Cada línea del archivo debe contener una expresión compleja y una más simple equivalente, separadas por una coma, por ejemplo:

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

Para cada línea, se simplifican tanto la expresión compleja como la simple y finalmente se comparan. La razón para simplificar esta última es hacer que los resultados de verificación sean independientes de los espacios en blanco, el orden de los factores o sumandos, etc.

Al igual que con simplify.py, se puede habilitar una comprobación de linealidad y una comprobación de simplificación correcta mediante las opciones -l y -z, respectivamente, y el número de bits se puede especificar mediante la opción -b. Si se desea ejecutar SiMBA solo sobre un cierto número máximo de expresiones contenidas en el archivo especificado, este número máximo se puede especificar mediante la opción -r:

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

Si some_file.txt contuviera las expresiones enumeradas anteriormente, solo se simplificarían las dos primeras:

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

En cualquier caso, la salida proporciona información sobre

• el número total de expresiones en la entrada,
• el número de expresiones que pudieron verificarse como equivalentes a la expresión más simple correspondiente usando Z3 después de la simplificación (a menos que el resultado de la simplificación ya tenga exactamente la misma representación de cadena),
• el número de expresiones que se simplifican a la misma expresión que la expresión simple correspondiente, y
• el tiempo de ejecución promedio en segundos.

Tenga en cuenta que una verificación opcional de una simplificación correcta mediante Z3 contribuye al tiempo de ejecución, mientras que no es el caso para la comparación de los resultados de simplificación de los pares que consisten en una expresión compleja y una más simple.

Por defecto, los resultados de la simplificación no se imprimen, sino que solo se presentan estas estadísticas. Si se desea información sobre los primeros, se puede utilizar la opción -v:

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

A continuación se mostraría la siguiente salida:

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

Otra opción, -e, proporciona la posibilidad de codificar las salidas de todas las expresiones mediante funciones afines $f(x) = ax+b$ con enteros aleatorios $a,b$ entre $1$ y $2^b-1$ si $b$ es el número de bits:

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

Por supuesto, la misma función se aplica a un par de expresiones en la misma línea. Esto daría una salida similar a la siguiente:

Simplify expressions from data/some_file.txt ...