I II

Antonio Mattioli

Non-Interferenza eComposizione

delle Policy12-12-2007

Indice

- Modello di Bell-La Padula…………1- Non-Interferenza…………………...4- Unwinding Theorem……………….7- Composizione di Sistemi…………..8- Non-Deducibilità………………….11- Non-Interferenza Forte……………13- Conclusioni………………………..14

IntroDi solito le organizzazioni hanno policy differenti a seconda della struttura a cui sono assegnate. Se ci sono conflitti o necessità differenti, quale policy deve essere adottata? Si possono fondere due policy differenti?

1

- Proprietà di Sicurezza Discrezionale: utilizzo di una matrice per controllare gli accessi

Modello di Bell - La Padula

2

É un modello di policy di sicurezza che definisce un insieme di regole di accesso ad informazioni riservate.

Definizione

Modalità di Accesso ai Dati

Regole

Top Secret

Secret

High

Subjects

Low

Public

Top Secret

Secret

High

Objects

Low

Public

Read

Write

Utilizza una classificazione di sicurezza per gli oggetti ed autorizzazioni per i soggetti.Una modalità di accesso ad un oggetto è permessa solo dopo la comparazione tra classificazione ed autorizzazione.(Livello di Sicurezza)

- Proprietà di Sicurezza Semplice: un soggetto con un certo livello di sicurezza non può accedere ad oggetti a livelli di sicurezza superiori (no read-up)- *-property (proprietà-stella): un soggetto con un livello di sicurezza non può scrivere oggetti con livelli di sicurezza inferiori (no write-down)

Accesso ai Dati

3 Non-Interferenza: Definizione

4

Un gruppo di utenti [...] non-interferisce con un altro gruppo di utenti se quello che il primo gruppo fa [...] non ha effetto su quello che il secondo gruppo può vedere [Goguen, Meseguer]

Definizione

VMASyste

m

Problema

VMBCPU

Sharing

Comunicazione tra A e B

tt2t1t0

ACPU=100%

Send

B=1

ACPU=0%

Send

B=0

ACPU=100%

Send

B=1

Il Sistema

Interferenza

La non-interferenza è un metodo alternativo per costruire modelli di policy di sicurezza

Per ottenere una separazione netta tra i soggetti di un sistema si devono interrompere tutti i canali tra di loro, e non solo quelli che tradizionalmente permettono la trasmissione delle informazioni

5 Non-Interferenza

6

Ogni comando può produrre un output, però alcuni utenti non hanno le autorizzazioni per visualizzarlo

Considerazioni

Non-Interferenza: Esempio

EsempioConsideriamo questo automa:

-Lo stato è definito da due bit: H(igh) e L(ow);

-Due comandi: xor0 e xor1;

-Due utenti: Holly (che può leggere informazioni di tipo High e Low) e Lucy (che può leggere solo informazioni Low);

-L’automa mantiene lo stato con due bit (H,L).

(0,0)

(0,1) (1,0)

(1,1)

xor0

xor1

(0,0)

(0,0)

(0,1)

(0,1)

(1,0)

(1,0)

(1,1)

(1,1)

Gli output dell’automa sono concatenati. L’output per Holly è costituito da entrambi i bit (es. (0,1)) mentre per Lucy solo dal bit Low (es. (1))

Eseguiamo i comandi con alcuni stati:

Questo è l’Automa a Due Bit.

Automa a Due Bit

7 Composizione di Sistemi

8Unwinding Theorem

Idea

Se si riesce a provare che in una sequenza di comandi ogni singolo comando che modifica lo stato di un automa è sicuro, allora lo sarà anche tutta la sequenza

Una transizione è consistente se per ogni c lo stato rimane equivalente rispetto a d

Sia c un comando che secondo la policy r non ha nessun effetto sul dominio d. Se applicando c allo stato corrente non si ottiene alcun effetto su d, allora il sistema rispetta r.

Sia r una policy, X un sistema consistente rispetto all’output ed alle transazioni, e che rispetti al policy r. Allora X è sicuro ripetto alla non-interferenza

Consistenza Transazione

Unwinding Theorem

Rispetto Policy

Sistema

Hughie

Prendiamo in esame questo sistema:

- Louie e Dewey elaborano a livello Low- Hughie elabora a livello High- Tutti possono leggere il buffer di output bL

- C’è un buffer bH per gli input di tipo High- Ci sono tre buffer bLH, bDH, bLDH che connetono i sistemi; possono essere scritti da Louie e Dewey e letti da Hughie- I buffer bDH e bLH hanno capacità 1

