denuvosoftwaresolutions/simbaDesofuscação Eficiente de Expressões Mistas Booleanas-Aritméticas Lineares
SiMBA é uma ferramenta para simplificação de expressões booleanas-aritméticas mistas lineares (MBAs). Como MBA-Blast e MBA-Solver, utiliza uma abordagem totalmente algébrica baseada na ideia de que uma MBA linear é completamente determinada por seus valores no conjunto de zeros e uns, mas aproveitando os novos insights de que uma transformação para o espaço de 1 bit não é necessária para isso.
Baseia-se no seguinte artigo:
@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}}
}
Encontre slides e uma gravação em vídeo da apresentação. Também disponível via ACM.
Dois programas principais (Python 3) são fornecidos:
simplify.py para simplificação de MBAs lineares individuaissimplify_dataset.py para simplificação de um conjunto de MBAs lineares contidos em um arquivo e sua verificação através de comparação com expressões mais simples correspondentes também contidas neste arquivoAdicionalmente, o programa check_linear_mba.py pode ser usado para verificar se expressões representam MBAs lineares.
Para simplificar uma única expressão expr, use
python3 src/simplify.py "expr"
Alternativamente, múltiplas expressões podem ser simplificadas de uma só vez, por exemplo:
python3 src/simplify.py "x+x" "a&a"
Na verdade, cada argumento de linha de comando que não é uma opção é considerado uma expressão a ser simplificada. Note que omitir as aspas pode implicar 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 a
*** ... simplified to a
Por padrão, nenhuma verificação se a expressão de entrada é uma MBA linear é realizada. Essa verificação pode ser opcionalmente ativada através da opção -l:
python3 src/simplify.py "x*x" -l
Como $x*x$ não é uma MBA linear, a seguinte saída apareceria neste caso:
*** Expression x*x
Error: Input expression may be no linear MBA: x*x
Se a opção -z for usada, os resultados da simplificação são finalmente verificados como iguais às expressões originais usando Z3. Isso não afeta a saída da linha de comando, desde que o algoritmo funcione corretamente e a expressão de entrada seja uma MBA linear:
python3 src/simplify.py "x*x" -z
Isso acionaria o seguinte erro:
*** Expression x*x
Error in simplification! Simplified expression is not equivalent to original one!
Como as constantes que ocorrem nas expressões de saída do SiMBA são sempre não negativas, elas podem depender do número de bits usados para constantes e também variáveis. Esse número é $64$ por padrão e pode ser definido usando a opção -b:
python3 src/simplify.py "-x" -b 32
Para um número $b$ de bits, as constantes que ocorrem na saída sempre estão entre $0$ e $2^b-1$. Portanto, a chamada acima implicaria a seguinte saída:
*** Expression -x
*** ... simplified to 4294967295*x
Para simplificar expressões armazenadas em um arquivo com caminho path_to_file, use
python3 src/simplify_dataset.py -f path_to_file
Isto é, o arquivo deve ser especificado usando a opção -f. Cada linha do arquivo deve conter uma expressão complexa e uma equivalente mais simples, separadas por vírgula, por exemplo:
(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 linha, tanto a expressão complexa quanto a simples são simplificadas e finalmente comparadas. A razão para simplificar a última é tornar os resultados da verificação independentes de espaços em branco, ordem dos fatores ou somandos, etc.
Assim como com simplify.py, uma verificação de linearidade, bem como uma verificação de simplificação correta, podem ser ativadas usando as opções -l e -z, respectivamente, e o número de bits pode ser especificado usando a opção -b. Se deseja executar o SiMBA apenas em um certo número máximo de expressões contidas no arquivo especificado, esse número máximo pode ser especificado através da opção -r:
python3 src/simplify_dataset.py -f some_file.txt -r 2
Se some_file.txt contivesse as expressões listadas acima, apenas as duas primeiras seriam simplificadas:
Simplify expressions from data/some_file.txt ...
* total count: 2
* verified: 2
* equal: 2
* average duration: 0.00014788552653044462
Em qualquer caso, a saída fornece informações sobre
Observe que uma verificação opcional de uma simplificação correta usando Z3 contribui para o tempo de execução, enquanto isso não ocorre para a comparação dos resultados de simplificação dos pares consistindo em uma expressão complexa e uma mais simples.
Por padrão, os resultados da simplificação não são impressos, mas apenas essas estatísticas são apresentadas. Se informações sobre os primeiros forem desejadas, a opção -v pode ser usada:
python3 src/simplify_dataset.py -f some_file.txt -v
A seguinte saída seria então mostrada:
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
Outra opção -e fornece a possibilidade de codificar as saídas de todas as expressões por funções afins $f(x) = ax+b$ com inteiros aleatórios $a,b$ entre $1$ e $2^b-1$ se $b$ for o número de bits:
python3 src/simplify_dataset.py -f some_file.txt -v -e
Naturalmente, a mesma função é aplicada a um par de expressões na mesma linha. Isso daria uma saída semelhante à seguinte:
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
Para reprodução de parte dos experimentos descritos no artigo, pode-se usar qualquer um dos arquivos de conjunto de dados contidos no diretório data/. Para cada uma das seguintes funções $e_1,\ldots, e_5$, são fornecidos conjuntos de dados de $1,000$ MBAs lineares equivalentes usando $2$, $3$ ou $4$ variáveis:
Para $e_1$, conjuntos de dados adicionais para $5$ a $7$ variáveis são fornecidos. Esses MBAs foram gerados usando um algoritmo baseado no método descrito por Zhou et al. em 2007 e descrito no artigo.
Observe que esses conjuntos de dados foram gerados para $b=64$ bits. Para diferentes números de bits, sua equivalência aos $e_i$ não pode ser garantida.
Para reprodução de experimentos adicionais, referimo-nos aos conjuntos de dados fornecidos pelo repositório MBA-Solver e pelo repositório NeuReduce, respectivamente.
O arquivo check_linear_mba.py é usado pelo simplificador, mas também fornece sua própria interface, por exemplo:
python3 src/check_linear_mba.py "x+x" "x*x"
Ele verifica todas as expressões que são passadas via argumentos de linha de comando. Neste caso, implicaria a seguinte saída:
*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid
O número de variáveis é teoricamente ilimitado, mas claro que o tempo de execução aumenta com a contagem de variáveis. Não há restrição forte na 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:
Os seguintes operadores são suportados, ordenados por sua precedência em Python:
Espaços em branco podem ser usados nas expressões de entrada. Por exemplo, a expressão "x+y" pode alternativamente ser escrita 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 $|$. Note que a última nem sequer é uma MBA linear.
O Solucionador SMT Z3 é necessário
Instalando Z3:
sudo apt-get install python3-z3Copyright (c) 2022 Denuvo GmbH, lançado sob GPLv3.