Detecting speculative leaks with compositional semantics

1. Il Problema

L'esecuzione speculativa è una tecnica fondamentale nei processori moderni per migliorare le prestazioni, prevedendo i risultati intermedi ed eseguendo istruzioni basandosi su queste previsioni. Tuttavia, quando le previsioni sono errate, le istruzioni speculativamente eseguite vengono annullate ("squashed") a livello architetturale, ma lasciano tracce persistenti nei componenti microarchitettonici (come cache, buffer di previsione e buffer di indirizzi di ritorno).

Queste tracce possono essere sfruttate da attaccanti per rubare informazioni sensibili, come dimostrato dalla famiglia di attacchi Spectre. Le sfide principali identificate dagli autori sono:

• Mancanza di caratterizzazione formale: Le contromisure esistenti spesso mancano di una definizione rigorosa di sicurezza, rendendo difficile verificarne l'efficacia.
• Limitazioni degli approcci attuali: Gli strumenti esistenti per il rilevamento delle fughe di informazioni (leaks) supportano solo meccanismi di speculazione fissi e hard-coded (es. solo previsione di branch o solo disambiguazione di memoria). Non sono in grado di modellare le interazioni complesse tra diversi meccanismi di speculazione che possono avvenire simultaneamente, portando a falsi negativi (mancato rilevamento di vulnerabilità combinate).
• Scalabilità: Non esiste un framework estensibile che permetta di aggiungere facilmente nuovi meccanismi di speculazione senza dover riscrivere interi modelli formali e relative dimostrazioni di sicurezza.

2. Metodologia

Gli autori propongono un approccio basato sulla semantica composizionale per modellare e analizzare le fughe di informazioni speculative. La metodologia si articola in tre pilastri principali:

A. Semantica Speculativa e Oracolo di Previsione

Il paper definisce un modello semantico operativo generalizzato per l'esecuzione speculativa.

• Oracolo di Previsione (Prediction Oracle): Un componente astratto che decide il percorso speculativo (es. quale ramo di un if prendere) e la durata della finestra speculativa.
• Semantica "Always-Mispredict" (AM): Per garantire garanzie di sicurezza indipendenti dalla specifica strategia di previsione di un processore (spesso non documentata), viene introdotta una semantica che assume che ogni previsione sia errata. Questo modello esplora sistematicamente tutti i percorsi sbagliati entro una finestra temporale limitata, garantendo che se un programma è sicuro sotto questa semantica "peggiore", lo sarà anche sotto qualsiasi altra strategia di previsione reale.

B. Speculative Non-Interference (SNI)

Viene introdotta una nuova nozione di sicurezza chiamata Speculative Non-Interference (SNI).

• Concetto: Un programma è sicuro se le informazioni che "trapelano" nello stato microarchitettonico durante l'esecuzione speculativa non sono maggiori di quelle che trapelano durante un'esecuzione non speculativa standard.
• Modello dell'Attaccante: L'attaccante osserva i pattern di accesso alla memoria e i target dei salti (jump targets). Se due stati iniziali indistinguibili per l'attaccante (basati su dati pubblici) producono tracce di osservazione diverse sotto la semantica speculativa ma identiche sotto quella non speculativa, allora c'è una violazione di SNI (una fuga di informazioni).

C. Framework di Composizione

Questa è l'innovazione centrale del lavoro. Invece di creare un unico modello monolitico per ogni combinazione di attacchi, gli autori definiscono un framework per comporre semantiche speculative individuali.

• Semantiche Atomiche: Vengono definiti modelli specifici per diversi meccanismi:
  • $\mathcal{B}$: Speculazione su Branch (Spectre-PHT).
  • $\mathcal{J}$: Speculazione su Salti Indiretti (Spectre-BTB).
  • $\mathcal{S}$: Speculazione su Store (Spectre-STL, bypass dello store).
  • $\mathcal{R}$: Speculazione su Return (Spectre-RSB).
  • $\mathcal{SLS}$: Straight-Line Speculation (Spectre-SLS).
