Sintesi Tecnica: Logica della Sufficienza dell'Incorrettezza (SIL) e Separation SIL

1. Definizione del Problema

I metodi formali per la verifica dei programmi si sono storicamente basati su tecniche di sovra-approssimazione (ad es., Logica di Hoare, Interpretazione Astratta) per garantire l'assenza di errori. Sebbene sound (corretti), questi metodi producono inevitabilmente falsi allarmi (errori spurii), il che può ostacolare l'adozione da parte dei programmatori. Al contrario, i metodi di sotto-approssimazione (ad es., Logica dell'Incorrettezza, Bounded Model Checking) sono progettati per il rilevamento di bug e sono privi di falsi allarmi, poiché riportano solo stati di errore raggiungibili. Tuttavia, le esistenti logiche di sotto-approssimazione, come la Logica dell'Incorrettezza (IL), si concentrano principalmente sul dimostrare l'esistenza di un errore raggiungibile da una precondizione. Esse non caratterizzano necessariamente l'insieme degli stati iniziali che portano a tali errori.

Il documento identifica una lacuna nel ragionamento sulle fonti dell'incorrettezza. I programmatori hanno bisogno di sapere non solo che un bug esiste, ma specificamente quali stati di input lo causano, per poter delimitare efficacemente il debugging e il testing. Sebbene le "triple di Lisbona" (sotto-approssimazioni backward) siano state precedentemente discusse nel contesto della Outcome Logic (OL), mancava un sistema di prova dedicato, minimale e completo specificamente per inferire le precondizioni sufficienti per gli errori.

2. Metodologia

Gli autori introducono la Sufficient Incorrectness Logic (SIL), una nuova logica di programmi basata su triple, progettata per la sotto-approssimazione backward.

2.1 Concetto Centrale: Triple SIL

Una tripla SIL è denotata come $\langle\langle P \rangle\rangle r \langle\langle Q \rangle\rangle$.

• Semantica: La tripla è valida se e solo se la semantica di raccolta backward del programma $r$ applicata all'insieme degli stati di errore $Q$ contiene l'insieme degli stati iniziali $P$. Formalmente: $J \leftarrow r K (Q) \supseteq P$.
• Interpretazione: "Tutti gli stati di input che soddisfano $P$ hanno almeno un'esecuzione di $r$ che conduce a uno stato che soddisfa $Q$."
• Distinzione da IL: Mentre la IL ($[P] r [Q]$) garantisce che alcuno stato in $Q$ sia raggiungibile da alcuno stato in $P$, la SIL garantisce che ogni stato in $P$ possa raggiungere un errore in $Q$. Ciò rende $P$ una condizione sufficiente per l'incorrettezza.

2.2 Sistema di Prova

Il documento definisce un insieme minimale di regole di prova per la SIL (Figura 7) che sono sia sound che complete per comandi regolari (inclusi non-determinismo e cicli).

• Semantica Backward: Le regole sono derivate dalla semantica backward dei comandi (ad es., l'assegnazione utilizza la sostituzione backward).
• Regola di Conseguenza: La regola $\langle\langle \text{cons} \rangle\rangle$ permette di rafforzare la precondizione e indebolire la postcondizione, facilitando la sotto-approssimazione.
• Gestione dei Cicli: La logica include regole per l'iterazione ($\langle\langle \text{iter} \rangle\rangle$) e regole aggiuntive come $\langle\langle \text{iter0} \rangle\rangle$ (saltare il ciclo) e $\langle\langle \text{unroll} \rangle\rangle$ (unroll una volta) per supportare l'analisi pratica senza richiedere invarianti di ciclo per la terminazione.
• Disgiunzione: A differenza della Logica di Hoare, la SIL permette di scartare i disgiunti nelle precondizioni (tramite $\langle\langle \text{choice} \rangle\rangle$ e $\langle\langle \text{disj} \rangle\rangle$), il che è cruciale per la scalabilità nella sotto-approssimazione.

2.3 Separation SIL

Per gestire i puntatori e l'allocazione dinamica della memoria, gli autori istanziano la SIL con formule di Separation Logic, creando la Separation SIL.

• Linguaggio di Asserzione: Combina la standard Separation Logic (separazione dell'heap, points-to) con l'asserzione $x \not\mapsto$ (che indica un puntatore deallocato), adattata da Incorrectness Separation Logic (ISL).
• Regole: Include regole backward per le operazioni sull'heap (alloc, free, load, store) e una regola di frame ($\langle\langle \text{frame} \rangle\rangle$) per consentire il ragionamento locale sugli errori di memoria.
• Completezza: Il sistema è dimostrato essere sound. Per i programmi privi di cicli, viene dimostrato essere relativamente completo (assumendo un oracle per l'implicazione tra asserzioni).

3. Contributi Chiave

1. Introduzione di SIL: Una nuova logica per triple di sufficiente incorrettezza che identifica le fonti degli errori (stati iniziali) piuttosto che la sola esistenza dei bug.
2. Tassonomia Formale: Il documento costruisce una tassonomia di logiche basate su triple (Figura 3) basata su due assi:
   • Direzione Semantica: Forward (Logica di Hoare, IL) vs. Backward (SIL, Condizioni Necessarie).
   • Tipo di Approssimazione: Sovra-approssimazione (Logica di Hoare, Condizioni Necessarie) vs. Sotto-approssimazione (IL, SIL).
   • Questa tassonomia chiarisce che la SIL è l'unica combinazione di semantica backward e sotto-approssimazione.
3. Analisi Comparativa:
   • SIL vs. IL: La IL trova che un errore è raggiungibile; la SIL trova quali input lo causano. Non sono logicamente equivalenti.
   • SIL vs. Logica di Hoare (HL): Per programmi deterministici e terminanti, la SIL e la HL coincidono (interpretando la postcondizione come stati di errore). Per programmi non deterministici, divergono.
   • SIL vs. Condizioni Necessarie (NC): Gli autori dimostrano che la NC è isomorfa alla HL (tramite doppia negazione) ma non è comparabile con la IL o la SIL nel caso generale.
   • SIL vs. Outcome Logic (OL): Sebbene la OL possa esprimere triple SIL (specificamente il pattern "Lisbon"), gli autori sostengono che il sistema di prova della SIL sia più diretto e naturale per inferire le precondizioni da specifiche di errore, specialmente riguardo alla gestione delle disgiunzioni e al ragionamento backward.
4. Separation SIL: È un'istanza sound e relativamente completa per gli errori di memoria, dimostrando che la sotto-approssimazione backward può produrre postcondizioni più succinte e garanzie più forti rispetto alla ISL in casi specifici (ad es., fornendo testimoni reali per il testing).

4. Risultati

• Correttezza e Completezza: L'insieme minimale di regole SIL è dimostrato essere sound e completo per comandi regolari.
• Completezza Relativa: La Separation SIL è dimostrata essere relativamente completa per programmi privi di cicli.
• Rilevanza Industriale: Il documento sostiene che la SIL fornisce una giustificazione formale a posteriori per le strategie di analisi backward utilizzate dagli strumenti industriali in Meta (Zoncolan, Mariana Trench, Pysa), che inferiscono precondizioni di sufficiente incorrettezza per rilevare bug di sicurezza.
• Esempi di Derivazione: Il documento fornisce derivazioni dettagliate (ad es., per un programma client che coinvolge free e alloc) mostrando come la Separation SIL possa derivare precondizioni che garantiscono che un errore avvenga, offrendo un percorso più diretto al debugging rispetto alle logiche orientate al forward.

5. Significato e Rivendicazioni

Il documento sostiene che la SIL colma un vuoto teorico critico fornendo un framework di sotto-approssimazione orientato al backward. Il suo significato risiede in:

• Precisione per il Debugging: Identificando l'esatto insieme di stati di input che portano agli errori, la SIL supporta il "ragionamento backward" che è più naturale per i developer che cercano di capire perché un bug avviene, rispetto alle sotto-approssimazioni forward che mostrano solo che un bug è raggiungibile.
• Unificazione Teorica: Chiarisce il panorama delle logiche di programma, mostrando che mentre esiste una dualità tra la Logica di Hoare e le Condizioni Necessarie, non esiste una tale dualità semplice tra la Logica dell'Incorrettezza e la Logica della Sufficienza dell'Incorrettezza.
• Utilità Pratica: Gli autori sostengono che la Separation SIL può produrre postcondizioni più succinte e garanzie più forti rispetto alla Incorrectness Separation Logic (ISL) per il testing e il debugging, poiché assicura che ogni stato nella precondizione conduca all'errore, fornendo testimoni concreti.

Il documento conclude che non esiste una logica "migliore" in assoluto; piuttosto, ciascuna (HL, IL, NC, SIL) serve a uno scopo specifico. La SIL è posizionata specificamente come lo strumento d'elezione quando l'obiettivo è localizzare le fonti dell'incorrettezza per guidare gli sforzi di debugging e testing.