Riepilogo Tecnico: Esecuzione Multi-Versione Divergente (DME)

Enunciato del Problema

I meccanismi di ridondanza tradizionali, come l'esecuzione lockstep e la Ridondanza Modulare Tripla (TMR), si basano sull'esecuzione di binari identici con layout di memoria identici. Sebbene efficaci contro guasti indipendenti, questi sistemi sono vulnerabili a guasti correlati. Studi sperimentali (ad esempio, Dutertre et al.) hanno dimostrato che disturbi fisici, come l'iniezione di guasti elettromagnetici, possono indurre perturbazioni identiche (ad esempio, un specifico $\Delta PC$) su tutte le repliche simultaneamente. Nei sistemi convenzionali, tali perturbazioni correlate ridirigono tutte le repliche lungo lo stesso percorso di esecuzione errato, portando a una corruzione silenziosa dei dati che rimane non rilevata perché tutte le repliche producono stati errati identici. Inoltre, la ridondanza convenzionale spesso non riesce a rilevare classi specifiche di bug software (ad esempio, puntatori non inizializzati, sovrascritture di indirizzi di ritorno) o difetti di compilazione/collegamento che si manifestano in modo identico su tutte le repliche.

Metodologia

Il documento propone l'Esecuzione Multi-Versione Divergente (DME), un verificatore di coerenza semantica runtime progettato per rilevare guasti correlati assicurando che perturbazioni numeriche identiche risultino in percorsi di esecuzione semanticamente divergenti.

Principi Fondamentali

Il DME opera su quattro principi fondamentali imposti al momento della compilazione:

1. Compilazione Indipendente: $N$ repliche sono compilate indipendentemente dallo stesso codice sorgente. Ciò produce layout fisici distinti di codice e dati, preservando al contempo semantiche identiche a livello di opcode e grafi di flusso di controllo isomorfi.
2. Decorrelazione a Grana Grossa: Le funzioni e i blocchi di base sono posizionati a indirizzi diversi tra le repliche utilizzando pattern di spostamento dei rami complementari (ad esempio, rami in avanti in una replica diventano rami all'indietro in un'altra). Ciò garantisce che perturbazioni identiche del flusso di controllo mappino su percorsi semanticamente diversi.
3. Decorrelazione a Grana Fina: Istruzioni NOP periodiche vengono inserite a offset specifici per la replica ($offset_r = \frac{l}{N} \cdot r$). Ciò crea una separazione spaziale minima tra le istruzioni logiche corrispondenti, consentendo il rilevamento di perturbazioni del Program Counter (PC) di piccola entità.
4. Decorrelazione degli Indirizzi dei Dati: Le variabili globali, i frame dello stack e le allocazioni dell'heap vengono assegnati a indirizzi di base assoluti unici per ogni replica.

Meccanismi di Rilevamento dei Guasti

Il DME impiega una strategia di rilevamento a doppio livello:

1. Livello Semantico (Traccia di Istruzione Canonica):

   • Il sistema confronta le "tracce canoniche" tra le repliche. Una traccia canonica include opcode, identificatori di registro, operandi immediati, valori caricati/archiviati e risultati calcolati.
   • Crucialmente, gli indirizzi assoluti sono esclusi dalla traccia.
   • In assenza di guasti, tutte le repliche producono tracce canoniche identiche. Qualsiasi guasto che alteri la semantica dell'esecuzione (ad esempio, l'esecuzione di un'istruzione diversa o il calcolo di un risultato diverso) causa una divergenza della traccia.

2. Livello Strutturale (Decorrelazione dello Spazio Indirizzi e Non-Aliasing):

   • Il DME tratta l'uguaglianza degli indirizzi fisici (ad esempio, $PC_1 = PC_2 = \dots = PC_N$) tra le repliche come una violazione dell'indipendenza strutturale, piuttosto che come uno stato ammissibile.
   • Invariante di Non-Aliasing degli Indirizzi: Il sistema impone che gli accessi alla memoria semanticamente corrispondenti (dati o istruzioni) debbano indirizzare indirizzi effettivi diversi tra le repliche.
   • Se un guasto (ad esempio, un overflow del buffer o una dereferenziazione di un puntatore nullo) causa a tutte le repliche il calcolo dello stesso indirizzo errato, il sistema attiva immediatamente un errore. Ciò consente il rilevamento di corruzioni di puntatori e sovrascritture di indirizzi di ritorno prima che si verifichi una divergenza semantica.

Modelli di Guasto e Regimi di Rilevamento

Il documento categorizza le garanzie di rilevamento in base alla natura della perturbazione:

