GAMBA

GAMBA è uno strumento per la semplificazione di espressioni booleano-aritmetiche miste (MBA). GAMBA è l'acronimo di General Advanced Mixed Boolean Arithmetic simplifier. Utilizza il semplificatore algebrico lineare SiMBA per semplificare iterativamente le sottoespressioni lineari di una MBA di input potenzialmente non lineare. Nel complesso, i suoi ingredienti principali sono i seguenti:

• Utilizzo di alberi sintattici astratti (AST)
• Isolamento delle sottoespressioni lineari tramite l'applicazione di trasformazioni (banali e più sofisticate)
• Refactoring per aumentare la probabilità di costruire sottoespressioni lineari semplificabili
• Semplificazione delle sottoespressioni lineari usando SiMBA
• Logica di sostituzione per eliminare temporaneamente costanti non banali e operazioni aritmetiche all'interno di operazioni bit a bit

GAMBA si basa sul seguente articolo; si vedano anche le diapositive usate per la presentazione:

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

Contenuto

Vengono forniti due programmi principali:

• simplify_general.py per la semplificazione di MBA generali
• simplify.py per la semplificazione di MBA lineari

Inoltre, viene fornito uno script di test per riprodurre i risultati descritti nell'articolo.

Utilizzo

Semplificazione di singole espressioni generali

Per semplificare una singola espressione expr, usare

python3 src/simplify_general.py "expr"

In alternativa, è possibile semplificare più espressioni contemporaneamente, ad esempio:

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

In effetti, ogni argomento della riga di comando che non è un'opzione viene considerato un'espressione da semplificare. Si noti che omettere le virgolette può portare a comportamenti indesiderati. I risultati della semplificazione vengono stampati sulla riga di comando come mostrato di seguito:

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

Se si usa l'opzione -z, i risultati della semplificazione vengono infine verificati per essere semanticamente equivalenti alle espressioni originali usando Z3. Ciò non incide sull'output della riga di comando finché l'algoritmo funziona correttamente:

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

Se l'algoritmo producesse un risultato errato, verrebbe attivato il seguente errore:

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

Inoltre, è possibile eseguire una validazione numerica dei risultati con tutti gli input possibili fino a un determinato numero di bit. Questa viene attivata con l'opzione -v, seguita dal numero massimo di bit degli input usati:

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

Anche in caso di risultato errato, l'output potrebbe apparire come segue:

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

Le costanti che compaiono nelle espressioni di output di GAMBA possono ovviamente dipendere dal numero di bit usati per le costanti e per le variabili. Questo numero è $64$ di default e può essere impostato usando l'opzione -b:

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

Di default, le costanti che compaiono nell'output vengono riportate nella rappresentazione più vicina possibile a zero. Cioè, nel caso precedente, il numero -1 rimarrebbe:

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

Questo comportamento può essere modificato: usando l'opzione -m, viene abilitata una riduzione modulo delle costanti:

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

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

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

Semplificazione di singole espressioni lineari

Il file src/simplify.py è pensato per essere utilizzato da src/simplify_general.py, ma può anche essere eseguito singolarmente. Usare l'opzione della riga di comando -h per vedere le impostazioni disponibili.

Riproduzione degli esperimenti

Il file experiments/tests.py può essere usato per riprodurre gli esperimenti descritti nell'articolo. Di default esegue GAMBA su 6 dataset:

python3 experiments/tests.py

In alternativa, si può indicare di eseguire SiMBA usando l'opzione --linear o -l. In tal caso, SiMBA viene eseguito solo su MBA con ground truth lineari:

python3 experiments/tests.py --linear

I controlli numerici o i controlli tramite Z3 possono essere attivati rispettivamente con le opzioni --check (-c) o --z3 (-z).

Le espressioni vengono categorizzate in base al successo della semplificazione o della verifica:

• ok: espressioni semplificate fino a ottenere esattamente lo stesso risultato delle corrispondenti ground truth
• okz: espressioni la cui equivalenza alle ground truth può essere verificata usando l'algoritmo (semplificando a 0 l'espressione meno l'espressione ground truth)
• z3: espressioni la cui equivalenza alle ground truth può essere verificata usando Z3
• to: espressioni per le quali l'algoritmo è andato in timeout
• ng: espressioni per le quali semplificazione e verifica non hanno avuto successo
• nc: espressioni per le quali l'algoritmo, nel caso venga usato SiMBA, non è stato eseguito poiché le ground truth non sono lineari
• err: espressioni per le quali si è verificato un errore

Dataset

I dataset da usare con experiments/tests.py si trovano nella directory experiments/datasets/.

• neureduce.txt: usare l'opzione -d 0; da https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv (con alcune correzioni applicate)
• mba_obf_linear.txt: usare l'opzione -d 1; da https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt (1000 espressioni lineari)
• mba_obf_nonlinear.txt: usare l'opzione -d 2; da 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 espressioni ciascuno; con alcune correzioni per le espressioni non polinomiali)
• syntia.txt: usare l'opzione -d 3; da MBA-Flatten, dataset/dataset_syntia.txt
• mba_flatten.txt: usare l'opzione -d 4; da MBA-Flatten, le prime 1000 espressioni da dataset/pldi_dataset_linear_MBA.txt, dataset/pldi_dataset_poly_MBA.txt, dataset/pldi_dataset_nonpoly_MBA.txt
• qsynth_ea.txt: usare l'opzione -d 5; da https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json

Inoltre, nella directory experiments/datasets/bonus/ sono forniti i seguenti dataset bonus (non trattati nella pubblicazione):

• loki_tiny.txt: usare l'opzione -d 6; da https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data, 25000 MBA generati dall'articolo LOKI per semplici espressioni ground truth ($x+y$, $x-y$, $x\&y$, $x|y$, $x^y$), fino a profondità 5

Formato delle MBA

Il numero di variabili è teoricamente illimitato, ma ovviamente il tempo di esecuzione aumenta con il numero di variabili. Non ci sono forti restrizioni sulla notazione delle variabili. Devono iniziare con una lettera e possono contenere lettere, numeri e underscore. Ad esempio, i seguenti nomi di variabile sarebbero tutti 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 per precedenza in Python:

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

Negli input si possono usare spazi bianchi. 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 $|$. Si noti che quest'ultima non è nemmeno una MBA lineare.

Dipendenze

Z3

L'SMT Solver Z3 è richiesto da simplify_general.py e 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
• su Debian: sudo apt-get install python3-z3

NumPy

Il pacchetto di calcolo scientifico NumPy è richiesto per pigrizia, ma non è realmente essenziale per il funzionamento. Nota: per numpy.quantile è richiesta almeno la versione 1.15.0

Installazione di NumPy:

• dal repository Github: https://github.com/numpy/numpy.git
• su Debian: sudo apt-get install python3-numpy

Licenza

Copyright (c) 2023 Denuvo GmbH, rilasciato sotto GPLv3.

Contatti

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