1 Parallelismo, nondeterminismo e sicurezza dei programmi Approfondimento per il corso di Semantica...

1

Parallelismo, nondeterminismo e sicurezza dei programmi

Approfondimento per il corso di Semantica dei Linguaggi di Programmazione A.A.

2006/07

Prof.ssa Annalisa BossiAutore: Elia Gaglio (matricola n° 809477)

21/05/2007

2

Obiettivi e step dell’approfondimento:

Fornire una panoramica sui passi fondamentali che hanno portato alla definizione di linguaggi di programmazione che sfruttino il parallelismo Definizione di una semantica per i comandi di composizione parallela

Valutazione del nondeterminismo del linguaggio che viene introdotto

Definizione del linguaggio di Dijkstra dei “comandi con guardia”

Definizione del linguaggio per “Processi Comunicanti”

CCS (Calculus of Communicating System) di Milner

Presentazione di un framework per definire dei flussi di informazioni sicuri in programmi concorrenti Definizione di uno schema generale di unwinding e di insiemi di proprietà istanziabili da esso

Istanziazioni delle proprietà precedenti in scenari che prevedono “Information Release” intenzionali

Definizione di un insieme di tecniche di verifica per proprietà composizionali di noninteference

3

Parallelismo & nondeterminismo [1]:

Per trattare gli elementi di base dei linguaggi di programmazione paralleli è necessario estendere IMP inserendo il costrutto di composizione parallela:

dati c0, c1 Com si definisce: c0 || c1

<c0, > 1 ’ <c0, > 1 <c0’, ’>

<c0||c1, > 1 <c1, ’> <c0||c1, > 1 <c0’||c1, ’>

<c1, > 1 ’ <c1, > 1 <c1’, ’>

<c0||c1, > 1 <c0, ’> <c0||c1, > 1 <c0||c1’, ’>

Si noti che si è utilizzata una semantica one-step

4

Parallelismo & nondeterminismo [2]:

Il parallelismo porta ad un ovvio nondeterminismo del linguaggio

Ciò è visibile con questo semplice esempio:

P1 (x:=0 || x:=1); if(x=0) then c0 else c1

Nondeterminismo = elemento ineliminabile nella programmazione parallela (sia nei semplici programmi che in sistemi complessi)

Però è possibile trarre vantaggio dal nondeterminismo…

5

I “comandi con guardia” [1]:

IDEA: un utilizzo disciplinato del nondeterminismo può portare allo sviluppo di algoritmi più immediati.

Introduzione del linguaggio di Dijkstra dei “comandi con guardia”

Si usa un costrutto nondeterministico per liberare il programmatore dalla necessità di specificare nei dettagli un metodo di soluzione

Estensione del linguaggio IMP:

c ::= skip | abort | x:=a | c0;c1 | if gc fi | do gc od

gc ::= b c | gc0 gc1 un comando con guardia ha la forma:

(b1 c1) … (bn cn)

6


Regole per i comandi (estensioni):

<gc, > <c, ’> nel caso gc fallisca si ha (if gc fi) abort

<if gc fi, > <c, ’>

<gc, > fail <gc, > <c, ’>

<do gc od, > <do gc od, > <c; do gc od, ’>

7


Regole per i comandi con guardia:

<b, > true <b, > false

 <c, > fail

<gc0, > <c, ’> <gc1, > <c, ’>

<gc0 gc1, > <c, ’> <gc0 gc1, > <c, ’>

<gc0, > fail <gc1, > fail

<gc0 gc1, > fail

8


Esempio: definire un comando C che assegna il valore massimo fra due locazioni X e Y e una locazione MAX:

C if

X ≥ Y MAX := X

Y ≥ X MAX := Y

fi

La simmetria tra X e Y sarebbe persa in un qualsiasi programma IMP tradizionale

9

Processi comunicanti:

Seconda metà degli anni ’70 – Hoare & Milner: definizione di un insieme di primitive di comunicazione innovative

IDEA: primitiva di comunicazione indipendente dal mezzo di comunicazione

utilizzo di un azione atomica di sincronizzazione (con scambio di valori)

Processi comunicanti mediante canali

Accesso ristretto ai canali comunicazione locale a 2 o più processi

