CHC-based Automated Verification of WebAssembly Programs

Sintesi Tecnica: Verifica Automatica di Programmi WebAssembly basata su CHC

Problematica
WebAssembly (Wasm) è un linguaggio imperativo basato su stack sempre più utilizzato come target per i linguaggi di programmazione di sistema. Con la crescita della sua adozione, la verifica della sicurezza dei programmi WebAssembly — specificamente la dimostrazione che gli stati di errore (modellati come istruzioni irraggiungibili o unreachable) siano irraggiungibili durante l'esecuzione — è diventata critica. Tuttavia, gli approcci di verifica esistenti affrontano sfide significative quando applicati a WebAssembly:

1. Chiamate a Funzioni Indirette: WebAssembly utilizza tabelle di riferimenti a funzioni per le chiamate indirette (call_indirect). Un approccio di verifica ingenuo che modella queste tabelle come array di punti di ingresso delle funzioni genera un'analisi dei casi eccessiva, producendo troppi candidati per le chiamate indirette e sovraccaricando i solver.
2. Codice Ausiliario (Panic Handler): I programmi compilati da linguaggi di alto livello (ad es. Rust) contengono spesso grandi e complessi gestori di panico (panic handlers) invocati in caso di errori. Questi gestori consistono spesso in blocchi diagnostici complessi e voluminosi, irrilevanti per la proprietà di sicurezza principale (raggiungibilità delle istruzioni unreachable). La traduzione diretta di questi massicci blocchi in clausole di Horn vincolate (CHC) crea formule inutilmente grandi e complesse che ostacolano la verifica.
3. Semantica di Basso Livello: A differenza del bytecode Java, WebAssembly si affida pesantemente a operazioni bitwise e semantica di vettori di bit, richiedendo una modellazione precisa piuttosto che approssimazioni con interi illimitati.

Metodologia
Gli autori propongono un metodo di verifica statica automatizzata che traduce i programmi WebAssembly in clausole di Horn vincolate (CHC), riducendo il problema della verifica della sicurezza alla soddisfacibilità delle CHC. L'approccio utilizza solver CHC esistenti (ad es. Z3 Spacer, Eldarica) per provare automaticamente la sicurezza.

• Linguaggio Target: Il metodo si rivolge a un sottoinsieme idealizzato di WebAssembly, che include interi a 32 bit, controllo del flusso strutturato, variabili locali/globali, tabelle, memorie e chiamate a funzioni dirette e indirette. Il linguaggio assume programmi validi dove la forma dello stack e i tipi sono determinati staticamente.
• Generazione delle CHC:
  • Codifica dello Stato: Ogni istruzione etichettata è associata a un predicato che riassume le esecuzioni da quel punto. Lo stato include lo stack degli operandi, lo store locale, le globali, le tabelle e le memorie. Per aiutare le prestazioni del solver, lo stack degli operandi e le variabili locali sono codificati come argomenti di vettori di bit piatti (sfruttando la determinazione statica dell'altezza dello stack), mentre tabelle e memorie sono modellati come Array.
  • Monitoraggio della Sicurezza: Un flag booleano (vsafe) traccia la sicurezza dell'esecuzione. Viene impostato a 0 se viene raggiunta un'istruzione unreachable o se una call_indirect causa un trap di discrepanza di tipo (type-mismatch trap).
  • Traduzione delle Istruzioni: Sono definite regole per generare CHC per ogni tipo di istruzione. Per call_indirect, il metodo genera clausole per tutte le possibili funzioni target il cui tipo corrisponde alla firma attesa nel sito di chiamata, controllando al contempo l'accesso a tabelle non valide.

Contributi Chiave e Ottimizzazioni
Per affrontare le specifiche sfide di WebAssembly, il documento introduce due ottimizzazioni primarie:

1. Ottimizzazione per Chiamate a Funzioni Indirette:

   • Filtraggio Basato sul Tipo: Invece di considerare tutte le funzioni in un modulo, il metodo utilizza il tipo di funzione atteso nel sito di chiamata per filtrare l'insieme dei possibili chiamanti in un insieme finito $F(tf)$.
   • Ottimizzazione Tabella in Sola Lettura: Se una tabella di riferimenti a funzioni è in sola lettura, il metodo calcola staticamente gli indici in cui sono memorizzati specifici riferimenti a funzioni. Ciò consente all'istruzione call_indirect di essere espansa in una distinzione di casi basata sull'indice letto dalla tabella, eliminando le operazioni di lettura dell'array dalle CHC generate.
   • Ottimizzazione Indice Costante: Se gli accessi alla tabella utilizzano indici costanti (anche se la tabella è mutabile), il metodo sostituisce le letture della tabella con nuove variabili globali, riducendo la complessità dell'array.
   • Risoluzione Statica: Se una tabella è sia in sola lettura che accessibile tramite indici costanti, la chiamata indiretta viene risolta staticamente e sostituita con una chiamata diretta.

2. Ottimizzazione per i Panic Handler:

   • Sintesi del Controllo del Flusso: Il metodo identifica i gestori di panico (funzioni che terminano in unreachable) e semplifica le sequenze di istruzioni immediatamente precedenti l'istruzione unreachable.
   • Regola di Riscrittura: Un'analisi conservativa del controllo del flusso applica la regola $e; \text{unreachable} \to \text{unreachable}$, a condizione che $e$ non possa trasferire il controllo al di fuori della continuazione corrente per saltare l'istruzione unreachable. Ciò elimina i calcoli diagnostici (ad es. costruzione di messaggi di errore) che non influenzano il raggiungimento dello stato di errore: questa trasformazione è corretta per la verifica della sicurezza: se il programma ottimizzato è sicuro, anche l'originale è sicuro, sebbene possa introdurre falsi allarmi se il codice eliminato conteneva uscite non locali (cosa che l'analisi assume conservativamente non esista).

