L'**esecuzione simbolica** è una tecnica di analisi che utilizza variabili simboliche anziché valori concreti per rappresentare gli input di un programma. Questo permette di esplorare sistematicamente i diversi percorsi di esecuzione (**path**) per identificare bug o vulnerabilità senza testare manualmente ogni caso.

## 1. Obiettivi e Funzionamento
L'obiettivo è verificare il comportamento del software su un insieme potenzialmente infinito di input.
*   **Esempio:** Lo strumento **SAGE** di Microsoft genera sequenze di input che dimostrano vulnerabilità reali.
*   **Problemi rilevabili:** Crash, dereferenziazione di puntatori null, errori di indice (out-of-bounds), **double free**, variabili non inizializzate, overflow (heap/stack).

### Esempio logico
Data una funzione `foo(x, y)`:
1.  Inizializza `t = 0`.
2.  Se `x > y` allora `t = x`, altrimenti `t = y`.
3.  Se `t < x` esegui blocco `[A]`.

L'esecuzione simbolica analizza se esiste un input simbolico tale per cui il blocco `[A]` sia raggiungibile. In questo caso, analizzando i vincoli:
*   Percorso 1: `x > y` AND `x < x` (Impossibile).
*   Percorso 2: `x <= y` AND `y < x` (Contraddizione, dato che `x <= y` e `y < x` non possono essere entrambi veri).
*   **Risultato:** Il blocco `[A]` è irraggiungibile.

## 2. Confronto: Dinamico vs Simbolico
*   **Approccio Dinamico (Fuzzing):** Analizza risultati su input concreti. È utile per trovare bug ma non garantisce l'assenza di vulnerabilità (non è esaustivo).
*   **Analisi Statica (Simbolica):** Considera tutti i possibili input. Può individuare bug e, in certi casi, **dimostrare l'assenza** di determinate classi di errori.

## 3. SMT Solvers
Per risolvere meccanicamente i vincoli logici si utilizzano gli **SMT (Satisfiability Modulo Theories) solvers**.
*   **Input:** Una teoria o formula logica.
*   **Output:** Soluzione trovata, "Insolvibile" o "I don't know" (poiché molti problemi SMT sono NP-completi).
*   **Domini:** Numeri reali, interi, liste, formule non interpretate.

### Funzionamento dei SAT/SMT Solvers
Gli SMT sono costruiti sopra i risolutori **SAT** (che lavorano su variabili booleane):
1.  La formula viene convertita in **CNF** (congiunzione di clausole).
2.  Il risolutore SAT assegna valori di verità alle variabili.
3.  L'SMT verifica se tale assegnamento soddisfa i vincoli specifici della teoria (es. disequazioni lineari).
4.  Se c'è una contraddizione, l'SMT aggiunge un nuovo vincolo al SAT per evitare quel percorso nelle iterazioni successive (**Conflict-Driven Clause Learning**).

## 4. Limitazioni
L'esecuzione simbolica deve affrontare l'**esplosione dei percorsi**: il numero di path possibili cresce in modo esponenziale rispetto alla complessità del codice.
*   **Strategie di mitigazione:**
    *   Controllare la **path condition** ad ogni passo per interrompere percorsi impossibili.
    *   Evitare di esplorare percorsi simili a quelli già esclusi.

## 5. Conclusioni
L'analisi simbolica è uno strumento potente per la sicurezza perché permette di esplorare rami di codice difficili da raggiungere con i test tradizionali, fornendo una copertura molto più profonda rispetto al semplice testing dinamico.