A Deductive System for Contract Satisfaction Proofs

Questo articolo presenta un sistema deduttivo basato sulla bisimulazione relativa e formalizzato nell'assistente di prova Rocq per verificare in modo modulare e completo la soddisfazione dei contratti hardware-software, offrendo un'alternativa ai metodi di model checking per garantire la sicurezza contro gli attacchi side-channel.

L'essenziale

🛡️ Il Contratto tra Hardware e Software: Un Gioco di Fiducia

Immagina di avere un computer (l'hardware) e un programma che ci gira sopra (il software). Spesso, quando usiamo computer condivisi (come nei cloud), c'è il rischio che informazioni segrete "trapelino" attraverso canali nascosti, come il modo in cui il processore usa la sua memoria o il tempo che impiega a fare calcoli. Questo è il problema degli attacchi side-channel (come i famosi Spectre e Meltdown).

Per proteggersi, gli ingegneri creano dei "Contratti Hardware-Software".

• Il Contratto è come una promessa scritta fatta dal produttore del processore: "Se esegui questo programma, prometto che non perderai più informazioni di quanto dice questa lista di regole astratte".
• Il Programma è come un viaggiatore che deve attraversare un territorio sconosciuto.

Il problema è: come facciamo a essere sicuri che il processore (il territorio) rispetti davvero la promessa (il contratto)?
Fino a poco tempo fa, per dimostrarlo, gli ingegneri dovevano scrivere manuali di prova lunghissimi e complessi (25 pagine dense di matematica!) o usare computer per cercare automaticamente errori. Ma questi metodi avevano dei limiti: i manuali potevano contenere errori umani, e i computer automatici potevano non trovare la soluzione giusta o fermarsi a metà.

🕵️‍♂️ La Nuova Idea: Un Investigatore Interattivo

Gli autori di questo paper hanno detto: "Perché non usiamo un assistente matematico interattivo (chiamato Rocq, simile a un tutor molto pignolo) per costruire la prova passo dopo passo?"

Hanno creato un nuovo sistema di regole (un sistema deduttivo) che permette di dimostrare in modo sicuro che il processore rispetta il contratto.

L'Analogia della "Doppia Corsa"

Immagina una gara di corsa con quattro corridori:

1. Corridore A e B (il Contratto): Eseguono il programma seguendo le regole astratte.
2. Corridore C e D (l'Hardware): Eseguono lo stesso programma sul processore reale.

Il contratto dice: "Se A e B fanno esattamente la stessa strada e vedono le stesse cose, allora anche C e D devono finire la gara vedendo le stesse cose (senza rivelare segreti diversi)."

Il problema è che A e B potrebbero correre a velocità diverse da C e D. A volte il processore fa un passo, a volte ne fa tre, a volte si "specula" (fa una scommessa su quale strada prendere prima di sapere se è giusta). È come se A e B corressero su un tapis roulant sincronizzato, mentre C e D corrono su un terreno accidentato che a volte accelera e a volte rallenta.

🧩 La Soluzione: Il "Bisimulatore Relativo"

Il cuore della scoperta è una tecnica chiamata Bisimulazione Relativa.
Invece di cercare di far correre tutti i corridori allo stesso ritmo (cosa impossibile), il sistema permette di:

1. Saltare i passi su un lato se non sono importanti (come se A e B facessero una pausa mentre C e D corrono).
2. Costruire la prova mentre si va avanti, invece di dover avere tutto il piano pronto prima di iniziare.

Immagina di dover dimostrare che due mappe (una astratta e una reale) portano allo stesso risultato. Invece di disegnare l'intera mappa prima di partire, il sistema ti permette di:

• Dire: "Ok, qui le due mappe coincidono."
• Dire: "Qui la mappa reale fa un passo in più, ma non cambia il segreto."
• Dire: "Qui la mappa astratta salta un passaggio perché sa già cosa succederà."

Grazie a questa flessibilità, il sistema può gestire la speculazione (quando il processore indovina la strada sbagliata e poi torna indietro) senza impazzire.

🛠️ Come Funziona nella Pratica?

Gli autori hanno usato questo sistema per dimostrare due cose fondamentali su un processore moderno:

1. La regola "Mispredizione Sempre": Un contratto che dice "Immagina che il processore sbagli sempre a indovinare la strada e ne provi due contemporaneamente". Hanno dimostrato che anche se il processore reale è intelligente e indovina spesso, il contratto è comunque sicuro (perché il contratto è più "paranoico" e copre anche il caso peggiore).
2. L'esecuzione "Fuori Ordine": I processori moderni eseguono le istruzioni in un ordine diverso da quello scritto per essere più veloci. Hanno dimostrato che, anche se il processore salta avanti e indietro, il contratto astratto (che esegue tutto in ordine) è comunque una rappresentazione sicura.

🌟 Perché è Importante?

1. Sicurezza Matematica: Non si basano più su "speriamo che funzioni" o su prove scritte a mano che potrebbero avere errori. Usano un assistente matematico che controlla ogni singolo passaggio.
2. Modularità: Puoi costruire la prova a pezzi. Se dimostri che una parte funziona, puoi riutilizzare quel pezzo per dimostrare un'altra parte, come costruire con i LEGO.
3. Flessibilità: Il sistema sa gestire i tempi diversi tra il contratto e l'hardware, cosa che i metodi precedenti faticavano a fare.

In Sintesi

Questo paper è come aver inventato un nuovo linguaggio di istruzioni per gli ingegneri di sicurezza. Invece di dover scrivere manuali giganti e incomprensibili per dimostrare che un processore non ruba segreti, ora possono usare un sistema logico interattivo che costruisce la prova passo dopo passo, gestendo la complessità del mondo reale (come le scommesse del processore e i tempi diversi) in modo elegante e sicuro.

È un passo avanti enorme per rendere i nostri computer più sicuri contro gli spionaggi digitali, trasformando una prova matematica ardua in un processo gestibile e affidabile.

Sommario tecnico

Titolo: Un Sistema Deduttivo per le Dimostrazioni di Soddisfacimento dei Contratti

Autori: Arthur Correnson, Haoyi Zeng, Jana Hofmann.

---

1. Il Problema: Verifica della Sicurezza Hardware e Contratti

Il lavoro affronta la sfida di verificare la sicurezza dei programmi contro gli attacchi side-channel (es. Meltdown, Spectre) in ambienti dove più parti condividono l'hardware (es. cloud computing).

• Contesto: I dati segreti possono fuoriuscire attraverso le microarchitetture della CPU (cache, buffer, predittori di branch).
• Contratti Hardware-Software: Per permettere agli sviluppatori software di ragionare sulla sicurezza senza conoscere i dettagli microarchitettonici, si utilizzano "contratti". Un contratto è una specifica formale che astrae il comportamento di perdita di informazioni (leakage) a livello dell'ISA (Instruction Set Architecture).
• Soddisfacimento del Contratto (Contract Satisfaction): Affinché l'approccio sia corretto, la microarchitettura reale deve "soddisfare" il contratto. Formalmente, questo significa che se il contratto prevede lo stesso leakage per due esecuzioni diverse, anche l'hardware reale deve produrre tracce indistinguibili.
• Sfide Attuali:
  • Le prove manuali (pen-and-paper) sono lunghe, complesse e difficili da verificare (es. 25 pagine dense per un semplice processore).
  • I metodi automatizzati (model checking) dipendono dalla correttezza degli algoritmi e possono fallire senza fornire spiegazioni chiare.
  • La verifica richiede un ragionamento relazionale 4-ario (confronto tra due tracce del contratto e due tracce dell'hardware) con esecuzioni asincrone (i passi del contratto e dell'hardware non sono necessariamente allineati).

2. Metodologia: Bisimilazione Relativa e Co-induzione Parametrizzata

Gli autori propongono un approccio basato su assistenti di prova interattivi (in particolare Rocq, il successore di Coq) per costruire dimostrazioni deduttive.

A. Riformulazione del Problema: Uguaglianza Relativa delle Tracce

Il problema del soddisfacimento del contratto viene identificato come un caso specifico di uguaglianza relativa delle tracce (relative trace equality): dimostrare che "l'uguaglianza delle tracce del contratto implica l'uguaglianza delle tracce dell'hardware".
$$\llbracket P \rrbracket_C(\sigma) = \llbracket P \rrbracket_C(\sigma') \implies \llbracket P \rrbracket_H(\sigma, \mu) = \llbracket P \rrbracket_H(\sigma', \mu)$$

B. Bisimilazione Relativa (Relative Bisimulation)

Per evitare di ragionare direttamente su tracce infinite, gli autori introducono una tecnica basata sugli stati: la Bisimilazione Relativa.

• È una relazione 4-aria tra stati: due stati del contratto ($s_1, s_2$) e due stati dell'hardware ($h_1, h_2$).
• Sfida dell'asincronia: Una semplice bisimilazione "lockstep" (passo dopo passo) non è sufficiente perché il contratto e l'hardware possono avanzare a velocità diverse.
• Soluzione Ibrida: La definizione formale di bisimilazione relativa combina:
  • Co-induzione (per le tracce dell'hardware, che possono essere infinite).
  • Induzione (per i passi del contratto, che permettono di "skippare" passi o gestire l'ipotesi di uguaglianza delle tracce).
  • Questo approccio ibrido (greatest fixpoint esterno, least fixpoint interno per i passi del contratto) garantisce correttezza (soundness) e completezza.

C. Sistema Deduttivo e Quintuple di Prova

Per rendere la prova gestibile in un assistente formale, gli autori sviluppano un sistema deduttivo basato sulla Co-induzione Parametrizzata (Paco).

• Invece di dover fornire un'invariante relazionale completa all'inizio, il sistema permette di costruire l'invariante incrementalmente durante la prova.
• Vengono introdotte le Quintuple di Prova ($R \vdash [s_1, h_1, s_2, h_2]$), che rappresentano lo stato della prova.
• Regole Chiave:
  • C-Leak / C-Step: Gestiscono i passi del contratto (spostamento o verifica di leakage diverso).
  • H-Step: Gestisce i passi dell'hardware (richiede che il leakage sia uguale e permette di avanzare).
  • Invariant / Cycle / Guard: Permettono di accumulare ipotesi, chiudere cicli e gestire le ipotesi "protette" (guarded) e "non protette" (unguarded).

D. Tecniche "Up-To"

Per semplificare ulteriormente le prove, il sistema integra tecniche "up-to" che sfruttano proprietà come:

• Simmetria: Scambiare l'ordine degli stati.
• Transitività: Sostituire stati con altri equivalenti per ridurre o aumentare il leakage in modo controllato.
• Queste tecniche sono formalmente giustificate tramite funzioni compatibili con la definizione di bisimilazione.

3. Risultati e Casi di Studio

Gli autori hanno formalizzato l'intero sistema in Rocq e lo hanno applicato a due casi di studio significativi tratti dal contratto CT-SPEC:

1. Contratto "Always-Mispredict" (Sempre Errato):

   • Scenario: Modella l'esecuzione speculativa dei branch. Il contratto esegue sempre entrambi i rami di un branch (simulando un errore di previsione), mentre l'hardware potrebbe prevedere correttamente o errare.
   • Risultato: La prova dimostra che l'hardware soddisfa il contratto anche quando l'hardware prevede correttamente e il contratto esegue il ramo sbagliato per un certo numero di passi (gestendo l'asincronia tramite le regole C-Step e H-Step).

2. Contratto "Sequential" (Sequenziale):

   • Scenario: Modella l'esecuzione fuori ordine (out-of-order). Il contratto esegue le istruzioni in ordine sequenziale, mentre l'hardware può ritardare istruzioni "delayable" e eseguirle in ordine diverso.
   • Risultato: La prova valida che l'hardware out-of-order soddisfa il contratto sequenziale, sfruttando la transitività e le tecniche up-to per gestire lo scambio di istruzioni.

4. Contributi Chiave

1. Nuova Definizione Teorica: Introduzione della Bisimilazione Relativa come caratterizzazione completa e corretta dell'uguaglianza relativa delle tracce, risolvendo il problema dell'asincronia tra due sistemi con semantica diversa.
2. Sistema Deduttivo Formale: Sviluppo di un sistema di regole di inferenza (basato su Paco) che permette di provare proprietà relazionali 4-arie in modo modulare e incrementale, senza bisogno di indovinare l'invariante completa a priori.
3. Formalizzazione e Verifica: Implementazione completa in Rocq, dimostrando la correttezza e la completezza del sistema.
4. Integrazione di Tecniche Avanzate: Applicazione sistematica delle tecniche "up-to" (simmetria, transitività) all'interno del contesto dei contratti hardware-software, semplificando notevolmente le dimostrazioni.

5. Significato e Impatto

• Affidabilità: Sposta la verifica dei contratti hardware-software da approcci basati su testing o model-checking (che possono avere bug o limitazioni) a prove formali meccanizzate, garantendo un livello di fiducia superiore.
• Scalabilità: Il metodo modulare e incrementale rende fattibile la verifica di microarchitetture complesse che prima richiedevano prove manuali ingestibili.
• Generalità: Sebbene focalizzato sui contratti hardware, il sistema di bisimilazione relativa è applicabile ad altri problemi di sicurezza che richiedono ragionamento relazionale (es. compilazione sicura, non-interferenza speculativa).
• Futuro: Apre la strada a logiche di programma più astratte per la sicurezza hardware e all'estensione del sistema a semantica non deterministiche.

In sintesi, il paper fornisce un framework teorico e pratico fondamentale per garantire che le astrazioni di sicurezza utilizzate dagli sviluppatori software siano rigorosamente supportate dal comportamento reale dell'hardware, mitigando i rischi di attacchi side-channel.