SiMBA

SiMBA è uno strumento per la semplificazione di espressioni lineari miste booleano-aritmetiche (MBA). Come MBA-Blast e MBA-Solver, utilizza un approccio completamente algebrico basato sull'idea che una MBA lineare è completamente determinata dai suoi valori sull'insieme di zeri e uni, ma sfruttando le nuove intuizioni che una trasformazione nello spazio a 1 bit non è necessaria per questo.

Si basa sul seguente articolo:

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

Le slides e la registrazione video della presentazione sono disponibili. Disponibile anche tramite ACM.

Contenuto

Vengono forniti due programmi principali (Python 3):

• simplify.py per la semplificazione di singole MBA lineari
• simplify_dataset.py per la semplificazione di un insieme di MBA lineari contenute in un file e la loro verifica tramite un confronto con le corrispondenti espressioni più semplici anch'esse contenute in questo file

Inoltre, il programma check_linear_mba.py può essere usato per verificare se le espressioni rappresentano MBA lineari.

Uso

Semplificazione di singole espressioni

Per semplificare una singola espressione expr, usa

python3 src/simplify.py "expr"

In alternativa, più espressioni possono essere semplificate contemporaneamente, ad esempio:

python3 src/simplify.py "x+x" "a&a"

In effetti, ogni argomento della riga di comando che non è un'opzione viene considerato come un'espressione da semplificare. Nota che l'omissione delle virgolette può causare comportamenti indesiderati. I risultati della semplificazione vengono stampati sulla riga di comando come mostrato di seguito:

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

Per impostazione predefinita non viene eseguito alcun controllo sul fatto che l'espressione di input sia una MBA lineare. Questo controllo può essere opzionalmente abilitato tramite l'opzione -l:

python3 src/simplify.py "x*x" -l

Poiché $x*x$ non è una MBA lineare, in questo caso verrebbe mostrato il seguente output:

*** Expression x*x
Error: Input expression may be no linear MBA: x*x

Se viene utilizzata l'opzione -z, i risultati della semplificazione vengono infine verificati come uguali alle espressioni originali usando Z3. Ciò non influisce sull'output della riga di comando finché l'algoritmo funziona correttamente e l'espressione di input è una MBA lineare:

python3 src/simplify.py "x*x" -z

Questo comporterebbe il seguente errore:

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

Poiché le costanti che compaiono nelle espressioni di output di SiMBA sono sempre non negative, possono dipendere dal numero di bit usati sia per le costanti che per le variabili. Questo numero è $64$ per impostazione predefinita e può essere impostato usando l'opzione -b:

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

Per un numero $b$ di bit, le costanti che compaiono nell'output sono sempre comprese tra $0$ e $2^b-1$. Quindi la chiamata precedente produrrebbe il seguente output:

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

Semplificazione e verifica di espressioni da un file

Per semplificare espressioni memorizzate in un file con percorso path_to_file, usa

python3 src/simplify_dataset.py -f path_to_file

Il file deve essere specificato usando l'opzione -f. Ogni riga del file deve contenere un'espressione complessa e una equivalente più semplice, separate da una virgola, ad esempio:

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

Per ogni riga, sia l'espressione complessa sia quella semplice vengono semplificate e infine confrontate. Il motivo per cui si semplifica quest'ultima è rendere i risultati della verifica indipendenti dagli spazi bianchi, dall'ordine dei fattori o degli addendi, ecc.

Come per simplify.py, un controllo di linearità e un controllo per una corretta semplificazione possono essere abilitati rispettivamente usando le opzioni -l e -z, e il numero di bit può essere specificato usando l'opzione -b. Se si vuole eseguire SiMBA solo su un certo numero massimo di espressioni contenute nel file specificato, questo numero massimo può essere specificato tramite l'opzione -r:

python3 src/simplify_dataset.py -f some_file.txt -r 2

Se some_file.txt contenesse le espressioni elencate sopra, solo le prime due verrebbero semplificate:

Simplify expressions from data/some_file.txt ...
  * total count: 2
  * verified: 2
  * equal: 2
  * average duration: 0.00014788552653044462

In ogni caso, l'output fornisce informazioni su:

• il numero totale di espressioni nell'input,
• il numero di espressioni che hanno potuto essere verificate come equivalenti alla corrispondente espressione più semplice usando Z3 dopo la semplificazione (a meno che il risultato della semplificazione abbia già esattamente la stessa rappresentazione testuale),
• il numero di espressioni che vengono semplificate fino alla stessa identica espressione della corrispondente espressione semplice, e
• il tempo medio di esecuzione in secondi.

Si noti che una verifica opzionale di una corretta semplificazione tramite Z3 contribuisce al tempo di esecuzione, mentre ciò non vale per il confronto dei risultati di semplificazione delle coppie costituite da un'espressione complessa e una più semplice.

Per impostazione predefinita i risultati della semplificazione non vengono stampati, ma vengono presentate solo queste statistiche. Se si desiderano informazioni sui primi, è possibile usare l'opzione -v:

python3 src/simplify_dataset.py -f some_file.txt -v

Verrà quindi mostrato il seguente output:

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

Un'altra opzione, -e, offre la possibilità di codificare gli output di tutte le espressioni tramite funzioni affini $f(x) = ax+b$ con interi casuali $a,b$ compresi tra $1$ e $2^b-1$ se $b$ è il numero di bit:

python3 src/simplify_dataset.py -f some_file.txt -v -e

Naturalmente la stessa funzione viene applicata a una coppia di espressioni nella stessa riga. Questo produrrebbe un output simile al seguente:

Simplify expressions from data/some_file.txt ...