Un processo può essere pronto in input/output su un dato canale

Comunicazione possibile se esiste un processo nel suo ambiente che esegue l’azione complementare di input/output

Assenza di buffer

10

Linguaggio per processi comunicanti [1]:

SINTASSI:

Loc Aexp Bexp nomi di canali: , , , … Chan

espressioni di input: ?X con X Loc

espressioni di output: !a con a Aexp

Comandi:

c ::= skip | abort | x:=a | ?X | !a | c0;c1 | if gc fi | do gc od | c0 || c1 | c \

Comandi con guardia:

gc ::= b c | b ?X c | b !a c | gc0 gc1

11


Come si può formalizzare il comportamento di questo linguaggio?

<?X;c, > la comunicazione avviene se in parallelo c’è un comando pronto

ad eseguire un azione complementare di output sul canale

La semantica deve esprimere questa dipendenza dall’ambiente:

<?X;c0, > <c0, [n/X]> <!e;c1, > <c1, > (hyp. <e, > n)

?n !n

La comunicazione è possibile se i 2 comandi sono posti in parallelo:

<(?X;c0) || (!e;c1), > <c0 || c1, [n/X]>

<(?X;c0) || (!e;c1), > <c0 || (!e;c1), [n/X]>

<(?X;c0) || (!e;c1), > <(?X;c0) || c1, [n/X]>

?n

!n

il primo componente riceve un valore dall’ambiente

il secondo componente spedisce un valore che viene ricevuto dall’ambiente

transizione non etichettata perché non ha effetti sull’ambiente

12



<?X, > [n/X] <a, > n <gc, > <c, ’>

<!a, > <if gc fi, > <c, ’>

<gc, > <c, ’> <gc, > fail

<do gc od, > <c; do gc od, ’> <do gc od, >

<c0, > <c0’, ’> <c1, > <c1’, ’>

<c0 || c1, > <c0’ || c1, ’> <c0 || c1, > <c0 || c1’, ’>

!n, ?n,

(transizioni etichettate / transizioni non etichettate)

!n

?n

13



<c0, > <c0’, ’> <c1, > <c1’, > <c, > <c’, ’>

<c0 || c1, > <c0’ || c1’, ’> <c \ , > <c’ \ , ’>

<c0, > <c0’, > <c1, > <c1’, ’>

<c0 || c1, > <c0’ || c1’, ’>

?n

?n

!n

!n

?n e !n

14


Regole per i comandi con guardia (estensioni):

<b, > true <b, > true <a, > n

 <c, [n/X]> <c, >

<b, > false <b, > false

 fail fail

?n !n

15

Processi comunicanti - esempi:

P1 if (true ?X c0) (true ?Y c1) fi

scelta nondeterministica del canale (se il processo volesse ricevere da entrambi i canali disponibili)

P2 if (true ?X;c0) (true ?Y;c1) fi

possibilità di deadlock se si sceglie il ramo destro e l’ambiente può eseguire output solo sul canale

16

Il CCS di Milner [1]:

CCS (Calculus of Communicating System): modello che ha avuto un forte impatto sullo studio teorico del parallelismo

Derivabile dai linguaggi precedenti eliminando alcune caratteristiche dei linguaggi imperativi

Un processo CCS comunica con il suo ambiente attraverso i canali connessi alle sue porte

processo p

?

!

? !

p \ {, }

17


Possibilità di effettuare la composizione parallela di processi

Possibilità di utilizzare più copie dello stesso processo

funzione di ridenominazione funzione sui nomi dei canali

?

!

? !processo p

p p[f]

dove si ha:

f() =

f() =

f() =

?

?

!

processo p[f]

18


Oltre alle comunicazioni ?n e !n esiste anche la comunicazione che può svolgere il ruolo del comando skip o azioni di comunicazione interna

In pratica denota un’azione non osservabile, mentre in L vi sono le azioni visibili agli altri processi (Act = L )

SINTASSI DEI PROCESSI:

p ::= nil | ( p) | (!a p) | (?X p) | (b p) | p0 + p1 | p0 || p1 | p \ L | p[f] | P(a1, …, ak)

19


SEMANTICA DEI PROCESSI:

