SiMBA

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.

Conteúdo

Dois programas principais (Python 3) são fornecidos:

• simplify.py para simplificação de MBAs lineares individuais
• simplify_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 arquivo

Adicionalmente, o programa check_linear_mba.py pode ser usado para verificar se expressões representam MBAs lineares.

Uso

Simplificando expressões individuais

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

Simplificando e verificando expressões de um arquivo

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:

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

• o número total de expressões na entrada,
• o número de expressões que puderam ser verificadas como equivalentes à expressão mais simples correspondente usando Z3 após simplificação (a menos que o resultado da simplificação já tenha exatamente a mesma representação em string),
• o número de expressões que são simplificadas para exatamente a mesma expressão que a expressão simples correspondente, e
• o tempo médio de execução em segundos.

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