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

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

Riproducibilità

Per riprodurre parte degli esperimenti descritti nell'articolo, si può usare uno qualsiasi dei file di dataset contenuti nella directory data/. Per ciascuna delle seguenti funzioni $e_1,\ldots, e_5$, sono forniti dataset di $1,000$ MBA lineari equivalenti che usano $2$, $3$ o $4$ variabili:

$e_1(x,y) = x+y$
$e_2 = 49,374$
$e_3(x) = 3,735,936,685, x + 49,374$
$e_4(x,y) = 3,735,936,685, (x\mathbin{^\wedge}y) + 49,374$
$e_5(x) = 3,735,936,685\cdot \mathord{\sim} x$

Per $e_1$, sono forniti dataset aggiuntivi per $5$ fino a $7$ variabili. Queste MBA sono state generate usando un algoritmo basato sul metodo descritto da Zhou et al. nel 2007 e descritto nell'articolo.

Si noti che questi dataset sono stati generati per $b=64$ bit. Per diversi numeri di bit, la loro equivalenza alle $e_i$ non può essere garantita.

Per la riproduzione di ulteriori esperimenti, si rimanda ai dataset forniti dal repository MBA-Solver e dal repository NeuReduce, rispettivamente.

Verifica della linearità

Il file check_linear_mba.py è usato dal semplificatore, ma fornisce anche una propria interfaccia, ad esempio:

python3 src/check_linear_mba.py "x+x" "x*x"

Controlla tutte le espressioni passate tramite gli argomenti della riga di comando. In questo caso produrrebbe il seguente output:

*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid

Formato delle MBA

Il numero di variabili è teoricamente illimitato, ma ovviamente il tempo di esecuzione aumenta con il numero di variabili. Non ci sono restrizioni severe sulla notazione delle variabili. Devono iniziare con una lettera e possono contenere lettere, numeri e underscore. Ad esempio, tutti i seguenti nomi di variabili sarebbero validi:

$a$, $b$, $c$, ..., $x$, $y$, $z$, ...
$v0$, $v1$, $v2$, ...
$v_0$, $v_1$, $v_2$, ...
$X0$, $X1$, $X2$, ...
$var0$, $var1$, $var2$, ...
$var1a$, $var1b$, $var1c$, ...
...

Sono supportati i seguenti operatori, ordinati in base alla loro precedenza in Python:

$\mathord{\sim}$, $-$: negazione bit a bit e meno unario
$*$: prodotto
$+$, $-$: somma e differenza
&: congiunzione
$\mathbin{^\wedge}$: disgiunzione esclusiva
$|$: disgiunzione inclusiva

Gli spazi bianchi possono essere usati nelle espressioni di input. Ad esempio, l'espressione "x+y" può essere scritta anche come "x + y".

Si prega di rispettare la precedenza degli operatori e di usare le parentesi se necessario! Ad esempio, le espressioni $1 + (x|y)$ e $1 + x|y$ non sono equivalenti poiché $+$ ha precedenza maggiore di $|$. Notare che quest'ultima non è nemmeno una MBA lineare.

Dipendenze

Il risolutore SMT Z3 è richiesto

da simplify_dataset.py, dove le espressioni semplificate vengono verificate come equivalenti alle corrispondenti espressioni semplici, e
da simplify.py se viene usata la verifica opzionale delle espressioni semplificate. Se questa opzione non viene usata, non viene generato alcun errore anche se Z3 non è installato.

Installazione di Z3:

dal repository Github: https://github.com/Z3Prover/z3, oppure
su Debian: sudo apt-get install python3-z3

Licenza

Contatti

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

SiMBA

Più Popolari

SiMBA

Contenuto

Uso

Semplificazione di singole espressioni

Semplificazione e verifica di espressioni da un file

Riproducibilità

Verifica della linearità

Formato delle MBA

Dipendenze

Licenza

Contatti