Sintesi dello Scudo come Analisi della Difendibilità per Reti Avversarie

1. Definizione del Problema

Gli strumenti attuali per la valutazione della sicurezza delle reti soffrono di una lacuna fondamentale. Gli strumenti di verifica statica possono confermare la raggiungibilità e l'isolamento su configurazioni fisse, ma non riescono a modellare avversari strategici. Al contrario, l'Apprendimento per Rinforzo (RL) per la cybersecurity addestra agenti adattivi contro attaccanti simulati, eppure una policy che sopravvive a un avversario può fallire contro un altro, e nessun metodo informale può certificare che una topologia di rete sia fondamentalmente indifendibile.

Gli approcci esistenti di Shielded Reinforcement Learning (ShRL) trattano tipicamente la sintesi dello scudo come un meccanismo di enforcement a runtime. In questo paradigma, le specifiche di logica temporale vengono compilate in automi per restringere le azioni di un agente durante l'addestramento o l'implementazione. Tuttavia, questo inquadramento affronta gravi limitazioni:

• Scalabilità: La sintesi a stati espliciti cresce esponenzialmente con le variabili di stato, limitando il calcolo trattabile a ambienti di piccole dimensioni.
• Fragilità del Modello: Le garanzie sono legate al modello. Se la dinamica implementata differisce dal modello di transizione assunto (mismatch del modello), lo scudo "sicuro" può assertare sicurezza dove non ne esiste.
• Osservabilità Parziale: Le formulazioni standard faticano con i Processi Decisionali di Markov Parzialmente Osservabili (POMDP) senza forti assunzioni di astrazione.

Gli autori sostengono che trattare la sintesi dello scudo come un filtro a runtime sia il "prodotto sbagliato". Propongono invece di riformulare lo stesso meccanismo teorico-automatistico come uno strumento analitico di design-time. L'obiettivo non è produrre una policy sicura per un agente distribuito, ma generare intuizioni strutturali e certificati formali sul fatto che un sistema sia difendibile, dove sia vulnerabile e come i cambiamenti architettonici influenzino la difendibilità.

2. Metodologia

Il paper istanzia questa prospettiva attraverso un Gioco di Sicurezza a Specifica Doppia Vincolata per la difesa di rete.

2.1 Il Gioco di Difesa di Rete

Il sistema modella un segmento critico di rete come un grafo diretto in cui gli host hanno stati (Pulito, Compromesso, Rilevato, Isolato, Distrutto). Il gioco coinvolge due giocatori:

• Difensore: Le azioni includono il monitoraggio, l'isolamento, il ripristino e la riparazione degli host.
• Attaccante: Le azioni includono la diffusione della compromissione e la distruzione degli host.

2.2 Doppia Specifica e Enforcement Asimmetrico

L'innovazione architettonica centrale è l'uso di due specifiche di logica temporale indipendenti compilate in Automi a Stati Finiti Deterministici (DFA), applicate asimmetricamente:

1. Specifica del Difensore ($\phi_D$): Definisce l'obiettivo di sicurezza (ad es., gli asset critici non devono essere simultaneamente compromessi). Questo automa ($A_D$) inizializza l'insieme non sicuro iniziale ($U$) del gioco di sicurezza. Se il sistema entra in uno stato in cui $A_D$ è in uno stato di rifiuto, la giocata è insicura.
2. Specifica dell'Attaccante ($\phi_A$): Impone vincoli operativi all'avversario (ad es., un budget di al massimo 2 azioni di "Distruzione" per impegno). Questo automa ($A_A$) filtra le azioni legali dell'attaccante durante il calcolo dell'attrattore. L'attaccante può scegliere solo transizioni che mantengano $A_A$ in uno stato di accettazione.

Questa asimmetria è cruciale: $\phi_D$ definisce cosa non deve mai accadere, mentre $\phi_A$ definisce cosa l'attaccante non può fare.

2.3 Soluzione del Gioco di Sicurezza e Calcolo dell'Attrattore

Il framework costruisce un gioco prodotto combinando lo stato della rete, l'indicatore di turno e entrambi gli stati degli automi. Calcola la Regione Vincente ($W$) per il difensore utilizzando un algoritmo di attrattore a punto fisso:

• L'Attrattore ($Attr^*$) è l'insieme degli stati da cui l'attaccante può forzare una violazione di $\phi_D$ indipendentemente dalla strategia del difensore.
• Il calcolo è modificato per rispettare $\phi_A$: un vertice dell'attaccante entra nell'attrattore solo se ha un successore legale (che soddisfa $\phi_A$) già presente nell'attrattore.
• Verdetto di Difendibilità: L'output primario è un certificato binario: lo stato iniziale $s_0 \in W$? Se sì, la topologia è difendibile; se no, non esiste una strategia di difesa.
• Estrazione dello Scudo: Lo scudo (una tabella di consultazione di azioni sicure) è derivato come un testimone del verdetto, non come un controllore a runtime.

2.4 Metriche di Difendibilità e Impronta Digitale

Per andare oltre un verdetto binario, gli autori derivano sei metriche per formare un'Impronta Digitale di Difendibilità:

• Livello 1 (Metriche di Gioco Formale): Derivate dalla decomposizione dei gusci dell'attrattore (la distanza degli stati dalla violazione).
  • Attaccabilità (ATK): Esposizione pesata della regione vincente all'attrattore.
  • Rapporto di Imboscata (SNK): Frazione di stati non violanti assorbiti nella regione insicura.
  • Attrito dello Scudo (FRC): La frazione di azioni del difensore bloccate dallo scudo per mantenere la sicurezza.
  • Ripidezza dell'Attrattore (STP): Entropia della distribuzione dei gusci (a scogliera vs pendenza dolce).
  • Prossimità della Violazione (VPX): Reciproco dei passi medi verso la violazione.
• Livello 2 (Metrica Operativa):
  • Rapporto di Dominanza dell'Attaccante (ADR): Derivato da MARL Avversariale con Scudo (Shielded Adversarial MARL). Due apprendisti minimax-Q giocano all'interno della regione vincente $W$. La metrica misura la frazione media di host controllati dall'attaccante all'equilibrio.

3. Contributi Chiave

1. Gioco di Sicurezza a Doppia Specifica Vincolata: Una formulazione in cui l'obiettivo di sicurezza del difensore e i vincoli operativi dell'attaccante sono compilati in separati DFA con ruoli di enforcement asimmetrici (inizializzazione dell'insieme insicuro vs filtraggio dei successori).
2. Verdetto di Difendibilità come Output Primario: Elevare la regione vincente da passaggio intermedio a deliverable principale — un certificato formale di difendibilità.
3. Impronta Digitale di Difendibilità: Un artefatto diagnostico unificato che combina sei metriche (cinque formali, una operativa) per caratterizzare le configurazioni di rete.
4. MARL Avversariale con Scudo come Diagnostica: Utilizzare il comportamento post-convergenza del MARL (Rapporto di Dominanza del Difensore) non come metrica di performance dell'agente, ma come diagnostica continua della topologia.
5. Analisi "What-If": Dimostrare che la sicurezza formale e l'efficacia operativa catturano aspetti distinti della sicurezza, rivelando che piccoli cambiamenti architettonici possono spostare drasticamente gli esiti operativi pur lasciando quasi invariati i margini di sicurezza formale.

4. Risultati Sperimentali

Il framework è stato valutato su una topologia di riferimento a 5 host con un bordo di bypass VPN "dimenticato". Sono stati analizzati cinque casi "what-if":

• Baseline: Topologia di riferimento.
• Caso 2 (Totalmente Connessa): Aumento della connettività (da 6 a 13 archi).
• Caso 3 (Distruzioni Illimitate): Rimozione dei vincoli di risorse dell'attaccante.
• Caso 4 ($\phi_D$ Rilassata): Riduzione del requisito minimo di host attivi.
• Caso 5 (VPN Rimossa): Rimozione del bordo specifico di bypass VPN.

Risultati Chiave:

• Disaccoppiamento dei Livelli: Nel Caso 2 (totalmente connessa), le metriche di sicurezza formale (dimensione della Regione Vincente, Attaccabilità) sono rimaste quasi identiche alla baseline. Tuttavia, l'esito operativo (Rapporto di Dominanza del Difensore) è crollato da ~54% a ~23%. Il gioco formale diceva "la sopravvivenza è possibile", ma il livello operativo rivelava che il difensore è sopraffatto.
• Sensibilità ai Singoli Archi: Nel Caso 5 (rimozione del bypass VPN), la dimensione della regione vincente formale è cambiata trascurabilmente (23.730 da 23.858 stati), ma il Rapporto di Dominanza del Difensore è balzato dal 53,9% all'80,7%. Ciò dimostra che un singolo difetto architettonico può rendere un sistema formalmente difendibile ma operativamente indifendibile.
• Perturbazione della Specifica: Il rilassamento dei vincoli (Casi 3 e 4) ha spostato entrambi i livelli in modo coerente, confermando che le specifiche governano la geometria del gioco, che a sua volta detta il comportamento operativo.

5. Significato e Rivendicazioni

Il paper sostiene che la sintesi dello scudo è più preziosa non come meccanismo di deployment per agenti sicuri, ma come framework per rispondere a domande architettoniche.

• Spostamento del Prodotto: L'output è un verdetto di difendibilità e intuizioni strutturali, non una policy sicura. Lo scudo è un testimone derivato, non il deliverable.
• Strumento di Design-Time: Il framework permette agli architetti di chiedere "Questa configurazione è difendibile?", "Quanto è difendibile?" e "Quali cambiamenti migliorano il margine?" con garanzie formali.
• Necessità dei Due Livelli: Il gioco di sicurezza formale e il livello operativo MARL sono necessari e non ridondanti. Un sistema può essere formalmente difendibile (la sopravvivenza è possibile) ma operativamente sopraffatto (la sopravvivenza è praticamente impossibile contro un avversario adattivo).
• Diagnostica Azionabile: L' "Impronta Digitale di Difendibilità" fornisce un modo visivo e quantitativo per confrontare le configurazioni, rivelando che piccoli cambiamenti topologici (come una singola regola del firewall) possono avere impatti operativi massicci che l'analisi statica o la simulazione informale potrebbero mancare.

Gli autori riconoscono i limiti, tra cui la scalabilità dell'analisi a stati espliciti (limitata a piccoli sottosistemi, $|V| \le 7$) e l'assunzione di transizioni deterministiche. Tuttavia, sostengono che per il regime dei piccoli segmenti di rete critici dove vengono prese decisioni architettoniche, il framework fornisce un metodo rigoroso e trattabile per quantificare la difendibilità che gli strumenti esistenti non possono offrire.