Risultati Sperimentali
Gli autori hanno implementato il metodo in uno strumento prototipo, WASMVERIFIER, e lo hanno valutato su un set di benchmark composto da:

• 13 programmi WebAssembly originali.
• 3 programmi Rust compilati in WebAssembly.
• 74 programmi C da SV-COMP 2026 (categorie bitvector, loop e ricorsione).

Utilizzando Z3 Spacer ed Eldarica con un timeout di 300 secondi:

• Z3 Spacer: Ha verificato con successo o smentito la sicurezza per 56 dei 90 programmi. È andato in timeout su 22 e ha riportato falsi allarmi su 12.
• Eldarica: Ha avuto successo su 54 programmi, è andato in timeout su 21, ha riportato falsi allarmi su 11 e ha fallito a causa dell'esaurimento delle risorse (memoria o stack) in 4 casi.

I falsi allarmi sono stati attribuiti principalmente alla gestione conservativa del tool per le istruzioni non supportate (sostituendole con unreachable), il che ha ridotto la precisione.

Significatività e Rivendicazioni
Il documento sostiene che la verifica basata su CHC è un approccio promettente per la verifica completamente automatizzata dei programmi WebAssembly. La significatività risiede in:

• Automazione: A differenza degli approcci basati sulla logica (ad es. Iris-Wasm) che richiedono la costruzione manuale di prove, questo metodo è completamente automatizzato e non richiede annotazioni.
• Gestione delle Caratteristiche Specifiche di Wasm: Affronta efficacemente le sfide uniche di WebAssembly, in particolare le chiamate indirette tramite tabelle di funzioni e la presenza di codice ausiliario voluminoso, che gli strumenti di verifica basati su stack precedenti (come JayHorn per Java) non gestivano con precisione.
• Scalabilità: Attraverso le ottimizzazioni proposte, il metodo riduce la dimensione e la complessità delle CHC generate, rendendole più adatte ai solver esistenti.

Gli autori notano con modestia che, sebbene la riduzione da WebAssembly a CHC sia congetturata essere corretta e completa, una prova formale rimane un lavoro futuro. Riconoscono anche i limiti riguardanti la risoluzione dei vincoli dei vettori di bit e la gestione delle istruzioni non supportate, suggerendoli come direzioni per futuri miglioramenti.