Security Engineering in IIIf, Part II -- Shadowing the IIIf

Sintesi Tecnica: Shadowing the Isabelle Insider and Infrastructure Framework

Problematica
L'Isabelle Insider and Infrastructure Framework (IIIf) fornisce una base formale per l'ingegneria della sicurezza di sistemi che coinvolgono attori umani, policy e componenti fisiche/logiche, utilizzando un ciclo di Raffinamento-Rischio (RR). Sebbene il IIIf supporti la raffinazione basata su tracce e la preservazione delle proprietà per le standard proprietà di sicurezza (es. raggiungibilità), esso affronta un limite critico riguardante il Controllo del Flusso di Informazioni (IFC). Nello specifico, la proprietà di Non-interferenza (NI)—che garantisce che gli stati ad alta sicurezza (segreti) non influenzino le osservazioni a bassa sicurezza (pubbliche)—non è generalmente preservata sotto la raffinazione della specifica. Questo fenomeno, noto come "paradosso della raffinazione", significa che una specifica che soddisfa la NI può generare un'implementazione raffinata che perde informazioni attraverso flussi impliciti. Gli approcci esistenti di model-checking all'interno del IIIf sono insufficienti per verificare tali proprietà di insieme di tracce, rendendo necessaria una nuova metodologia per caratterizzare e garantire raffinazioni sicure.

Metodologia
Per affrontare il paradosso della raffinazione, il documento introduce una formalizzazione del concetto di "Shadow" (Ombra) di Morgan all'interno del framework IIIf. La metodologia procede attraverso i seguenti passaggi:

1. Integrazione del Caso di Studio: Gli autori utilizzano una specifica di un sistema radar di volo (precedentemente formalizzata in IIIf) come esempio corrente. Questo sistema coinvolge posizioni di aeromobili, rotte e località critiche. La specifica iniziale dimostra come si verifichino flussi di informazioni impliciti quando un aeromobile aggira una località critica, rivelando l'esistenza di tale criticità attraverso irregolarità osservabili nella traiettoria di volo.
2. Formalizzazione della Non-interferenza (NI): La NI è definita all'interno del IIIf come una relazione di indistinguibilità su transizioni di stato. Due stati sono indistinguibili per un attaccante (con livello di autorizzazione $a$) se le loro componenti osservabili (quelle con etichette di sicurezza $\leq a$) sono identiche. La NI si tiene se, per ogni coppia di stati iniziali indistinguibili, le loro tracce di esecuzione successive rimangono indistinguibili.
3. Definizione dello Shadow: Ispirandosi alla logica epistemica di Morgan, uno "Shadow" è definito come l'insieme di tutti i possibili valori che una componente di stato critica per la sicurezza potrebbe assumere dal punto di vista dell'attaccante.
   • Inizializzazione: Una componente shadow è inizializzata all' "universo" del suo tipo (tutti i valori possibili), rappresentando la massima ignoranza.
   • Restringimento (Shrinking): Durante le transizioni di stato, lo shadow "si restringe" (riduce l'insieme dei valori possibili) solo se la transizione rivela informazioni sulla componente segreta all'attaccante.
   • Invariante: Un sistema sicuro deve soddisfare l'invariante $IFC_a$, dove lo shadow di una componente segreta non si restringe durante l'esecuzione. Se lo shadow si restringe, implica che l'attaccante ha acquisito conoscenza riguardo al segreto, indicando una violazione della NI.
4. Prova di Equivalenza: Il documento stabilisce formalmente (sulla carta, a causa dei limiti di quantificazione dei tipi in Higher Order Logic) che l'invariante dello shadow $IFC_a$ è equivalente alla Non-interferenza ($NI_a$). Nello specifico, la negazione della NI (esistenza di un flusso di informazioni illecito) è mostrata essere equivalente all'esistenza di una componente il cui shadow si restringe.
5. Caratterizzazione della Raffinazione Sicura: Gli autori definiscono una condizione per la raffinazione sicura. Una raffinazione da un sistema astratto $A$ a un sistema concreto $C$ preserva la sicurezza se la mappa di raffinazione $E$, quando ristretta alle componenti shadow di $C$, è iniettiva e compatibile con lo shadow astratto.

Contributi Chiave

• Formalizzazione dello Shadow nel IIIf: Il documento estende il IIIf con una definizione formale di componenti "Shadow" per gli stati delle infrastrutture, permettendo il tracciamento dell'incertezza di un attaccante riguardo alle componenti segrete dello stato.
• Equivalenza tra Shadow e NI: Dimostra che l'invariante dello shadow ($IFC_a$) è equivalente alla proprietà di Non-interferenza ($NI_a$) nel contesto del modello a transizione di stato del IIIf.
• Teorema della Raffinazione Sicura (Teorema 2): Il contributo primario è un teorema che caratterizza la raffinazione sicura. Esso afferma che se una mappa di raffinazione $E$ è iniettiva sulle componenti shadow del sistema concreto ed è compatibile con lo shadow astratto, allora l'invariante dello shadow (e quindi la NI) è preservata dal sistema astratto al sistema concreto.
• Risoluzione del Paradosso della Raffinazione: La metodologia fornisce un meccanismo per verificare che un passo di raffinazione non introduca nuovi flussi di informazioni che violerebbero la NI, affrontando un difetto noto del ciclo RR standard del IIIf.

Risultati

• Applicazione al Sistema Radar di Volo: Gli autori applicano la definizione di shadow al caso di studio del sistema radar di volo.
  • In una versione insicura (senza meccanismi di occultamento), lo shadow della componente della località critica si restringe quando un aereo aggira un'area critica, provando la violazione di $IFC_a$ e della NI.
  • In una versione sicura (utilizzando una componente critpos per nascondere l'effettivo aggiramento), l'invariante dello shadow è rispettata, confermando l'assenza di flussi illeciti.
• Analisi della Raffinazione: Il documento dimostra che l'aggiunta di una nuova componente (es. "velocità") calcolata sulla base di posizioni nascoste costituisce una raffinazione insicura perché causa il restringimento dello shadow, violando le condizioni di iniettività/compatibilità del Teorema 2. Al contrario, mostra che l'aggiunta di componenti che non dipendono dai segreti e che sono gestite correttamente dalla mappa di raffinazione preserva la sicurezza.
• Limiti Meta-Teorici: Gli autori notano che, sebbene l'equivalenza tra Shadow e NI possa essere ragionata, la piena formalizzazione del teorema di equivalenza su tutti i tipi di infrastruttura è limitata dal sistema di tipi di Isabelle/HOL, poiché richiede la quantificazione su componenti di tipi differenti dello stato.

Significatività e Rivendicazioni
Il documento sostiene di estendere le capacità di ingegneria della sicurezza del framework IIiff integrando il Controllo del Flusso di Informazioni. La sua significatività risiede nel:

1. Affrontare il Paradosso della Raffinazione: Offre una metodologia concreta per garantire che le proprietà di sicurezza (specificamente la NI) siano preservate durante il processo di raffinazione, una capacità precedentemente assente nel framework.
2. Colmare il divario tra Astrazione e Implementazione: Utilizzando il concetto di shadow, il framework può ora ragionare formalmente sull' "ignoranza" di un attaccante e garantire che le raffinazioni non riducano inadvertamente tale ignoranza (ovvero, non perdano informazioni).
3. Verifica Pratica: L'approccio permette la verifica di sistemi complessi ed eterogenei (che combinano aspetti fisici e logici) dove il model checking standard fallisce.

Gli autori rimangono modesti riguardo all'ambito, riconoscendo che le prove di equivalenza sono attualmente stabilite "sulla carta" a causa dei vincoli di teoria dei tipi in Isabelle/HOL, e che la metodologia è specificamente adattata al modello di infrastruttura IIIf piuttosto che a una logica di linguaggio di programmazione general-purpose. Il lavoro si basa sui concetti fondamentali di Morgan ma li adatta a un sistema a transizione di stato con attori e policy espliciti, evitando la necessità di una logica epistemica dedicata sfruttando il modello di diritti di accesso degli attori già presente nel IIIf.