Per rappresentare il comportamento di un processo si associa un sistema di transizione etichettato (labeled transition system = LTS)

LTS correlate al concetto di stato e transizione

LTS (P, Act, ) P è l’insieme dei processi (stati)

Act è l’insieme delle azioni (etichette)

è una relazione di transizione Act

Esempio:

P1 P2 P1 compie un’azione e si trasforma in P2

20


Processo nil: no regole (non esegue nessuna azione!)

Prefisso: ( p) p

a n b true p p’

(!a p) p (b p) p’ (?X p) p[n/x]

Somma: p0 p0’ p1 p1’

p0 + p1 p0’ p0 + p1 p1’

Restrizione: p p’ dove se ?n o !n allora L

p \ L p’ \ L

?n, !n,

!n

?n

21

Composizione: p0 p0’ p0 p0’ p1 p1’

p0 || p1 p0’ || p1 p0 || p1 p0’ || p1’

p1 p1’ p0 p0’ p1 p1’

p0 || p1 p0 || p1’ p0 || p1 p0’ || p1’

Ridenominazione: p p’

p[f] p’[f]

Identificatori: p p’ dove X := p p[a1/X1,…,ak/Xk] p’ P(x1,..,Xk)=p

X p’ P(a1,…,ak) p’


?n

?n

!n

!n

f()

def def

22


Le transizioni definite nella semantica precedente sono associate a processi che NON contengono variabili libere

non è necessario utilizzare il concetto di ambiente per variabili

in Aexp e Bexp si hanno variabili al posto delle locazioni

(?X (!X nil))

(?X (!X nil)) (!X nil)[n/X]

che equivale a: (?X (!X nil)) (!n nil)

(!n nil) nil

!n

?n

?n

qui la variabile X è già legata ad un particolare numero n

23

Problematiche nelle esecuzioni concorrenti:

Sfruttare la concorrenza nelle esecuzioni di programmi introduce però alcune problematiche da dover considerare esplicitamente:

possibilità di accessi alle stesse variabili

interpretazione dei comandi eseguiti non sempre certa

mancanza di protezione in insiemi di dati confidenziali

Necessario un controllo del flusso delle informazioni in modo da verificare che le informazioni considerate segrete non siano trasmesse a parti non autorizzate

introdurre dei livelli di sicurezza alle informazioni di un sistema

“noninterference principle”

24

Flussi di informazione sicuri in programmi concorrenti - introduzione

Introduzione di un unwinding framework che definisce proprietà di sicurezza su flussi di informazione, descritto in linguaggio imperativo esteso [Bossi – Piazza – Rossi]

Studio di diverse classi di programmi, ottenuti mediante differenti istanziazioni del framework

Valutazione di diverse proprietà di sicurezza che garantiscano il “noninterference principle”

Estensione dell’ unwinding condition per modellare proprietà di sicurezza in sistemi che prevedono il rilascio intenzionale di informazioni

Definizione di sistemi di prova per decidere le proprietà di sicurezza sui programmi

25

Flussi di informazione sicuri in programmi concorrenti – sintassi e semantica [1]:

Il linguaggio utilizzato è un linguaggio imperativo esteso, dove:

livello pubblico (L)

livello confidenziale (H)

SINTASSI:

a ::= n | X | a0+a1 | a0-a1 | a0*a1 dove X L H

b ::= true | false| (a0=a1) | (a0≤a1) | b | b0 b1 | b0 b1

S ::= skip | X:=a | S0;S1

P ::= S | P0;P1 | if(b) then {P0} else {P1} | while(b) {P} | await (b) {S} |

co P1 || … || Pn oc

locazioni (Loc) L H =

26

SEMANTICA OPERAZIONALE:

strettamente legata al concetto di stato: L H Z

espressa in termini di LTS: <P, > <P’, ’> dove P’ = {P end}

e {high, low}

<P0, 0> <Pn, n> <P0, 0> <Pn, n>

Estensioni della Semantica di IMP introdotte:

<b, > true <S, > <end, ’>

<skip, > <end, > <await (b) {S}, > <end, ’> b 1

=l l = l

low high


low

2

1 2

27


<b, > false

<await (b) {S}, > <await (b) {S}, > b

<Pi, > <Pi’, ’>