Louie

Dewey

bH

bL

bLH

bLDH

bDH

9 Composizione di Sistemi

10

Composizione di Sistemi

In Azione

In questo caso un input di tipo High viene copiato in un buffer che contiene dati di tipo Low.Questo sistema non è sicuro rispetto alla non-interferenza

Hughie

Louie

Dewey

0

0

0

0

1

Non-Interferenza

Ognuno dei tre sistemi è sicuro rispetto alla non-interferenza:-Hughie non ha output, quindi gli input non possono interferire.-Louie e Dewey non hanno input, quindi non c’è interferenza con gli output.

Houghie legge un bit da bH, riceve un messaggio da bLH (se legge 0 da bH) o da bDH (se legge 1 da bH) e poi riceve da bLDH.

Esempio

-Luoie invia un messaggio a bLH. Il buffer è pieno-Louie invia un secondo messaggio a bLH

-Louie manda uno 0 a bL

-Luoie manda un messaggio a bDLH per segnalare ad Houghie che Louie ha completato un ciclo

Dewey segue la stessa procedura con bDH al posto di bLH e invia 1 a bL

bLH

bH

bLDH

bL

11

Non-Deducibilità

12

Lucy può visualizzare solo i bit Low, cioè

0001111Questa funzione non è sicura rispetto alla non-interferenza; infatti eliminando i comandi di Holly, l’output per Lucy dovrebbe essere

00111In quest’ultimo caso Lucy non può dedurre quali istruzioni sono state eseguite e poi cancellate, perché non hanno influenzato l’output (ma solo la sua lunghezza)

Considerazioni

Non-Deducibilità

H,xor1

L,xor1L,xor0

H,xor1

H

L

(1,0)

(1,1)

(0,1)

L,xor0 L,xor0

(1,0)

(1,1)

(0,0)

IS

Un sistema è non-deducibile se, analizzando gli output, un utente non può dedurre gli input di un altro utente

Se un utente Low, che può inserire e ottenere solo dati di tipo Low, da questi riesce a dedurre i dati High, allora i dati sono trapelati da High a Low.

Adesso consideriamo l’automa a due bit visto in precedenza, però con alcune modifiche:-Due set di input: High e Low;-Due set di output: High e Low;

Introduciamo un’altra modifica: se Holly esegue un’operazione, cambia solo il bit High, se invece è Lucy a farlo, varia solo il bit Low.

Lo stato iniziale è (0,0), i comandi eseguiti sono:(Holly,xor1), (Lucy,xor0), (Lucy,xor1), (Lucy,xor0), (Holly,xor1), (Lucy,xor0).L’output risultante è

00101011110101compreso lo stato iniziale. I bit dispari sono gli High, i pari sono i Low

Premessa

(0,1)

(0)

(1)

(1)

(0)

(1)

(0)

(1)

Definizione

13

Conclusioni

14

Conclusioni

Non-Interferenza Forte

Premessa

La Non-Interferenza è una formulazione alternativa di modelli di policy di sicurezza; una separazione stretta tra i soggetti può avvenire solo se tutti i canali sono chiusi.La composizione di sistemi che presi singolarmente sono sicuri non sempre ha come risultato un sistema sicuro, ma ha sempre bisogno di modifiche ed ottimizzazioni, anche per garantire l’autonomia degli oggetti che lo compongono

In generale (ma non lo dimostriamo), i sistemi non-deducibili non sono componibili.C’è una modifica che permette la composizione

- Studiare come approssiamare il minimo numero di operazioni negate che permettono il massimo livello di sicurezza ed autonomia- I sistemi non deducibili non incorporano la probabilità degli eventi

Non-Interferenza Forte

Nessun output di tipo High viene prodotto senza un input di tipo High

Nell’automa a due bit un’operazione modifica solo il bit corrispondente, però invia all’output sia il bit High che quello Low; se invece inviasse all’output solo il bit del livello dell’operazione, allora soddisferebbe la non-interferenza forte

Esempio

Conclusione

Si può dimostrare (ma non in questa sede) che dei sistemi che soddisfano la non-interferenza forte sono componibili tra di loro mantenendo il requisito della non-interferenza [Weber]

Campi di Studio

III IV

Antonio Mattioli

Non-Iterferenza eComposizione

delle Policy12-12-2007

Bibliografia

-libro, di ---, capitolo 8

-Abstract Non-Interference, di Mastroeni

-Varie, risorse in rete

Grazie per l’Attenzione.Domande?