💻 computer science

SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

SEAL è un analizzatore statico prototipale e modulare per la verifica di programmi con strutture dati collegate illimitate che sfrutta la logica di separazione e il solver SMT-based Astral per ottenere risultati competitivi nella categoria LinkedLists, offrendo al contempo una significativa estensibilità per lo sviluppo futuro.

Autori originali: Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Pubblicato 2026-02-09

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di dover verificare che una città complessa e in continuo mutamento di strade e palazzi sia sicura da percorrere. Devi assicurarti che nessuno cada da un ponte (un "NULL-pointer dereference"), che nessuno provi a demolire un edificio che è già stato rimosso (un errore "use-after-free") e che nessuno abbatta accidentalmente lo stesso edificio due volte (un errore "double-free").

Questo è esattamente ciò che fa SEAL, ma invece di una città, analizza programmi informatici che gestiscono liste di dati complesse e variabili (come le liste collegate).

Ecco come il documento spiega SEAL, suddiviso in concetti semplici:

1. L'idea centrale: Un detective specializzato

La maggior parte degli strumenti che controllano questi programmi sono come detective che utilizzano un libro di regole specifico e rigido per ogni tipo di crimine. SEAL è diverso. Utilizza un "motore logico" general-purpose chiamato ASTRAL.

Pensa ad ASTRAL come a un super-intelligente traduttore. Quando SEAL vede un puzzle complesso su come i dati sono connessi in memoria, traduce quel puzzle in un linguaggio che un risolutore (solver) SMT standard e potente comprende perfettamente. Questo rende SEAL molto flessibile. È come avere un detective che può cambiare lingua per parlare con qualsiasi esperto, invece di essere limitato a parlare un solo dialetto.

2. La sfida: Infinito vs Finito

I programmi che SEAL controlla spesso coinvolgono liste collegate (linked lists) — catene di dati in cui un elemento punta al successivo.

Il Problema: Alcune liste sono brevi e fisse (come una catena di 3 anelli). Altre sono illimitate (unbounded), il che significa che potrebbero avere 10 anelli, o 10.000, o essere infinite.
La Difficoltà: Cercare di controllare ogni singola possibile lunghezza di una catena infinita è impossibile per un computer. Ci vorrebbe un tempo infinito.
Il Trucco di SEAL: SEAL utilizza una tecnica di astrazione. Immagina di guardare un treno molto lungo. Inveve di contare ogni singolo vagone, SEAL dice: "Ok, questo è un 'treno lungo'". Sostituisce i dettagli disordinati del mezzo della catena con un'unica etichetta pulita (un "predicato"). Questo gli permette di ragionare sull'intera catena senza perdersi nei dettagli.

3. Come funziona: L'analizzatore di "forma"

SEAL è un "analizzatore di forma" (shape analyzer). Non guarda solo i numeri; guarda la forma della memoria.

Heap Simbolici: Crea una mappa della memoria utilizzando "heap simbolici". Pensa a questo come a una planimetria che dice: "Qui c'è un blocco di memoria, e si connette a questo altro blocco".
Il Punto Fisso del Ciclo (Loop Fixpoint): Quando un programma viene eseguito in un ciclo (ripetendo la stessa azione), SEAL controlla se la "forma" della memoria si è stabilizzata. Se la forma nel round attuale appare "abbastanza sicura" rispetto al round precedente, smette di controllare e dichiara il ciclo sicuro.

4. Punti di forza e debolezza attuali

Il documento ammette che SEAL è ancora un prototipo (una versione iniziale), ma ha delle statistiche impressionanti:

Le Buone Notizie (Punti di forza):

Il "Club degli Illimitati": In una competizione recente, c'erano 20 strumenti che cercavano di verificare programmi con liste infinite. Solo quattro strumenti sono riusciti nell'intento. SEAL era uno di questi.
Potenziale Futuro: Poiché SEAL utilizza quel "traduttore" flessibile (ASTRAL), è più facile insegnargli nuove forme. Gli autori credono che potranno eventualmente insegnargli a gestire strutture complesse come gli alberi o le skip-list (che sono come autostrade multilivello per i dati) che altri strumenti faticano a gestire.