<co P1 || … || Pi || … || Pn oc, > <co P1 || … || Pi’ || … || Pn oc, ’>

<co end || … || end || … || end oc, > <end, >

low

28

Introduzione della relazione binaria Reach e Reach* su P:

(P, Q) Reach , ’ tali che <P, > → <P’, ’>

Q Reach*(P) n ≥ 0, 0, …, n-1, 0, …, n-1 t.c <P, 0> <P1, 0>

<P1, 1> <P2, 1>

…

<Pn-1, n-1> <Q, n-1>

Reach*(P) è ottenuto riducendo P, permettendo cambiamenti aribitrari nella memoria durante la derivazione (legato al concetto di threads)

P if (L=1) {P’} else {skip}

P’ if (L≠1) {L:=2} else {skip}

possiamo definire: Reach(P) = {P, P’, skip}

Reach*(P) = Reach(P) {L:=2}

29

E’ importante valutare se 2 programmi sono indistinguibili per un low-level observer (nozione di behavioural equivalence)

P H:=1; L:=1 e si definisca

Q H:=2; L:=H-1

<H:=1; L:=1, > <H:=2; L:=H-1, >

<L:=1; [H/1]> <L:=H-1; [H/2]>

<end, [H/1, L/1]> <end, [H/2, L/1]>

I 2 programmi sono equivalenti per un low level observer

Questa proprietà è catturata dalla nozione di low level bisimulation

low

low

low

high

30

Low Level Bisimulation (): relazione binaria simmetrica B su P X t.c. per ogni (<P, >, <Q, >) B si ha che:

=l

se <P, > <P’, ’> allora esiste <Q’, ’> t.c. <Q, > <Q’, ’>

Strong Low Level Bisimulation (): relazione binaria simmetrica B su P t.c. per ogni (P, Q) B si ha che:

per ogni , t.c. =l se <P, > <P’, ’> allora esiste <Q’, ’> t.c. <Q, > <Q’, ’>, ’ =l’ e (P’, Q’) B

E’ immediato provare che la relazione di Strong Low Level Bisimulation è più forte () della relazione di Low Level Bisimulation


P’ e Q’ devono essere equivalenti per ogni , t.c. =l

31

Riprendiamo l’esempio visto prima e vediamo di applicare le definizioni introdotte nella slide precedente:

P H:=1; L:=1 e si definisca

Q H:=2; L:=H-1

<H:=1; L:=1, > <H:=2; L:=H-1, >

<L:=1; [H/1]> <L:=H-1; [H/2]>

<end, [H/1, L/1]> <end, [H/2, L/1]>

I 2 programmi sono low level bisimilar (i valori di L sono equivalenti)

Ma non sono strong low level bisimilar (cambiando [H/5] si otterrebbero valori differenti per L). Ciò riflette il fatto che:

Sia R H:=5 co P || R oc co Q || R oc


low

low

low

high

32

Flussi di informazione sicuri in programmi concorrenti – generalized unwinding condition ed istanziazioni [1]:

Si utilizza una generalized unwinding condition per definire classi di programmi parametrici a:

= relazione binaria che valuta se 2 stati sono indistinguibili per un low

level observer;

= relazione binaria che valuta se 2 coppie <P, >, <Q, > sono

indistinguibili per un low level observer;

R relazione binaria di Reachability che associa a ciascuna coppia <P, >

tutte le coppie <F, > raggiungibili da <P, >

.

.

.

33


<P, > soddisfa l’ unwinding framework se:

<F, > <G, > {t.c. <F, > Reach(P)} non vi sono effetti sull’ osservazione di un utente low level

Equivalentemente: “ogni high level transition deve essere vista come una transizione indipendente, garantendo che un low level observer non possa capire che tipo di transizione sia occorsa” ( high level transitions non hanno influenza sulle low level observation)

high

34

La nozione di generalized unwinding è il punto di partenza per definire:

unwinding class: W(=, =, R)

E’ possibile istanziare la unwinding class, in modo da trattare diverse classi di programmi concordanti con il “noninterference principle”. Ad esempio:

SIMPl class: W(=l, l, →)

SIMPl* class: W(=l, l, Reach*)

Le classi SIMPl* SIMPl non sono composizionali rispetto

