Riepilogo Tecnico: Il Lato Positivo dell'Opacità Temporizzata

1. Definizione del Problema

Il documento affronta il problema dell'opacità temporizzata per gli Automi Temporizzati (TA). L'opacità temporizzata formalizza l'assenza di fuga di informazioni riguardante posizioni designate come "private" in un sistema in cui un attaccante osserva un sottoinsieme di azioni insieme ai loro timestamp. L'obiettivo di sicurezza fondamentale è garantire che un attaccante non possa dedurre con certezza se una posizione privata sia stata visitata durante l'esecuzione di un sistema.

Il problema è motivato dal lavoro seminale di Cassez [Cas09], che ha stabilito che l'opacità temporizzata è indecidibile per i TA generali, e notevolmente anche per la sottoclasse ristretta degli Automi di Registrazione di Eventi (ERA). Questa indecidibilità deriva dalla memoria illimitata richiesta da un attaccante per correlare i timestamp e dallo spazio degli stati infinito dei TA. Gli autori mirano a identificare i "lati positivi" di questo problema limitando o il modello di sistema o le capacità dell'attaccante per recuperare la decidibilità.

Il documento definisce tre varianti di opacità basate sulla relazione tra l'insieme di tracce generate dalle esecuzioni private ($Tr_{priv}$) e dalle esecuzioni pubbliche ($Tr_{pub}$):

1. $\exists$-opacità: Esiste almeno una traccia comune sia alle esecuzioni private che a quelle pubbliche (forma più debole).
2. Opacità debole (Weak opacity): Ogni traccia privata è anche una traccia pubblica ($Tr_{priv} \subseteq Tr_{pub}$).
3. Opacità totale (Full opacity): Gli insiemi di tracce private e pubbliche sono identici ($Tr_{priv} = Tr_{pub}$).

2. Metodologia

Gli autori impiegano una combinazione di costruzioni basate sugli automi, riduzioni a problemi classici dei TA (raggiungibilità, inclusione di linguaggi) e analisi della complessità.

2.1. Framework di Inter-riducibilità

Un contributo metodologico fondamentale è l'instaurazione dell'inter-riducibilità tra le varianti di opacità e i problemi classici dei TA:

• Opacità Debole vs. Totale: Si è dimostrato che sono inter-riducibili tramite una costruzione che scambia le esecuzioni private con quelle pubbliche (Teorema 4.5). Ciò consente agli autori di concentrarsi su una variante (tipicamente l'opacità debole) per le prove di decidibilità.
• $\exists$-opacità vs. Raggiungibilità: Si è dimostrato che sono inter-riducibili. Poiché la raggiungibilità è PSPACE-completa per i TA, ciò stabilisce la complessità della $\exists$-opacità.
• Opacità Debole vs. Inclusione di Linguaggi: Si è dimostrato che sono inter-riducibili. Poiché l'inclusione di linguaggi è indecidibile per i TA generali, ciò spiega l'indecidibilità dell'opacità debole/totale nel caso generale.

2.2. Analisi delle Sottoclassi

Gli autori analizzano l'opacità per specifiche sottoclassi di TA:

• TA a singola azione: Riduzione della dimensione dell'alfabeto.
• TA a singolo clock: Riduzione del numero di clock, con o senza transizioni $\epsilon$.
• TA a tempo discreto: Restrizione delle valutazioni dei clock ai numeri naturali ($\mathbb{N}$) invece che ai reali ($\mathbb{R}_{\ge 0}$).
• oERA (Observable ERAs): Una nuova sottoclasse in cui tutte le azioni che resettano i clock sono osservabili (nessuna transizione $\epsilon$ nascosta che resetta i clock).

2.3. Riduzione del Budget dell'Attaccante

Per gestire l'intera classe di TA, gli autori introducono una nuova metodologia che limita il "budget" dell'attaccante. Definiscono funzioni di selezione temporale ($\sigma$) che determinano quando un attaccante osserva il sistema. Vengono analizzate tre impostazioni specifiche:

1. Prime $N$ osservazioni: L'attaccante vede solo le prime $N$ azioni osservabili.
2. $N$ timestamp statici: L'attaccante pre-seleziona $N$ punti temporali e osserva la prima azione che avviene dopo ciascuno di essi.
3. $N$ timestamp dinamici: L'attaccante seleziona adattivamente il successivo tempo di osservazione in base alle osservazioni precedenti.

Per dimostrare la decidibilità per queste impostazioni limitate, gli autori introducono una costruzione "tick". Questa consiste nell'augumentare il TA con un clock "tick" globale e clock ausiliari per codificare la classe di equivalenza delle parole temporizzate (basata sulle parti intere e sull'ordinamento relativo delle parti frazionarie) in una traccia non temporizzata. Ciò trasforma il problema dell'inclusione di linguaggi temporizzati per osservazioni limitate in un problema di inclusione di linguaggi per automi regolari finiti (specificamente, linguaggi $N$-limitati).

