Nozioni di Opacità e Osservabilità Critica, esatte e approssimate per sistemi di transizione metrici

Università degli Studi dell'Aquila

Ingegneria

di laurea in Ingegneria dell'informazione

Tesi

Nozioni di opacità e osservabilità critica, esatte e approssimate per sistemi di transizione metrici

Relatori: Prof.ssa Elena De Santis, Prof. Giordano Pola

Laureando: Gino Ventura

Matricola: 249319

Anno Accademico 2018-2019

Indice

• Introduzione
• Capitolo 1. Concetti fondamentali
  • 1.1 Modelli per i sistemi
• Capitolo 2. Opacità esatta e approssimata
  • 2.1 Opacità agli stati iniziali
  • 2.2 Opacità agli stati correnti
  • 2.3 Opacità ad infiniti step
• Capitolo 3. Osservabilità critica esatta e approssimata
  • 3.1 Osservabilità critica agli stati iniziali
  • 3.2 Osservabilità critica agli stati correnti
  • 3.3 Osservabilità critica forte agli stati iniziali
  • 3.4 Osservabilità critica forte agli stati correnti
• Capitolo 4. Stimatori
  • 4.1 Stimatore agli stati iniziali
  • 4.2 Stimatore agli stati correnti
• Capitolo 5. Esempi sull'analisi dell'opacità e dell'osservabilità critica
  • 5.1 Costruzione degli stimatori
  • 5.2 Analisi degli stimatori e condizioni da verificare
    • 5.2.1 Condizioni sull'opacità (esatta e approssimata) sull'osservabilità critica (esatta e approssimata)
    • 5.2.2 Condizioni
  • 5.3 Applicazioni pratiche: Opacità e Osservabilità critica esatte
  • 5.4 Applicazioni pratiche: Opacità e Osservabilità critica δ-approssimate
• Conclusioni
• Bibliografia
• Appendice A: Calcoli sulle nozioni esatte
• Appendice B: Calcoli sulle nozioni approssimate
• Appendice C: Dimostrazioni delle nozioni forti dell'Osservabilità critica

Introduzione

I sistemi cyber-fisici (Cyber-Physical-Systems, CPS) sono sistemi derivanti da strette interazioni di sistemi dinamici e dispositivi computazionali. Tali sistemi sono generalmente molto complessi e presentano comportamenti sia continui che discreti, il che rende la verifica e la progettazione di tali sistemi significativamente impegnative. In particolare, le componenti di CPS sono generalmente collegate tramite reti di comunicazione per acquisire e scambiare informazioni in modo da poter ottenere alcune funzionalità globali del sistema. Tuttavia, questo porta anche nuove sfide per la verifica e la progettazione di CPS, poiché la comunicazione tra il sistema e le componenti, può rilasciare informazioni che potrebbero compromettere la sicurezza dell'intero sistema. Pertanto, è importante poter determinare quali informazioni possano essere rilasciate e quali no.

Vengono dunque esaminate due importanti proprietà di sicurezza del flusso di informazioni, chiamate opacità e osservabilità critica. In parole povere, l'opacità è una proprietà di riservatezza legata al sistema stesso, che rileva se il "segreto" possa essere rivelato o meno ad un intruso (il quale deduce il comportamento reale del sistema in base al flusso di informazioni che acquisisce). L'osservabilità critica è invece una proprietà di sicurezza, legata a delle dinamiche "critiche", ovvero a dei malfunzionamenti del sistema (le quali devono essere individuabili e distinguibili).

In questa tesi, le due proprietà verranno studiate più approfonditamente nel contesto di sistemi ad eventi discreti (Discrete-Event Systems, DES), un'importante classe di sistemi dinamici guidati da eventi con spazi di stato discreti. Poiché l'opacità e l'osservabilità critica sono delle proprietà del flusso di informazioni, la loro definizione dipende strettamente dal modello informativo del sistema. In generale, un sistema si dice opaco se qualsiasi suo comportamento segreto risulta celato e difficilmente individuabile; differentemente, un sistema si dice criticamente osservabile se le criticità possono essere sempre indubbiamente individuabili.

Per l'analisi delle due proprietà, viene adottato un modello basato sull'osservazione degli eventi, ovvero alcuni eventi del sistema (etichette di stato) sono osservabili o distinguibili mentre alcune non lo sono. È possibile, ad esempio, analizzare tali proprietà su un sistema ad output simbolico, ovvero un sistema le cui uscite sono associate a dei livelli logici, in cui è possibile distinguere con precisione due uscite con etichette diverse. Le proprietà di opacità e di osservabilità critica associate a questa classificazione di sistemi, vengono denominate "esatte".