l’operatore di composizione parallela

. ..

SIMPl* SIMPl

P if(H=1) {P0} else {P1}

P0 L:=1; if(L=1) {L:=2} else {L:=3}

P1 L:=1; skip; L:=2;

Vale la relazione P SIMPl*

Q L:=0

Vale la relazione Q SIMPl*

Si consideri ora: co P||Q oc

=l, (H)=1 e (H)=0

quindi: <co P||Q oc, > <co P0||Q oc, > … (L) = 3

<co P||Q oc, > <co P1||Q oc, > … (L) 3

SIMPl*

35


La composizionalità è una proprietà utile ed importante (è possibile lavorare con i sottoprogrammi ed “estendere” la proprietà all’intero programma)

SIMP* class: W(=l, l, Reach*)

dove è una relazione binaria t.c. <P, > <Q, > se =l e P l Q

La classe SIMP* è più restrittiva delle classi precedentemente introdotte. Infatti vale che: l l

Inoltre SIMP* gode di importanti proprietà composizionali utili per lo sviluppo di tecniche automatiche di verifica

..

.. ..

SIMP* SIMPl*

SIMPl

..

Teorema di composizionalità:

Siano (ah, bh) h.l.e. e (al, bl) l.l.e. e (P0, P1, S) SIMP* allora:

1) skip

2) L:=al, H:=ah, H:=al;

3) P0; P1

4) if (bl) {P0} else {P1}

5) if (bh) {P0} else {P1} se P0 l P1

6) while (bl) {P0}

7) await (bl) {S}

8) co P0 || P1 oc

SIMP*

36

Flussi di informazione sicuri in programmi concorrenti – Delimited Information Release

La noninterferenza è una proprietà troppo forte per le applicazioni pratiche

Necessità di prevedere rilasci, declassificazioni di informazioni segrete

Esempio: D= {H1 > 5, H1 + H2} D= {Aexp, Bexp}

Anche le informazioni ottenute combinando gli elementi di D saranno degradate: (2H1 – 10 >0), (H2 + H1 + 1) (D)

Definizione: =l,D se =l e (d D) <d, > c sse <d, > c

E’ perciò possibile istanziare la condizione di “generalized unwinding” in un contesto che tenga conto della declassificazione di informazioni. Ad esempio:

SIMPD* class: W(=l,D, l,D, Reach*)

..

P L:=H1; H1:=H2

D={H1}

P SIMPD* infatti H1:=H2 assegna un high value ad una variabile

degradata

37

Flussi di informazione sicuri in programmi concorrenti – Tecniche di verifica [1]:

In generale è problematico decidere se un programma appartiene ad una determinata unwinding class

Teorema: La relazione l è non decidibile

Dimostrazione: per dimostrare la non decibilità della relazione è possibile

ridurre il problema della strong l.l. bisimulation al decimo

problema di Hilbert

Per superare questo problema è possibile introdurre una nuova relazione…

Gli “ingredienti” sono i risultati sulla decidibilità delle formule del prim’ordine di Tarski sui reali e un mapping interi reali…

38

Flussi di informazione sicuri in programmi concorrenti – Tecniche di verifica [2]:

E la una nuova definizione delle nozioni di stato e di stati low level equivalent:

r : L H r =l r

Relazione (l su Aexp Bexp Prog)

Lemma: La relazione l è decidibile e si comporta come la relazione l

E’ anche possibile definire una relazione decidibile per sistemi che prevedono declassificazione di informazioni

Relazione (l,D su Aexp Bexp Prog)

Lemma: La relazione l,D è decidile e si comporta come la relazione l,D

39

Bibliografia:

La Semantica Formale dei Linguaggi di Programmazione – Glynn Winskel – The MIT Press

Communication and Concurrency – Robin Milner – Prentice Hall

Compositional Information Flow Security for Concurrent Programs – Annalisa Bossi, Carla Piazza, Sabina Rossi – Dipartimento di Informatica, Università Cà Foscari di Venezia

1 Parallelismo, nondeterminismo e sicurezza dei programmi Approfondimento per il corso di Semantica...

Documents

Transcript of 1 Parallelismo, nondeterminismo e sicurezza dei programmi Approfondimento per il corso di Semantica...