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