• Rilevamento Deterministico:

  • Si applica ai guasti fully correlati dove $\Delta PC$ è identico su tutte le repliche.
  • Se $|\Delta PC| \geq l/N$ (dove $l$ è l'intervallo di inserimento NOP), la perturbazione garantisce che almeno una replica esegua un'istruzione logica diversa, portando a una divergenza immediata della traccia.
  • Il collasso dello spazio degli indirizzi (PC o puntatori identici) viene rilevato immediatamente come violazione strutturale.

• Rilevamento Probabilistico:

  • Si applica ai guasti parzialmente correlati (dove $\Delta PC$ differisce tra le repliche) o ai guasti dove $|\Delta PC| < l/N$.
  • Il rilevamento si basa sulla bassa probabilità che le repliche si allineino accidentalmente alla stessa istruzione logica e producano risultati identici.
  • La probabilità di rimanere non rilevati per $k$ passi è limitata da $(\frac{C}{|S|} \cdot \epsilon)^k$, dove $C$ è il numero di istruzioni canonicamente equivalenti, $|S|$ è lo spazio totale delle istruzioni e $\epsilon$ è la probabilità di risultati identici. Per architetture ISA tipiche a 32 bit, questa probabilità decade esponenzialmente (ad esempio, $\epsilon \leq 2^{-52}$).

Contributi Chiave

1. Decorrelazione Strutturale dello Spazio Indirizzi: Il documento introduce un metodo per trasformare perturbazioni a basso livello correlate in divergenza semantica osservabile diversificando attivamente i layout di memoria e gli spostamenti dei rami durante la compilazione.
2. Monitoraggio della Traccia Canonica: Definisce una rappresentazione di traccia indipendente dal layout che cattura l'esecuzione semantica (opcode, registri, risultati) scartando le informazioni dipendenti dall'indirizzo, consentendo un confronto robusto tra binari diversi.
3. Rilevamento a Doppio Livello: Il DME combina il confronto delle tracce semantiche con il monitoraggio strutturale degli indirizzi. Ciò consente il rilevamento immediato di eventi di "collasso degli indirizzi" (ad esempio, indirizzi di ritorno identici) che la ridondanza tradizionale potrebbe non rilevare se il percorso di esecuzione risultante fosse per caso identico.
4. Modello di Correttezza Formale: Il documento distingue tra correttezza semantica runtime (uguaglianza delle tracce) e correttezza a livello di sistema (uguaglianza semantica + indipendenza strutturale). Dimostra formalmente che l'indipendenza strutturale è una condizione sufficiente per garantire l'osservabilità dei guasti correlati.

Risultati e Affermazioni

Il documento afferma che il DME fornisce:

• Rilevamento deterministico per guasti PC correlati dove l'entità della perturbazione supera l'intervallo di decorrelazione ($|\Delta PC| \geq l/N$).
• Rilevamento probabilistico con decadimento esponenziale per altri tipi di guasti, limitato dallo spazio degli stati dell'architettura del set di istruzioni.
• Rilevamento immediato delle violazioni della semantica dei puntatori (ad esempio, puntatori nulli, errori di valore come puntatore) tramite l'Invariante di Non-Aliasing degli Indirizzi, spesso prima della divergenza semantica.
• Fattibilità Pratica: Gli autori citano un'implementazione prototipale su un processore soft a 32 bit (3o|||sheet) eseguito su un FPGA Altera Cyclone IV e un'implementazione di Macchina Virtuale su un core Cortex-M, dimostrando che l'overhead è gestibile (ad esempio, 3000 LUT e 16 KB BRAM per replica).

Significato

Il documento posiziona il DME come una ridefinizione della ridondanza per sistemi embedded critici per la sicurezza. A differenza degli Ambienti di Esecuzione Multi-Variante (MVEE), che utilizzano principalmente la diversificazione per ostacolare la portabilità degli exploit, il DME utilizza la decorrelazione strutturale come invariante di correttezza runtime formale per rilevare corruzioni a livello di bit causate da disturbi fisici.

Gli autori sottolineano che il DME affronta una specifica lacuna nella tolleranza ai guasti esistente: l'incapacità della ridondanza convenzionale di rilevare perturbazioni correlate a livello di istruzione che preservano l'uguaglianza dello stato ma violano la semantica del programma. Imponendo l'indipendenza strutturale, il DME garantisce che guasti numerici identici non possano risultare in comportamenti logici identici, trasformando così i rischi di corruzione silenziosa dei dati in eventi rilevabili. Il lavoro è presentato come un meccanismo indipendente dall'hardware, analizzabile formalmente, adatto per ambienti in cui l'iniezione di guasti elettromagnetici o ambientali rappresenta una minaccia realistica.