Riepilogo Tecnico: iSMC – Un Model Checker Simbolico basato su BDD con Certificazione Interattiva

1. Enunciato del Problema

Il model checking è una tecnica fondamentale per verificare la correttezza di sistemi hardware e software. Tuttavia, garantire l'affidabilità dello stesso model checker rappresenta una sfida critica. I paradigmi di certificazione tradizionali si basano su protocolli non interattivi: un prover (il model checker) genera un certificato (ad esempio, un'assegnazione soddisfacente o una prova di risoluzione), e un verifier lo verifica in modo indipendente.

Il documento identifica una limitazione teorica fondamentale in questo approccio: per molti problemi, incluso il model checking CTL generale, i certificati possono avere una lunghezza esponenziale nel caso peggiore rispetto alla dimensione dell'istanza. Di conseguenza, il verifier richiede tempo esponenziale per verificarli, rendendo il processo di certificazione impraticabile per sistemi di grandi dimensioni a meno che $NP = coNP$.

Gli autori propongono la certificazione interattiva, un paradigma basato sui sistemi di prova interattiva (IP), in cui un prover e un verifier partecipano a un protocollo a più round. Il verifier pone domande in modo adattivo, permettendogli di rilevare errori con alta probabilità in tempo polinomiale, anche se il calcolo sottostante è complesso. Sebbene le prove interattive per problemi PSPACE (come il model checking CTL) siano teoricamente stabilite ($IP=PSPACE$ di Shamir), renderle pratiche per il model checking simbolico utilizzando Diagrammi di Decisione Binaria (BDD) è rimasto una sfida aperta.

2. Metodologia

Il documento presenta iSMC, il primo model checker auto-certificante che implementa la certificazione interattiva per il model checking CTL con requisiti di giustizia. Il sistema è costruito su tre moduli fondamentali:

2.1 Architettura

• Solver: Un model checker simbolico basato su BDD che calcola l'insieme degli stati raggiungibili che soddisfano una specifica CTL. Opera su modelli booleani appiattiti (formato SMV) e utilizza la libreria BDD clic.
• Prover: Esegue sulla stessa macchina del Solver. Esegue l'istanza di model checking e genera una traccia di esecuzione composta dalla sequenza di chiamate alla libreria BDD e asserzioni effettuate durante il calcolo.
• Verifier: Un modulo leggero che può essere eseguito su un client con risorse limitate. Non riesegue l'algoritmo di model checking. Invece, partecipa a un protocollo interattivo con il Prover per verificare la traccia di esecuzione.

2.2 Il Protocollo TraceCert

L'innovazione centrale è TraceCert, un protocollo di prova interattiva adattato dal lavoro sulla certificazione QBF di Couillard et al. [11].

1. Traccia a Circuito: La traccia di esecuzione viene trasformata in un Circuito Booleano Generalizzato (GBC). Ogni istruzione nella traccia diventa una porta, e le asserzioni (ad esempio, "l'insieme di stati $C_1$ non è equivalente a $C_0$") diventano affermazioni di equivalenza.
2. Aritmetizzazione: Le funzioni booleane sono codificate come polinomi multivariati su un campo finito $\mathbb{F}_p$. Ciò permette al verifier di verificare le proprietà del calcolo valutando i polinomi in punti casuali invece di attraversare l'intero circuito.
3. Riduzione del Grado: Per garantire che i polinomi abbiano un grado basso (necessario per la verifica in tempo polinomiale), il protocollo introduce porte di riduzione del grado ($\delta_x$) che riducono gli esponenti a 1 senza cambiare il valore della funzione su input booleani.
4. Round Interattivi: Il protocollo procede a round, attraversando il circuito. Il Prover afferma il valore di una porta; il Verifier sfida il Prover con assegnazioni casuali agli input della porta. Il Prover deve fornire polinomi coerenti con l'affermazione. Se il Prover mente, la probabilità di essere scoperto è limitata dal lemma di Schwartz-Zippel.

2.3 Miglioramenti Tecnici Chiave rispetto al Lavoro Precedente

Gli autori estendono la tecnologia da [11] (che si concentrava su QBF) per gestire le esigenze specifiche del model checking CTL, affrontando tre principali colli di bottiglia:

1. Rinomina ed Equivalenza Efficienti: Il protocollo originale (CPCertify) gestiva le porte di equivalenza e rinomina in modo inefficiente ($O(n^2)$ e $O(n^k)$). TraceCert ottimizza questi round a $O(1)$ e $O(n)$ rispettivamente.
2. Compatibilità con la Raccolta della Spazzatura: Le librerie BDD standard utilizzano cache di calcolo globali e raccolta della spazzatura. L'approccio precedente richiedeva al Prover di memorizzare tutti i BDD intermedi, impedendo la raccolta della spazzatura. Gli autori introducono TraceCertRev, una variante bottom-up del protocollo che permette al Prover di scartare i risultati intermedi (agendo come un oracolo) senza compromettere la correttezza, a condizione che il Prover non cospiri maliziosamente per ricordare le sfide passate.
3. Cache di Calcolo Globale: L'implementazione precedente (blic) non poteva utilizzare una cache globale perché manipolava BDD estesi (eBDD) in modo incompatibile con la memorizzazione nella cache. Gli autori introducono una nuova rappresentazione eBDD immutabile utilizzando campi di collegamento per versionare i nodi, permettendo l'uso di una tabella globale unica e migliorando significativamente le prestazioni.

3. Contributi Chiave

1. Sistema iSMC: La prima implementazione di un model checker auto-certificante con certificazione interattiva per proprietà CTL arbitrarie con requisiti di giustizia.
2. Protocollo TraceCert: Un nuovo protocollo di prova interattiva che gestisce in modo efficiente la rinomina delle variabili e le asserzioni di equivalenza comuni nelle tracce di model checking, riducendo la complessità di specifici round di porte.
3. Implementazione eBDD Ottimizzata: Un nuovo algoritmo (ApplyEBDD) e una struttura dati che permettono l'uso di cache di calcolo globali e raccolta della spazzatura, superando le inefficienze della precedente libreria blic.
4. TraceCertRev: Una variante del protocollo che permette la raccolta della spazzatura durante la certificazione, rendendo il sistema fattibile per il model checking su larga scala dove la memoria è un vincolo.

4. Risultati Sperimentali

Gli autori hanno valutato iSMC su 53 benchmark dalla traccia di vivacità (liveness track) di HWMCC'25.

• Prestazioni del Solver: Rispetto allo strumento maturo NuSMV, il Solver di iSMC è in media 5,84 volte più lento. Gli autori attribuiscono ciò principalmente alla mancanza di supporto per i prodotti relazionali (un'ottimizzazione BDD) nel prototipo corrente, poiché certificarli in modo interattivo rimane un problema aperto.
• Sovraccarico del Prover: Il Prover esegue in tempo $O(S)$, dove $S$ è il tempo del Solver. Il fattore costante è approssimativamente 2,00, il che significa che il sovraccarico di certificazione è circa il doppio del tempo di risoluzione.
• Efficienza del Verifier: Il Verifier è altamente efficiente. Per un timeout di 15 minuti sul Prover, il Verifier non ha mai impiegato più di 3,6 secondi (accelerazione media di 33,4x rispetto al Prover). Il tempo di esecuzione del Verifier scala linearmente con la lunghezza della traccia di esecuzione, non con il tempo di calcolo.
• Impatto delle Ottimizzazioni: I miglioramenti (TraceCert, libreria clic, cache globale) hanno portato a un'accelerazione media di 2,26x nel tempo di esecuzione e a una riduzione di 16,12x nell'uso della memoria rispetto all'implementazione di base che utilizzava CPCertify e blic.

5. Significato e Affermazioni

Il documento afferma che iSMC rappresenta un passo significativo verso la certificazione interattiva pratica per il model checking.

• Fiducia in Server Non Attendibili: Il sistema permette uno scenario in cui un client con risorse limitate può delegare il model checking a un server potente ma non attendibile. Il server (Solver + Prover) esegue il calcolo pesante, mentre il client (Verifier) certifica il risultato con alta probabilità in tempo polinomiale.
• Verifica Polinomiale: A differenza dei metodi di certificazione non interattivi che richiedono tempo esponenziale per proprietà CTL generali, il Verifier di iSMC esegue in tempo polinomiale rispetto al numero di variabili e alla lunghezza della traccia.
• Scalabilità: Gli autori dimostrano che con le loro ottimizzazioni, il sovraccarico della certificazione interattiva è gestibile e l'ingombro di memoria è significativamente ridotto, rendendo l'approccio fattibile per benchmark non banali.

Gli autori rimangono modesti, notando che iSMC è un primo prototipo. Riconoscono che il Solver è attualmente più lento di strumenti all'avanguardia come NuSMV a causa della mancanza di ottimizzazioni (prodotti relazionali) e che l'implementazione corrente è mirata al CTL, sebbene il framework sottostante potrebbe teoricamente estendersi al calcolo modale $\mu$ completo.