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

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

Reproducibilidad

Para reproducir parte de los experimentos descritos en el artículo, se puede utilizar cualquiera de los archivos de conjuntos de datos contenidos en el directorio data/. Para cada una de las siguientes funciones $e_1,\ldots, e_5$, se proporcionan conjuntos de datos de $1,000$ MBAs lineales equivalentes que utilizan $2$, $3$ o $4$ variables:

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

Para $e_1$, se proporcionan conjuntos de datos adicionales para $5$ a $7$ variables. Estos MBAs se han generado utilizando un algoritmo basado en el método descrito por Zhou et al. en 2007 y descrito en el artículo.

Tenga en cuenta que estos conjuntos de datos se han generado para $b=64$ bits. Para diferentes números de bits, no se puede garantizar su equivalencia con los $e_i$.

Para la reproducción de experimentos adicionales, nos remitimos a los conjuntos de datos proporcionados por el repositorio de MBA-Solver y el repositorio de NeuReduce, respectivamente.

Comprobación de linealidad

El archivo check_linear_mba.py es utilizado por el simplificador, pero también proporciona su propia interfaz, por ejemplo:

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

Comprueba todas las expresiones que se pasan a través de argumentos de línea de comandos. En este caso, daría lugar a la siguiente salida:

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

Formato de los MBAs

El número de variables es en teoría ilimitado, pero por supuesto el tiempo de ejecución aumenta con la cantidad de variables. No hay una restricción estricta sobre la notación de las variables. Deben comenzar con una letra y pueden contener letras, números y guiones bajos. Por ejemplo, los siguientes nombres de variable serían todos válidos:

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

Se admiten los siguientes operadores, ordenados por su precedencia en Python:

• $\mathord{\sim}$, $-$: negación bit a bit y menos unario
• $*$: producto
• $+$, $-$: suma y diferencia
• &: conjunción
• $\mathbin{^\wedge}$: disyunción exclusiva
• $|$: disyunción inclusiva

Se puede utilizar espacios en blanco en las expresiones de entrada. Por ejemplo, la expresión "x+y" puede escribirse alternativamente como "x + y".

Por favor, respete la precedencia de los operadores y utilice paréntesis si es necesario! Por ejemplo, las expresiones $1 + (x|y)$ y $1 + x|y$ no son equivalentes ya que $+$ tiene mayor precedencia que $|$. Tenga en cuenta que esta última ni siquiera es un MBA lineal.

Dependencias

Se requiere el solucionador SMT Z3

• por simplify_dataset.py, donde las expresiones simplificadas se verifican como equivalentes a las expresiones simples correspondientes, y
• por simplify.py si se utiliza la verificación opcional de las expresiones simplificadas. Si esta opción no se utiliza, no se produce ningún error incluso si Z3 no está instalado.

Instalación de Z3:

• desde el repositorio de GitHub: https://github.com/Z3Prover/z3, o
• en Debian: sudo apt-get install python3-z3

Licencia

Copyright (c) 2022 Denuvo GmbH, publicado bajo GPLv3.

Contacto

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