Le Cattive Notizie (Debolezze):

Vocabolario Limitato: Attualmente, SEAL comprende solo un piccolo sottoinsieme del linguaggio C. Non può ancora gestire calcoli matematici complessi con i numeri o molti tipi di puntatori.
Gioco di Indovini: A volte, SEAL deve indovinare che tipo di struttura dati sta costruendo un pezzo di codice. Se indovina male (ad esempio, pensando che una struttura complessa sia solo una semplice lista), potrebbe perdere un bug o dare una risposta del tipo "non lo so".
Falsi Positivi: Poiché utilizza astrazioni (semplificando i dettagli), potrebbe talvolta pensare che un programma sia insicuro quando in realtà è corretto. Il documento nota che potrebbero risolvere questo problema rieseguendo il controllo senza semplificazione, ma questo richiede più tempo.

5. In sintamente

SEAL è un nuovo strumento modulare progettato per dimostrare che i programmi che gestiscono catene di dati complesse e infinite sono sicuri. Sebbene non sia ancora perfetto e non comprenda ogni caratteristica del linguaggio C, il suo design unico — l'uso di un traduttore generale per risolvere enigmi logici — lo rende uno dei pochi strumenti capaci di gestire i tipi più difficili di problemi di sicurezza della memoria. Gli autori sperano che, mantenendo il sistema flessibile, possano renderlo ancora migliore nelle competizioni future.

Riepilogo Tecnico: SEAL – Esecuzione Simbolica con Logica di Separazione

Definizione del Problema

La verifica di programmi che manipolano strutture dati collegate non limitate rimane una sfida significativa nell'analisi statica. Sebbene molti strumenti si affidino al model checking limitato o a euristiche specializzate, questi approcci spesso faticano con la complessità del ragionamento su lunghezze arbitrarie di liste e forme di memoria complesse. Inoltre, gli esistenti analizzatori basati sulla logica di separazione (SL) spesso accoppiano l'analisi con solver dedicati e non modulari, limitandone l'estensibilità e la capacità di integrare altre teorie logiche.

Metodologia

SEAL è un analizzatore statico progettato per la verifica di programmi che manipolano strutture dati collegate non limitate. Utilizza l'interpretazione astratta forward su formule di logica di separazione (SL). La metodologia centrale si distingue attraverso un'architettura modulare che scinde nettamente il motore di analisi dal motore di ragionamento logico.

Componenti Core

Dominio Astratto (Heap Simbolici):
- SEAL rappresenta gli stati di memoria astratti come heap simbolici, che sono formule SL della forma $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$ .
- Le formule atomiche ( $\phi_i$ $ϕ_{i}$ ) includono:
  - Formule pure: Descrivono disuguaglianze di puntatori o vincoli su valori non-puntatore.
  - Atomi points-to: Descrivono singole celle di heap.
  - Predicati induttivi: Descrivono sequenze non limitate di puntatori (es. liste).
  - Memoria libera: Un predicato speciale che rappresenta esplicitamente la memoria liberata che rimane raggiungibile.
