Sintesi Tecnica: Controllo Supervisorio Attivo per la Preservazione dell'Opacità

Definizione del Problema

L'ingegneria dei sistemi moderni si affida sempre più ai metodi formali per verificare la sicurezza, eppure quando un sistema viene ritenuto insicuro, la riprogettazione fondamentale è spesso proibitivamente costosa o impraticabile, particolarmente per i sistemi legacy o embedded. Le teorie tradizionali del controllo supervisorio affrontano questo problema limitando dinamicamente i percorsi di esecuzione del sistema, abilitando o disabilitando azioni controllabili per imporre politiche di sicurezza o di protezione. Tuttavia, questo paradigma classico di restrizione delle azioni è insufficiente contro gli attacchi temporali (timing attacks), una potente classe di attacchi side-channel dove gli avversari inferiscono dati interni sensibili misurando le variazioni nei tempi di esecuzione e di risposta.

In tali scenari, il semplice blocco delle azioni fallisce perché la cadenza degli eventi stesso rivela informazioni critiche. Per mitigare queste vulnerabilità, i sistemi devono manipolare il comportamento temporale, spesso inserendo ritardi artificiali per smussare le varanze temporali. Inoltre, la ricerca esistente sull'opacità (una proprietà di sicurezza basata sul linguaggio che garantisce che i segreti rimangano nascosti agli osservatori) si è concentrata ampiamente su automi finiti o modelli basati sullo stato. Questo articolo affronta il divario nella gestione dell'opacità basata sul linguaggio all'interno di un framework di Algebra dei Processi Temporizzati (TPA), specificamente per sistemi equivalenti alle macchine di Turing, dove né il supervisore né l'attaccante possiedono informazioni complete sul comportamento del sistema.

Metodologia

Il documento impiega un framework di Algebra dei Processi Temporizzati (TPA), un'estensione del Calculus of Communicating Systems (CCS) di Milner. La TPA introduce un'azione di tempo discreto ($t$) per modellare il trascorrere del tempo, permettendo la rappresentazione formale degli attacchi temporali e della fuga di informazioni.

Concetti Core

1. Opacità e Funzioni di Osservazione:

   • L'opacità è definita come la proprietà per cui, per ogni traccia che soddisfa un predicato segreto $\phi$, esiste un'altra traccia che non soddisfa $\phi$ ed è indistinguibile per un osservatore sotto una specifica funzione di osservazione $O$.
   • Il documento formalizza varie funzioni di osservazione ($O$) per modellare diverse capacità dell'attaccante:
     • Statica: Le azioni sono osservate indipendentemente dal contesto.
     • Dinamica: L'osservazione di un'azione dipende dalla cronologia delle azioni precedenti.
     • Orwelliana/m-Orwelliana: L'osservazione dipende dall'intera cronologia o da una finestra limitata di $m$ azioni precedenti.
   • Il framework assume un'informazione asimmetrica: l'attaccante ($O$) e il supervisore ($O_S$) possono avere diverse funzioni di osservazione e visibilità parziale.

2. Supervisore Attivo:

   • A differenza dei supervisori tradizionali che si limitano a disabilitare le azioni, il Supervisore Attivo proposto possiede una doppia capacità:
     1. Disabilitazione Azioni: Può proibire specifiche azioni controllabili da un insieme $C$.
     2. Inserimento Temporale: Può iniettare dinamicamente sequenze di azioni temporali ($t$) nel flusso di esecuzione.
   • Il supervisore opera sotto osservabilità parziale ($O_S$) e mira a garantire che la traccia supervisionata risultante appartenga a un insieme di Tracce Sicure ($K_{P,\phi,O}$), dove il predicato segreto $\phi$ non può essere dedotto dall'attaccante.

3. Modellazione Formale:

   • Le funzioni di osservazione, i predicati e i supervisori sono modellati come processi all'interno del framework TPA. Ciò consente l'uso di tecniche di verifica standard (equivalenza di tracce, bisimulazione) per analizzare le interazioni tra il sistema, il supervisore e l'attaccante.
   • Il sistema è modellato come un contesto $C(P, O_S, Sup)$, dove il supervisore intercetta e modifica l'esecuzione del processo $P$ in base alle proprie osservazioni.

Contributi Principali

Il documento presenta tre contributi primari:

1. Nuovo Framework di Supervisore Attivo sotto Visibilità Parziale:
   Gli autori introducono un modello di supervisore che opera sotto informazioni asimmetriche e incomplete. Questo modello combina unicamente le capacità di disabilitazione delle azioni con l'inserimento dinamico di azioni temporizzate per mitigare attivamente la fuga di informazioni, mirando specificamente ai side-channel temporali.

