GAMBA

GAMBA es una herramienta para la simplificación de expresiones mixtas booleanas-aritméticas (MBAs). GAMBA es el acrónimo de General Advanced Mixed Boolean Arithmetic simplifier (simplificador aritmético booleano mixto avanzado general). Utiliza el simplificador algebraico lineal SiMBA para simplificar iterativamente subexpresiones lineales de un MBA de entrada potencialmente no lineal. En general, sus ingredientes principales son los siguientes:

• Uso de árboles de sintaxis abstracta (ASTs)
• Aislamiento de subexpresiones lineales mediante la aplicación de transformaciones (triviales y más sofisticadas)
• Refactorización para aumentar la probabilidad de construir subexpresiones lineales que puedan simplificarse
• Simplificación de subexpresiones lineales mediante SiMBA
• Lógica de sustitución para eliminar temporalmente constantes no triviales y operaciones aritméticas dentro de operaciones bit a bit

GAMBA se basa en el siguiente artículo; véanse también las diapositivas utilizadas para la presentación:

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

Contenido

Se proporcionan dos programas principales:

• simplify_general.py para la simplificación de MBAs generales
• simplify.py para la simplificación de MBAs lineales

Además, se proporciona un script de prueba para reproducir los resultados indicados en el artículo.

Uso

Simplificación de expresiones generales individuales

Para simplificar una única expresión expr, utilice

python3 src/simplify_general.py "expr"

Alternativamente, se pueden simplificar varias expresiones a la vez, p. ej.:

python3 src/simplify_general.py "x+x" "y*y" "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 provocar 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 y*y
*** ... simplified to y**2
*** Expression a
*** ... simplified to a

Si se utiliza la opción -z, los resultados de la simplificación se verifican finalmente para que sean semánticamente equivalentes a las expresiones originales mediante Z3. Esto no afecta a la salida de la línea de comandos siempre que el algoritmo funcione correctamente:

python3 src/simplify_general.py "x+x" -z

Si el algoritmo produjera un resultado incorrecto, se activaría el siguiente error:

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

Además, se puede realizar una validación numérica de los resultados con todas las entradas posibles hasta un número de bits específico. Esto se habilita con la opción -v, seguida de un número máximo de bits de las entradas utilizadas:

python3 src/simplify_general.py "x+x" -v 3

Nuevamente, en caso de un resultado incorrecto, la salida podría verse así:

*** Expression x+x
*** ... verify via evaluation ... [                    ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2

Las constantes que aparecen en las expresiones de salida de GAMBA pueden depender obviamente del número de bits utilizados tanto para las constantes como para las variables. Este número es $64$ por defecto y se puede configurar con la opción -b:

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

Por defecto, las constantes que aparecen en la salida se notifican en la representación lo más cercana posible a cero. Es decir, en el caso anterior, el número -1 permanecería:

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

Este comportamiento se puede cambiar: con la opción -m, se habilita una reducción módulo de las constantes:

python3 src/simplify_general.py "-x" -b 32 -m

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

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

Simplificación de expresiones lineales individuales

El archivo src/simplify.py está pensado para ser utilizado por src/simplify_general.py, pero también puede ejecutarse de forma aislada. Utilice la opción de línea de comandos -h para ver las configuraciones disponibles.

Reproducción de experimentos

El archivo experiments/tests.py se puede utilizar para reproducir los experimentos indicados en el artículo. Por defecto, ejecuta GAMBA en 6 conjuntos de datos:

python3 experiments/tests.py

Alternativamente, se le puede indicar que ejecute SiMBA en su lugar utilizando la opción --linear o -l. En ese caso, SiMBA solo se ejecuta en MBAs con verdades de terreno lineales:

python3 experiments/tests.py --linear

Las comprobaciones numéricas o las comprobaciones con Z3 se pueden habilitar mediante las opciones --check (-c) o --z3 (-z), respectivamente.

Las expresiones se clasifican según el éxito de la simplificación o verificación:

• ok: expresiones que se simplifican exactamente al mismo resultado que las correspondientes verdades de terreno
• okz: expresiones cuya equivalencia con las verdades de terreno se puede verificar mediante el algoritmo (simplificando la expresión menos la expresión de verdad de terreno a 0)
• z3: expresiones cuya equivalencia con las verdades de terreno se puede verificar mediante Z3
• to: expresiones para las que el algoritmo agotó el tiempo de espera
• ng: expresiones para las que la simplificación y la verificación no tuvieron éxito
• nc: expresiones para las que el algoritmo, en caso de que se utilice SiMBA, no se ejecutó porque las verdades de terreno no son lineales
• err: expresiones para las que se produjo un error

Conjuntos de datos

Los conjuntos de datos para usar con experiments/tests.py se pueden encontrar en el directorio experiments/datasets/.

• neureduce.txt: Use la opción -d 0; de https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (con algunas correcciones aplicadas)
• mba_obf_linear.txt: Use la opción -d 1; de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 expresiones lineales)
• mba_obf_nonlinear.txt: Use la opción -d 2; de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt y https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt (500 expresiones cada uno; con algunas correcciones para expresiones no polinómicas)
• syntia.txt: Use la opción -d 3; de MBA-Flatten, dataset/dataset_syntia.txt
• mba_flatten.txt: Use la opción -d 4; de MBA-Flatten, primeras 1000 expresiones de dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt
• qsynth_ea.txt: Use la opción -d 5; de https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json