- Il dominio traccia valori interi precisi entro un intervallo configurabile (default $[-5, 5]$ ). Gli stati nelle posizioni del programma sono rappresentati come disgiunzioni (insiemi) di heap simbolici.
Astrazione e Widening:
- Per gestire i cicli e gli spazi di stato infiniti, SEAL esegue il widening generalizzando le forme di memoria. Ciò comporta la ricerca di predicati spaziali compatibili (points-to o predicati di lista) e la loro unione in un singolo predicato di lista, a condizione che la posizione di collegamento non sia target di puntatori esterni o variabili del programma.
- Il sistema traccia le lunghezze minime delle liste fino a un limite fisso per garantire le garanzie di aciclicità durante l'astrazione.
- Indovinare i Predicati (Predicate Guessing): Attualmente, SEAL ipotizza il predicato induttivo atteso per le strutture C prima dell'analisi basandosi sul numero di campi (es. un campo auto-referenziale $\to$ SLL; due $\to$ DLL). Questa euristica può portare a una classificazione errata (es. una struttura intesa come lista annidata classificata come lista doppiamente concatenata).
Il Solver ASTRAL:
- A differenza della maggior parte degli strumenti SL che utilizzano euristiche dedicate per la soddisfacibilità e l'entailment, SEAL si affida a ASTRAL, un solver di logica di separazione general-purpose.
- ASTRAL traduce le formule SL in teorie SMT (specificamente bitvector e array) utilizzando un limite sull'unrolling dei predicati.
- Le formule tradotte vengono passate al solver SMT BITWUZLA.
- ASTRAL supporta predicati induttivi definiti dall'utente, permettendo a SEAL di definire i propri predicati senza supporto integrato del solver per essi.
Meccanica dell'Analisi:
- Fixpoint dei Cicli: Un fixpoint viene raggiunto quando l'entailment tra lo stato dell'iterazione corrente del ciclo ( $S$ ) e lo stato dell'iterazione precedente ( $T$ ) è valido. Questo è approssimato verificando se per ogni heap in $S$ , esiste un heap in $T$ che lo implica (entails).
- Analisi Interprocedurale: Le chiamate a funzione sono ottimizzate tramite riassunti (coppie precondizione/postcondizione).
- Semplificazione: Il sistema applica semplificazioni sintattiche, come la riduzione delle classi di equivalenza e la rimozione di variabili fuori ambito.

Contributi Chiave

Architettura Modulare: Separando il motore di interpretazione astratta dal motore di ragionamento logico tramite ASTRAL, SEAL ottiene un design destinato a essere più facile da estendere e combinare con il ragionamento in altre teorie.
Solving General-Purpose: L'integrazione di ASTRAL consente a SEAL di sfruttare i solver SMT per l'entailment e la soddisfacibilità della SL, evitando la necessità di solver personalizzati e dedicati per ogni specifica variante di logica.
Verifica di Liste Non Limitate: Lo strumento è in grado di verificare programmi con liste collegate non limitate, una categoria in cui molti strumenti concorrenti falliscono.

Risultati Sperimentali

SEAL ha partecipato alla categoria MemSafety-LinkedLists della competizione SV-COMP.

Performance Complessiva: Sul set completo di 134 programmi, SEAL ne ha verificati 55 come "True" (corretti) e ha trovato 4 "False" (bug), con 75 che non hanno riportato alcun risultato.
Sottoinsieme Liste Non Limitate: Sul sottoinsieme di 69 programmi che richiedono il ragionamento su strutture dati non limitate, SEAL ha verificato 14 programmi come corretti e ha trovato 2 bug.
Confronto:
- SEAL ha superato 2LS (che ha verificato solo 3 programmi non limitati).
- SEAL ha verificato meno programmi rispetto a PREDATORHP (46) e CPACHECKER (40), entrambi basati su grafi di memoria simbolica (SMG).
- SEAL è stato uno dei soli quattro analizzatori capaci di verificare programmi con liste non limitate in questa categoria.

Significato e Rivendicazioni

Il paper posiziona SEAL come un prototipo promettente con un focus specifico sull'estensibilità piuttosto che sul dominio immediato delle prestazioni grezze.

Potenziale Futuro: Gli autori affermano che il design modulare di SEAL e la sua dipendenza da ASTRAL forniscono una base solida per supportare strutture dati complesse che non possono essere facilmente rappresentate da SMG, come skip-list e alberi.
Limitazioni: Come prototipo iniziale, SEAL supporta attualmente solo un sottoinsieme di C (aritmetica dei puntatori limitata, tracciamento specifico degli interi) e si affida all'ipotesi euristica dei predicati, il che può portare a falsi positivi o all'incapacità di segnalare violazioni quando mancano informazioni sugli interi.
Roadmap: Gli autori intendono migliorare la selezione dei predicati durante l'analisi, sintetizzare predicati induttivi da esempi e potenzialmente integrare SEAL come dominio astratto all'interno del framework Frama-C EVA per gestire valori non-puntatore più complessi.

In sintesi, SEAL dimostra che un approccio general-purpose basato su SMT per il solving della logica di separazione è un'alternativa valida ed estensibile alle euristiche specializzate, offrendo una via per verificare strutture dati complesse e non limitate in futuro.