2. Formalizzazione di Funzioni di Osservazione Asimmetriche:
   Lo studio formalizza scenari in cui l'attaccante e il supervisore possiedono funzioni di osservazione distinte (ad esempio, statica vs dinamica, o diversi livelli di visibilità). Ciò consente di modellare contesti di sicurezza realistici in cui nessuna delle due entità ha la piena visibilità e le loro visioni della cronologia di esecuzione divergono.

3. Delimitazione dei Confini di Decidibilità:
   Il documento stabilisce un insieme completo di risultati di decidibilità e indecidibilità riguardanti l'esistenza di tali supervisori. Esso mappa i confini della fattibilità della verifica attraverso vari tipi di sistemi (stato finito vs equivalente a Turing), granularità di osservazione e capacità sia degli attaccanti che dei supervisori.

Risultati

L'analisi teorica produce i seguenti risultati chiave:

• Indecidibilità nei Casi Generali:

  • Verificare se un supervisore specifico è valido per un dato processo e opacità del linguaggio è indecidibile in generale (Proposizione 3).
  • Determinare se esiste qualsiasi supervisore che garantisca la sicurezza per un dato processo è anch'esso indecidibile (Proposizione 4). Ciò deriva dall'indecidibilità dell'opacità del linguaggio stesso nei modelli equivalenti a Turing.

• Decidibilità nei Casi Restretti:

  • Se il processo $P$ è a stato finito, le funzioni di osservazione sono statiche e il predicato segreto $\phi$ (e la sua negazione) è finitamente definibile (modellato da processi di test a stato finito), allora:
    • Verificare se un supervisore è valido è decidibile.
    • Confrontare i supervisori e trovare un supervisore massimale (uno che restringe minimamente il comportamento del sistema) è decidibile.
    • Un supervisore massimale a stato finito è garantito esistere (Proposizioni 7 e 8).

• Attacchi Temporali e Mitigazione:

  • Il documento definisce un sistema come incline agli attacchi temporali se è opaco sotto un'osservazione "tempo-astratta" ma non sotto un'osservazione "tempo-sensibile".
  • Dimostra che se un predicato è tempo-dipendente (ovvero una traccia segreta può essere resa non segreta inserendo ritardi temporali) e il supervisore ha almeno quanto di precisione osservativa dell'attaccante ($O \preceq O_S$), allora esiste un supervisore anche con un insieme vuoto di azioni controllabili ($C = \emptyset$). In questo caso, la sicurezza è ottenuta esclusivamente tramite l'inserimento di ritardi temporali (Proposizione 9).

• Vincoli di Controllabilità:

  • Se l'insieme delle tracce sicure non è controllabile (ovvero esiste una traccia sicura seguita da un'azione incontrollabile che conduce a una traccia non sicura), nessun supervisore esiste (Proposizione 2).

Significato e Rivendicazioni

Il documento rivendica di fornire una solida base teorica per l'analisi della sicurezza dei sistemi in un contesto di algebra dei processi, affrontando specificamente i limiti del controllo supervisorio tradizionale contro gli attacchi temporali.

• Unione di Paradigmi: Esso unisce il divario tra l'imposizione logica (blocco delle azioni) e la manipolazione temporale (inserimento di ritardi), offrendo un meccanismo di controllo unificato per l'opacità basata sul linguaggio.
• Modellazione Avversariale Realistica: Modellando sia gli attaccanti che i supervisori con potenti funzioni di osservazione asimmetriche, il framework cattura le dinamiche realistiche dei moderni sistemi decentralizzati dove gli agenti operano sotto visibilità parziale.
• Verifica Pratica: Gli autori affermano che per i sistemi a stato finito con osservazioni statiche, il framework proposto consente la verifica esatta e la sintesi di supervisori utilizzando strumenti esistenti come CAAL (Concurrency Workbench Alternating-Time Logic), a condizione che i predicati siano espressi tramite $\mu$-calculus.
• Direzioni Future: Il documento delinea modestamente i lavori futuri focalizzati sulla sintesi di supervisori a inserimento temporale minimo per ridurre l'overhead temporale (mantenendo la QoS) e sull'estensione del framework algebrico per includere la distribuzione spaziale, le architetture di rete e le metriche del consumo energetico per la verifica della sicurezza multi-dominio.

Il lavoro non propone nuove implementazioni sperimentali, ma stabilisce le condizioni matematiche sotto le quali la supervisione attiva e sicura è teoricamente possibile o impossibile, guidando la progettazione di architetture robuste per sistemi embedded e cyber-fisici.