GAMBA

GAMBA é uma ferramenta para simplificação de expressões booleanas-aritméticas mistas (MBAs). GAMBA é a abreviação de General Advanced Mixed Boolean Arithmetic simplifier (Simplificador Geral Avançado de Aritmética Booleana Mista). Ela usa o simplificador algébrico linear SiMBA para simplificar iterativamente subexpressões lineares de uma entrada MBA potencialmente não linear. Seus ingredientes principais são os seguintes:

• Uso de árvores de sintaxe abstrata (ASTs)
• Isolamento de subexpressões lineares via aplicação de transformações (triviais e mais sofisticadas)
• Refatoração para aumentar a chance de construir subexpressões lineares que possam ser simplificadas
• Simplificação de subexpressões lineares usando SiMBA
• Lógica de substituição para se livrar temporariamente de constantes não triviais e operações aritméticas dentro de operações bit a bit

GAMBA é baseado no seguinte artigo, veja também os slides usados para apresentação:

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

Conteúdo

Dois programas principais são fornecidos:

• simplify_general.py para a simplificação de MBAs gerais
• simplify.py para a simplificação de MBAs lineares

Além disso, um script de teste é fornecido para reproduzir os resultados apresentados no artigo.

Uso

Simplificando expressões gerais únicas

Para simplificar uma única expressão expr, use

python3 src/simplify_general.py "expr"

Alternativamente, múltiplas expressões podem ser simplificadas de uma vez, ex.:

python3 src/simplify_general.py "x+x" "y*y" "a&a"

Na verdade, cada argumento de linha de comando que não seja uma opção é considerado uma expressão a ser simplificada. Observe que omitir as aspas pode levar a um comportamento indesejado. Os resultados da simplificação são impressos na linha de comando conforme mostrado a seguir:

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

Se a opção -z for usada, os resultados da simplificação são finalmente verificados como semanticamente equivalentes às expressões originais usando Z3. Isso não afeta a saída da linha de comando desde que o algoritmo funcione corretamente:

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

Se o algoritmo produzisse um resultado errado, o seguinte erro seria acionado:

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

Além disso, uma validação numérica dos resultados com todas as entradas possíveis até uma contagem de bits específica pode ser realizada. Isso é habilitado com a opção -v, seguida por uma contagem máxima de bits das entradas usadas:

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

Novamente, em caso de resultado errado, a saída pode se parecer com o seguinte:

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

As constantes que ocorrem nas expressões de saída do GAMBA podem obviamente depender do número de bits usados para constantes e variáveis. Esse número é $64$ por padrão e pode ser definido usando a opção -b:

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

Por padrão, as constantes que ocorrem na saída são relatadas na representação mais próxima possível de zero. Ou seja, no caso acima, o número -1 permaneceria:

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

Esse comportamento pode ser alterado: Usando a opção -m, uma redução modular de constantes é habilitada:

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

Então, para um número $b$ de bits, as constantes sempre ficam entre $0$ e $2^b-1$. Portanto, a chamada acima implicaria na seguinte saída:

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

Simplificando expressões lineares únicas

O arquivo src/simplify.py deve ser utilizado por src/simplify_general.py, mas também pode ser executado isoladamente. Use a opção de linha de comando -h para ver as configurações disponíveis.

Reprodução de experimentos

O arquivo experiments/tests.py pode ser usado para reproduzir os experimentos apresentados no artigo. Por padrão, ele executa o GAMBA em 6 conjuntos de dados:

python3 experiments/tests.py

Alternativamente, pode ser instruído a executar o SiMBA usando a opção --linear ou -l. Nesse caso, o SiMBA é executado apenas em MBAs com ground truths lineares:

python3 experiments/tests.py --linear

Verificações numéricas ou verificações usando Z3 podem ser habilitadas através das opções --check (-c) ou --z3 (-z), respectivamente.

As expressões são categorizadas dependendo do sucesso da simplificação ou verificação:

• ok: expressões que são simplificadas exatamente para o mesmo resultado que os ground truths correspondentes
• okz: expressões cuja equivalência aos ground truths pode ser verificada usando o algoritmo (simplificando a expressão menos a expressão ground truth para 0)
• z3: expressões cuja equivalência aos ground truths pode ser verificada usando Z3
• to: expressões para as quais o algoritmo atingiu um timeout
• ng: expressões para as quais simplificação e verificação não foram bem-sucedidas
• nc: expressões para as quais o algoritmo, no caso de uso do SiMBA, não foi executado pois os ground truths não são lineares
• err: expressões para as quais ocorreu um erro

Conjuntos de dados

Conjuntos de dados para uso com experiments/tests.py podem ser encontrados no diretório experiments/datasets/.

• neureduce.txt: Use a opção -d 0; de https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (com algumas correções aplicadas)
• mba_obf_linear.txt: Use a opção -d 1; de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 expressões lineares)
• mba_obf_nonlinear.txt: Use a opção -d 2; de https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt e https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt (500 expressões cada; com algumas correções para expressões não polinomiais)
• syntia.txt: Use a opção -d 3; de MBA-Flatten, dataset/dataset_syntia.txt
• mba_flatten.txt: Use a opção -d 4; de MBA-Flatten, primeiras 1000 expressões de dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt
• qsynth_ea.txt: Use a opção -d 5; de https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json

Além disso, os seguintes conjuntos de dados bônus são fornecidos no diretório experiments/datasets/bonus/ (não cobertos na publicação):

• loki_tiny.txt: Use a opção -d 6; de https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBAs gerados pelo artigo LOKI para expressões ground truth simples ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$), até profundidade 5

Formato dos MBAs

O número de variáveis é teoricamente ilimitado, mas, é claro, o tempo de execução aumenta com a contagem de variáveis. Não há restrição forte quanto à notação das variáveis. Elas devem começar com uma letra e podem conter letras, números e sublinhados. Por exemplo, os seguintes nomes de variáveis seriam 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$, ...
• ...

Os seguintes operadores são suportados, ordenados por sua precedência em Python:

• $**$: exponenciação
• $\mathord{\sim}$, $-$: negação bit a bit e menos unário
• $*$: produto
• $+$, $-$: soma e diferença
• <<: deslocamento à esquerda
• &: conjunção
• $\mathbin{^\wedge}$: disjunção exclusiva
• $|$: disjunção inclusiva

Espaços em branco podem ser usados nas expressões de entrada. Por exemplo, a expressão "x+y" pode ser escrita alternativamente como "x + y".

Respeite a precedência dos operadores e use parênteses se necessário! Por exemplo, as expressões $1 + (x|y)$ e $1 + x|y$ não são equivalentes, pois $+$ tem precedência maior que $|$. Observe que a última nem mesmo é uma MBA linear.

Dependências

Z3

O solucionador SMT Z3 é necessário para simplify_general.py e simplify.py se a verificação opcional de expressões simplificadas for usada. Se essa opção não for usada, nenhum erro será gerado mesmo que o Z3 não esteja instalado.

Instalando o Z3:

• do repositório do Github: https://github.com/Z3Prover/z3
• no Debian: sudo apt-get install python3-z3

NumPy

O pacote de computação científica NumPy é necessário por preguiça, mas não é essencial para a operação. Nota: pelo menos a versão 1.15.0 é necessária para numpy.quantile

Instalando o NumPy:

• do repositório do Github: https://github.com/numpy/numpy.git
• no Debian: sudo apt-get install python3-numpy

Licença

Copyright (c) 2023 Denuvo GmbH, lançado sob GPLv3.

Contato

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