denuvosoftwaresolutions/gambaSimplificación de Expresiones Booleanas-Aritméticas Mixtas Generales: 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:
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}
}
Se proporcionan dos programas principales:
simplify_general.py para la simplificación de MBAs generalessimplify.py para la simplificación de MBAs linealesAdemás, se proporciona un script de prueba para reproducir los resultados indicados en el artículo.
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
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.
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:
Los conjuntos de datos para usar con experiments/tests.py se pueden encontrar en el directorio experiments/datasets/.
-d 0; de https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (con algunas correcciones aplicadas)-d 1; de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 expresiones lineales)-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)-d 3; de MBA-Flatten, dataset/dataset_syntia.txt-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-d 5; de https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.jsonAdemás, se proporcionan los siguientes conjuntos de datos adicionales en el directorio experiments/datasets/bonus/ (no cubiertos en la publicación):
-d 6; de https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBAs generados por el artículo LOKI para expresiones de verdad de terreno simples ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$), hasta profundidad 5El número de variables es, en teoría, ilimitado, pero por supuesto el tiempo de ejecución aumenta con el número 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:
Se admiten los siguientes operadores, ordenados por su precedencia en Python:
Se puede usar espacio en blanco en las expresiones de entrada. Por ejemplo, la expresión "x+y" también puede escribirse como "x + y".
Respete la precedencia de los operadores y use 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 la última ni siquiera es un MBA lineal.
El solucionador SMT Z3 es requerido por simplify_general.py y simplify.py si se utiliza la verificación opcional de expresiones simplificadas. Si esta opción no se usa, no se lanza ningún error incluso si Z3 no está instalado.
Instalación de Z3:
sudo apt-get install python3-z3El paquete de computación científica NumPy se requiere por pereza, pero no es realmente esencial para el funcionamiento. Nota: se requiere al menos la versión 1.15.0 para numpy.quantile
Instalación de NumPy:
sudo apt-get install python3-numpyCopyright (c) 2023 Denuvo GmbH, publicado bajo GPLv3.