L'analisi delle proprietà esatte risulta essere molto significativa per i sistemi i cui set di output non sono metrici, ad esempio sistemi discreti le cui uscite sono, appunto, eventi logici. Tuttavia, per molte applicazioni del mondo reale le cui uscite sono segnali fisici, invece di dire semplicemente che due eventi sono distinguibili o indistinguibili, è possibile effettuare una misurazione per valutare quantitativamente la vicinanza di due risultati. Tali sistemi sono indicati come sistemi metrici, in cui gli insiemi delle uscite sono dotati di metriche appropriate. Per i sistemi metrici, se due segnali sono molto vicini tra loro, sarà molto difficile distinguerli in modo univoco a causa della precisione di misurazione o di potenziali rumori e disturbi di misurazione. Pertanto, le definizioni esatte di opacità e osservabilità critica risultano essere troppo forti per i sistemi metrici poiché implicitamente si assume che si possa sempre distinguere due segnali di uscita anche quando sono arbitrariamente vicini l'uno all'altro.

In [01] viene proposto un nuovo concetto chiamato opacità approssimata che è applicabile ai sistemi metrici. In particolare, vengono trattate due uscite come uscite "indistinguibili" se la loro distanza (misurata) è inferiore a un dato parametro di soglia δ ≥ 0, in cui δ rappresenta la precisione con cui l'intruso è obbligato a misurare le uscite per poterle distinguere. Vengono considerate tre tipologie di opacità:

• Opacità δ-approssimata agli stati iniziali: Richiede che l'intruso non possa mai distinguere se l'evoluzione del sistema abbia origine da uno stato segreto.
• Opacità δ-approssimata agli stati correnti: Richiede che l'intruso non possa mai distinguere se il sistema raggiunga uno stato segreto.
• Opacità δ-approssimata a step infiniti: Richiede che l'intruso non possa mai determinare se il sistema sia in uno stato segreto per una qualsiasi evoluzione del sistema, se la sua precisione di misura non è superiore a δ.

Intuitivamente, invece di richiedere l'opacità esatta a tutto il sistema, le opacità δ-approssimate forniscono delle versioni rilassate (più deboli) di opacità.

L'osservabilità critica "esatta", introdotta in [04], viene trattata ed implementata allo stesso modo; considerando infatti una tolleranza δ ≥ 0 legata a errori o a potenziali disturbi durante la misurazione delle uscite, è possibile definire delle forme di osservabilità critica meno restrittive, e meglio applicabili a sistemi metrici. Vengono implementate due nozioni di osservabilità critica basate sulle etichette di stato:

• Osservabilità critica δ-approssimata agli stati iniziali: Richiede che l'osservatore sia sempre in grado di determinare se l'evoluzione del sistema sia stata originata da uno stato critico.
• Osservabilità critica δ-approssimata agli stati correnti: Richiede che l'osservatore sia sempre in grado di determinare se il sistema raggiunga uno stato critico.

Dalle nozioni esatte introdotte in [04], vengono implementate anche due nuove forme di osservabilità critica, denominate "forti". L'asserzione a tali proprietà permette non solo di determinare quando il sistema si trovi in uno stato critico, ma anche di distinguere le diverse criticità che possono coesistere in uno stesso sistema. Le nozioni forti dell'osservabilità critica vengono anch'esse analizzate servendosi della tolleranza δ ≥ 0. Chiaramente, le nozioni approssimate di opacità e osservabilità critica, si riducono fino a quelle esatte quando δ = 0.

Lo studio dell'opacità e dell'osservabilità critica di un sistema viene successivamente affrontato attraverso le tecniche proposte in [01], le quali prevedono la costruzione di un nuovo sistema denominato "stimatore di stato", che tiene traccia di tutti i possibili stati coerenti con l'osservazione. L'utilizzo di questi nuovi sistemi permette di determinare a quali nozioni di opacità e osservabilità critica il sistema riesce ad asserire; lo scopo principale è quello di riuscire a determinare se, e in che modalità, le diverse nozioni risultino affermate. La variazione del parametro δ permette di comprendere come mutino le nozioni di opacità e quelle di osservabilità critica nel caso di sistemi "reali". Durante lo studio delle nozioni approssimate, si avranno dunque diversi stimatori, ottenuti tramite variazione della tolleranza δ.

L’analisi dei sistemi avviene considerando la "vicinanza tra due segnali di uscita", in cui le uscite sono, come già introdotto, basate sugli stati; la metrica utilizzata per determinare la distanza tra due uscite, è la medesima introdotta in [01]. Oltretutto, dal momento che le uscite sono basate sugli stati, le transizioni che permettono al sistema di evolvere vengono considerate generiche; come verrà successivamente introdotto, la costruzione degli stimatori non dipende dal tipo di transizione, ma dalla generica possibilità di avere una transizione a partire da uno stato. Si suppone dunque che l’osservatore possa distinguere l’evoluzione del sistema, unicamente dalle etichette di uscita associate agli stati.

Capitolo 1. Concetti fondamentali

1.1 Modelli di Sistemi

La nozione di "sistema" introdotta in [02] permette di descrivere sia sistemi di controllo a spazio continuo che sistemi di controllo a spazio finito; tale nozione verrà impiegata per la rappresentazione di un Cyber-Physical-System.