• Composizione: Il framework permette di combinare queste semantiche (es. $\mathcal{B} + \mathcal{S}$) in una semantica composta unica. Il sistema utilizza parametri metaparametrici ($Z$) per gestire la delega delle istruzioni tra le semantiche sorgente, garantendo che le interazioni siano corrette.
• Preservazione della Sicurezza: Viene dimostrato teoricamente che se le semantiche sorgente sono "ben formate" (Well-Formed Speculative Semantics - WFSS), anche la semantica composta lo è. Questo permette di riutilizzare le dimostrazioni di sicurezza per le combinazioni complesse senza doverle riscrivere da zero.

3. Contributi Chiave

1. SNI (Speculative Non-Interference): La prima definizione semantica di sicurezza specifica per gli attacchi di esecuzione speculativa, basata sul confronto tra comportamento speculativo e non speculativo.
2. Framework Composizionale: Un metodo formale per combinare modelli di speculazione diversi, permettendo di analizzare vulnerabilità che emergono solo dall'interazione di più meccanismi (es. un attacco che richiede sia un branch mispredict che un store bypass).
3. Spectector: Uno strumento di analisi statica basato su esecuzione simbolica e solver SMT (Z3) che implementa il framework.
   • Traduce assembly x86 in un linguaggio intermedio ($\mu$Asm).
   • Esegue l'analisi su tutte le semantiche speculative definite (singole e combinate).
   • Verifica automaticamente la SNI generando formule logiche per rilevare discrepanze nelle tracce di osservazione.
4. Copertura Completa: Il framework supporta 5 classi di attacchi Spectre e le loro 18 combinazioni possibili (escludendo combinazioni incompatibili come RSB e SLS che agiscono sullo stesso istruzione).

4. Risultati Sperimentali

Gli autori hanno valutato Spectector su due casi studio principali:

• Benchmarks Individuali: Analisi di 291 programmi (varianti di Spectre-PHT, BTB, STL, RSB, SLS) compilati con diversi compilatori (Clang, GCC, MSVC, ICC) e livelli di ottimizzazione.

  • Spectector ha rilevato con successo tutte le fughe note negli esempi non patchati.
  • Ha dimostrato la sicurezza delle versioni patchate (con lfence, retpoline, o hardening dei carichi speculativi).
  • Ha identificato casi in cui i compilatori inserivano contromisure non necessarie (over-patching) o, al contrario, fallivano nel proteggere il codice in scenari specifici (es. ottimizzazioni aggressive che bypassano le difese).

• Benchmarks Combinati (Spectre-Comb): Creazione di 18 micro-benchmark progettati per essere vulnerabili solo quando due o più meccanismi di speculazione interagiscono.

  • Gli strumenti esistenti che analizzano i meccanismi in isolamento non hanno rilevato alcuna vulnerabilità in questi programmi (falsi negativi).
  • Spectector, utilizzando le semantiche composte, ha rilevato con successo le fughe di informazioni in tutti i 18 casi.
  • Ha dimostrato che le semantiche composte "più forti" (che includono più meccanismi) rilevano le vulnerabilità dei casi "più deboli", confermando la correttezza del framework.

5. Significato e Impatto

Questo lavoro rappresenta un avanzamento significativo nella sicurezza dei sistemi informatici per diversi motivi:

• Rigore Formale: Fornisce una base matematica solida per ragionare sulla sicurezza contro Spectre, superando l'approccio euristico o basato su pattern.
• Scalabilità e Estendibilità: Il framework composizionale risolve il problema della complessità crescente dei processori moderni. Quando viene scoperto un nuovo meccanismo di speculazione, è sufficiente definire la sua semantica atomica; la sicurezza delle combinazioni con i meccanismi esistenti è garantita "gratuitamente" dai teoremi di composizione.
• Strumento Pratico: Spectector offre agli sviluppatori e ai ricercatori uno strumento automatizzato per verificare la sicurezza del codice a livello di assembly, identificando vulnerabilità sottili che sfuggono alle analisi manuali o agli strumenti attuali.
• Ottimizzazione delle Contromisure: Permette di identificare quando le contromisure sono eccessive, aiutando a bilanciare sicurezza e prestazioni.

In sintesi, il paper trasforma la rilevazione delle fughe speculative da un'attività di "caccia ai pattern" a un processo di verifica formale composizionale, rendendo possibile analizzare la sicurezza di sistemi complessi in modo modulare e rigoroso.