3. Contributi Chiave e Risultati

3.1. Inter-riducibilità e Complessità

• Equivalenza tra Opacità Debole e Totale: Gli autori dimostrano che decidere l'opacità debole è polinomialmente equivalente a decidere l'opacità totale. Ciò semplifica l'analisi delle sottoclassi.
• Complessità della $\exists$-opacità: Il problema è PSPACE-completo per i TA generali. Per i TA a singolo clock, gli autori dimostrano che rimane PSPACE-completo (Teorema 5.1), raffinando i limiti precedenti.

3.2. Decidibilità nelle Sottoclassi

Il documento traccia un confine preciso tra decidibilità e indecidibilità per l'opacità debole/totale:

• Indecidibile:
  • TA con una singola azione (anche senza transizioni $\epsilon$) (Teorema 5.2).
  • TA con due o più clock (Teorema 5.7).
  • TA con un singolo clock con transizioni $\epsilon$ (Teorema 5.4).
• Decidibile:
  • TA con un singolo clock senza transizioni $\epsilon$: Decidibile con complessità non-primitiva ricorsiva (Teorema 5.5).
  • TA su tempo discreto: Decidibile con complessità EXPSPACE-completa (Corollario 5.14).
  • oERA (Observable ERAs): Decidibile con complessità PSPACE-completa (Teorema 5.16).

Nota: Il documento stabilisce anche che l'inclusione di linguaggi temporizzati per i TA a tempo discreto è EXPSPACE-completa, un risultato precedentemente noto come decidibile ma con complessità esatta ignota.

3.3. Budget Limitato dell'Attaccante (Contributo Principale)

Il contributo più significativo è la prova che l'opacità diventa decidibile per l'intera classe di TA se il budget di osservazione dell'attaccante è limitato a $N$ osservazioni.

• Impostazioni: Il risultato è valido per tutti e tre i modelli di attaccante: prime $N$ azioni, $N$ timestamp statici e $N$ timestamp dinamici.
• Complessità: Il problema decisionale per tutte e tre le impostazioni è Co-NEXPTIME-completo (Teorema 6.19, Corollario 6.20, Teorema 6.31, Teorema 6.33).
• Meccanismo: La prova si basa sulla costruzione "tick" per ridurre il problema temporizzato all'inclusione di linguaggi temporizzati $N$-limitati, che si dimostra essere Co-NEXPTIME-completa.

3.4. Combinazione di Restrizioni

Gli autori analizzano anche la combinazione di restrizioni del modello (es. un solo clock, tempo discreto) con il budget dell'attaccante.

• Per i TA a singola azione con $N$ osservazioni, il problema rimane Co-NEXPTIME-completo.
• Per i TA a singolo clock con $N$ osservazioni, il problema è PSPACE-hard e appartenente a Co-NEXPTIME (Teorema 6.35).
• Per gli oERA con $N$ osservazioni, il problema è PSPACE-completo (Teorema 6.37).

4. Significato e Rivendicazioni

Il documento sostiene di fornire una caratterizzazione completa del panorama della decidibilità per l'opacità temporizzata, andando oltre i risultati negativi di Cassez [Cas09].

• Chiarire il Confine: Il lavoro identifica precisamente le condizioni minime (ad esempio, la presenza di transizioni $\epsilon$ nei TA a singolo clock, o il numero di azioni) che innescano l'indecidibilità.
• Decidibilità Pratica: Introducendo il concetto di un budget di osservazione limitato (osservazioni finite), gli autori dimostrano che l'opacità è decidibile per l'intera classe di Automi Temporizzati, a condizione che l'attaccante non possa osservare una sequenza illimitata di eventi. Ciò modella scenari realistici in cui gli attaccanti hanno risorse o capacità di monitoraggio limitate.
• Precisione della Complessità: Il documento fornisce classi di complessità esatte (PSPACE, EXPSPACE, Co-NEXPTIME) per varie impostazioni, raffinando la comprensione del costo computazionale della verifica dell'opacità.
• Innovazione Metodologica: La costruzione "tick" e l'uso di funzioni di selezione temporale offrono nuovi strumenti per analizzare sistemi temporizzati sotto osservazione parziale, colmando il divario tra la semantica a tempo denso e le tecniche di verifica a stati finiti.

Gli autori concludono che, sebbene l'indecidibilità persista in contesti altamente espressivi (TA generali con osservazione illimitata), limitare il potere dell'attaccante a un budget finito produce un framework robusto e decidibile applicabile all'intera formalizzazione dei TA.