Definizione 1.1: Un sistema S è una tupla S = (X, X₀, U, →, Y, h) in cui:

• X è l’insieme degli stati
• X₀ è l’insieme degli stati iniziali, X₀ ⊆ X
• U è l’insieme degli ingressi
• → ⊆ X × U × X è la funzione di transizione
• Y è l’insieme delle uscite
• h: X → Y è la funzione di uscita

Un sistema S viene detto metrico se l’insieme delle uscite Y è dotato di una metrica d. Un sistema S viene detto finito se gli insiemi X e U hanno cardinalità finita. Una transizione viene anche indicata come (x, u) → x′, x′ ∈ Post(x, u). L’insieme di tutti gli stati raggiungibili da x a fronte di un ingresso u viene indicato come Post(x), analogamente l’insieme di tutti gli stati che eccitano lo stato x a fronte di un ingresso u viene indicato come Pre(x).

Capitolo 2. Opacità esatta e approssimata

La riservatezza di un sistema è riferita alla possibilità di occultare delle informazioni, che non devono poter essere acquisite da un intruso per non compromettere l’integrità del sistema stesso. La "segretezza" dell’informazione viene formulata basandosi sugli stati, i quali non devono poter essere identificabili durante l’evoluzione del sistema. Specificatamente, si assume che S₀ ⊆ X sia l’insieme degli stati segreti; un sistema S = (X, X₀, U, →, Y, h) con stati segreti viene descritto da una nuova tupla S₀ = (X, X₀, S₀, U, →, Y, h).

Al fine di determinare la sicurezza di un sistema, vengono esaminate tre diverse nozioni di opacità, associate sia al concetto di opacità esatta sia al concetto di opacità δ-approssimata rivisitata in [01].

2.1 Opacità agli stati iniziali

Tale proprietà richiede che non si possa mai determinare se una traiettoria di stato finita sia stata generata a partire da uno stato iniziale segreto.

Definizione 2.1.1 (Opacità esatta agli stati iniziali): Un sistema S = (X, X₀, U, →, Y, h) si dice opaco agli stati iniziali se e se per ogni traiettoria di stato finita x₀u₀ → x₁u₁ → ... → x_n-1u_n-1 → x_n, con x₀ ∈ X₀ ∩ X_S, esiste un x′₀ ∈ X₀ \ X_S ed una nuova traiettoria di stato finita x′₀u′₀ → x′₁u′₁ → ... → x′_n-1u′_n-1 → x′_n, tale che h(x_i) = h(x′_i) per ogni i = 0, 1, ..., n.

Definizione 2.1.2 (Opacità δ-approssimata agli stati iniziali): Sia S un sistema dotato di metrica d definita sull’insieme delle uscite Y, e sia δ ≥ 0 una costante. Il sistema S = (X, X₀, U, →, Y, h) si dice opaco agli stati iniziali se e se per ogni traiettoria di stato finita x₀u₀ → x₁u₁ → ... → x_n-1u_n-1 → x_n, con x₀ ∈ X₀ ∩ X_S, esiste un x′₀ ∈ X₀ \ X_S ed una nuova traiettoria di stato finita x′₀u′₀ → x′₁u′₁ → ... → x′_n-1u′_n-1 → x′_n, tale che max{d(h(x_i), h(x′_i)) | i ∈ {0, ..., n}} ≤ δ.

2.2 Opacità agli stati correnti

Tale proprietà richiede che non si possa mai determinare se una traiettoria di stato finita giunga ad uno stato segreto.

Definizione 2.2.1 (Opacità esatta agli stati correnti): Un sistema S = (X, X₀, U, →, Y, h) si dice opaco agli stati correnti se e se per ogni traiettoria di stato finita x₀u₀ → x₁u₁ → ... → x_n-1u_n-1 → x_n, con x_n ∈ X_S, esiste un x′_n ∈ X \ X_S ed una nuova traiettoria di stato finita x′₀u′₀ → x′₁u′₁ → ... → x′_n-1u′_n-1 → x′_n, tale che h(x_i) = h(x′_i) per ogni i = 0, 1, ..., n.

Definizione 2.2.2 (Opacità δ-approssimata agli stati correnti): Sia S un sistema dotato di metrica d definita sull’insieme delle uscite Y, e sia δ ≥ 0 una costante. Il sistema S = (X, X₀, U, →, Y, h) si dice opaco agli stati correnti se e se per ogni traiettoria di stato finita x₀u₀ → x₁u₁ → ... → x_n-1u_n-1 → x_n, con x_n ∈ X_S, esiste un x′_n ∈ X \ X_S ed una nuova traiettoria di stato finita x′₀u′₀ → x′₁u′₁ → ... → x′_n-1u′_n-1 → x′_n, tale che max{d(h(x_i), h(x′_i)) | i ∈ {0, ..., n}} ≤ δ.