Requisiti di sistema

Su sistemi di tipo Debian, eseguire il seguente comando:

sudo apt install libgmp3-dev gcc-multilib gdb python3 python3-pip python3-venv openjdk-17-jdk libgmp-dev pkg-config opam

È inoltre necessario installare Ghidra e aggiungere la variabile d'ambiente GHIDRA con la directory di installazione di Ghidra

export GHIDRA=<ghidra-directory>

Installazione

Il modo più semplice per installare xyntia è creare uno switch opam. Questo installerà automaticamente xyntia e le sue dipendenze:

$ cd <xyntia-directory>
$ opam switch create . 4.14.1 -y # or any version >= 4.14.1
$ eval $(opam env)

Per sintetizzare una funzione da un file di campionamento, eseguire il seguente comando:

$ xyntia [-ops <grammar>] [-time <time>] [-heur <heur>] <file.json>

dove grammar è l'abbreviazione della grammatica usata per definire lo spazio di ricerca (vedi sotto), heur è l'abbreviazione dell'euristica di ricerca da utilizzare (vedi sotto), time è il budget di tempo della sintesi in secondi e file è il percorso del file di campionamento.

Il file di campionamento deve essere nel formato prodotto dal modulo di campionamento casuale di Syntia. Il file examples/samples/example.json è un esempio di file di campionamento.

Puoi lasciare che xyntia campioni l'output di un binario e lo sintetizzi con il seguente comando:

$ xyntia [-ops <grammar>] [-time <time>] [-heur <heur>] -bin <binary-file> -config <config-file> 

dove binary-file è il percorso del binario da analizzare e config-file è un file di scripting per indicare quale output campionare e come campionarlo.

Il linguaggio di scripting usato in config-file è un'estensione del linguaggio di scripting di Binsec. Aggiunge le seguenti nuove dichiarazioni e istruzioni:

• sample N [ reg_1, ..., reg_n ], che specifica di generare N campioni per ogni output. È possibile impostare una lista di output di registro target; in tal caso, solo questi vengono campionati, altrimenti vengono campionati tutti gli output rilevati;
• set domain VAR [MIN, MAX], che specifica il dominio di campionamento per l'input VAR. VAR può essere un registro o qualsiasi variabile DBA, ma non una cella di memoria. Per specificare il dominio di una cella di memoria, vedere questo esempio;
• prune constant outputs, che rimuove tutti gli output costanti (cioè senza variabili di input) dall'insieme degli output campionati;
• set optimal sampling per utilizzare la strategia di campionamento descritta nell'articolo su Xyntia.

Ad esempio, per sintetizzare l'output eax della funzione add, eseguire

Quando usare le regole di inferenza ?

In breve: se prevedi che la tua espressione target contenga valori costanti.

Risposta completa: La sintesi di programmi ha limitazioni fondamentali, in particolare la gestione di valori costanti arbitrari e di espressioni grandi. Per superare queste limitazioni, Xyntia include regole di inferenza per guidare meglio la ricerca e portare in un solo passaggio una soluzione candidata all'espressione target (possibilmente con valori costanti arbitrari). Quindi, se la tua espressione target contiene probabilmente valori costanti, usa le regole di inferenza.

Per capire meglio, leggi il nostro articolo [3]:

Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation, Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin, Jean-Yves Marion, ACM Conference on Computer and Communications Security 2025

Utilizzo

Per usare le regole di inferenza devi impostare l'opzione -infrules <val>, dove <val> può essere:

1. Un elenco di regole (r1, r2, ..., rk) in cui ogni regola mira a gestire un caso specifico come descritto di seguito

Per confrontare facilmente altri sintetizzatori con Xyntia o applicarli a compiti di deoffuscazione, forniamo un modo per estrarre il problema di sintesi nel formato SyGUS standard. Per farlo, basta usare l'opzione -sygus.

Ad esempio, per estrarre il problema sygus da un codice binario, eseguire:

$ xyntia -bin <binary-file> -config <config-file> -sygus

Tutti i dataset e gli script sono forniti per riprodurre gli esperimenti presentati in [1]. In particolare, contiene il dataset B1 dell'articolo su Syntia [2] (grazie a Tim Blazytko per averlo condiviso con noi), il nostro dataset B2 e i dataset usati per valutare la deoffuscazione anti-black-box.

Dipendenze Python

Per facilitare l'installazione, forniamo anche il file requirements.txt per installare facilmente le dipendenze Python.

Per creare e attivare un ambiente Python, eseguire i seguenti comandi (facoltativi):

$ python3 -m venv <name-virtualenv> # create a virtual environment for python3
$ source <name-virtualenv>/bin/activate # active the virtual environment

Quindi, installare le dipendenze:

$ pip install -r requirements.txt

Avviare gli esperimenti

I dataset usati in [1] si trovano nella directory ./datasets. Per eseguire Xyntia su un dataset (es. B2) con un timeout prefissato (es. 1s), eseguire i seguenti comandi:

$ python3 ./scripts/bench/bench.py --dataset datasets/b2 --out results --parallel -- xyntia -check -time 1

Le opzioni e i loro significati si trovano tramite l'opzione .

Forniamo anche ./scripts/utils/all_from_trace.sh, che traccia l'esecuzione del codice con Ghidra o GDB, estrae ogni blocco di codice eseguito, lo campiona e lo sintetizza. Il manuale è disponibile tramite ./scripts/utils/all_from_trace.sh --help e può essere eseguito come segue:

$ XYNTIA="xyntia <options>" # the xyntia command to use
$ ./scripts/utils/all_from_trace.sh --outdir <resdir> --all -- binary arg1 arg2 ...

Ecco un esempio:

$ cd examples/bin && make && cd -
$ ./scripts/utils/all_from_trace.sh --outdir <resdir> --all -- ./examples/bin/add