Parallelismo, nondeterminismo e
sicurezza dei programmi
Approfondimento per il corso di Semantica dei
Linguaggi di Programmazione A.A. 2006/07
Prof.ssa Annalisa Bossi
Autore: Elia Gaglio (matricola n° 809477)
21/05/2007
1
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
2
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
3
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…
4
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)
5
I “comandi con guardia” [2]:
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, ’>
6
I “comandi con guardia” [3]:
Regole per i comandi con guardia:
<b, >  true
<b  c, >  <c, >
<b, >  false
<b  c, >  fail
<gc0, >  <c, ’>
<gc0 gc1, >  <c, ’>
<gc1, >  <c, ’>
<gc0 gc1, >  <c, ’>
<gc0, >  fail <gc1, >  fail
<gc0 gc1, >  fail
7
I “comandi con guardia” [4]:
 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
8
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
9
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
10
Linguaggio per processi comunicanti [2]:
 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:
il secondo componente
!n
?n
transizione
non >  spedisce
valore
il primo
componente
<?X;c0,
> 
<c0, [n/X]>
<!e;c1,
<c1, > un(hyp.
<e, >  n)
etichettata perché non che viene ricevuto
riceve un valore
ha effetti sull’ambiente dall’ambiente
dall’ambiente
?n
<(?X;c0)
|| (!e;c1),
>  <c0
(!e;c1),
[n/X]>
La comunicazione
è possibile
se i 2 comandi
sono||posti
in parallelo:
!n
<(?X;c0) || (!e;c1), >  <(?X;c0)
<c0 || c1, [n/X]>
|| c1, [n/X]>
11
Linguaggio per processi comunicanti [3]:
!n, ?n,   
Regole per i comandi (estensioni):
  (transizioni etichettate /
transizioni non etichettate)
?n
<?X, >  [n/X]
<a, >  n
!n
<!a, >  

<gc, >  <c, ’>

<do gc od, >  <c; do gc od, ’>

<c0, >  <c0’, ’>

<c0 || c1, >  <c0’ || c1, ’>

<gc, >  <c, ’>

<if gc fi, >  <c, ’>
<gc, >  fail
<do gc od, >  

<c1, >  <c1’, ’>

<c0 || c1, >  <c0 || c1’, ’>
12
Linguaggio per processi comunicanti [4]:
Regole per i comandi (estensioni):
?n
!n
<c0, >  <c0’, ’> <c1, >  <c1’, >
<c0 || c1, >  <c0’ || c1’, ’>
!n
  ?n e !n

<c, >  <c’, ’>

<c \ , >  <c’ \ , ’>
?n
<c0, >  <c0’, > <c1, >  <c1’, ’>
<c0 || c1, >  <c0’ || c1’, ’>
13
Linguaggio per processi comunicanti [5]:
Regole per i comandi con guardia (estensioni):
<b, >  true
?n
<b  ?X  c, >  <c, [n/X]>
<b, >  true <a, >  n
!n
<b  !a  c, >  <c, >
<b, >  false
<b, >  false
<b  ?X  c, >  fail
<b  !a  c, >  fail
14
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 
15
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 \ {, }
!
?
!
16
Il CCS di Milner [2]:
 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[f]
p  p[f]
!
?
?
!
!
dove si ha:
f() = 
f() = 
f() = 
17
Il CCS di Milner [3]:
 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)
18
Il CCS di Milner [4]:
 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
19
Il CCS di Milner [5]:
Processo nil: no regole (non esegue nessuna azione!)

Prefisso:
  ?n, !n, 
(  p)  p

an
b  true p  p’
!n

(!a  p)  p
Somma:
(b  p)  p’

p0  p0’

p0 + p1  p0’
Restrizione:

p  p’
?n
(?X  p)  p[n/x]

p1  p1’

p0 + p1  p1’
dove se   ?n o   !n allora   L

p \ L  p’ \ L
20
Il CCS di Milner [6]:

Composizione:
!n
?n
p0  p0’
p0  p0’ p1  p1’

p0 || p1  p0’ || p1

p0 || p1  p0’ || p1’
!n

p1  p1’
?n
p0  p0’ p1  p1’

p0 || p1  p0 || p1’

p0 || p1  p0’ || p1’

Ridenominazione:
p  p’
f()
p[f]  p’[f]
Identificatori:

p  p’

X  p’
def

def
dove X := p p[a1/X1,…,ak/Xk]  p’ P(x1,..,Xk)=p

P(a1,…,ak)  p’
21
Il CCS di Milner [7]:
 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))
?n
(?X  (!X  nil))  (!X  nil)[n/X]
che equivale a:
?n
(?X  (!X  nil))  (!n  nil)
!n
(!n  nil)  nil
qui la variabile X è
già legata ad un
particolare numero n
22
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”
23
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
24
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)
locazioni (Loc)
L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
25
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [2]:
 SEMANTICA OPERAZIONALE:
strettamente legata al concetto di stato: L  H  Z

espressa in termini di LTS: <P, >  <P’, ’>
low
<P0, 0>  <Pn, n>
 =l   l = l
dove P’ = {P  end}
e   {high, low}
high
<P0, 0>  <Pn, n>
 Estensioni della Semantica di IMP introdotte:
low
<skip, >  <end, >
2
<b,  >  true <S, >  <end, ’>
 1  2
<await (b) {S}, >  <end, ’>
b  1
26
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [3]:
<b,  >  false

<await (b) {S}, >  <await (b) {S}, >
b

<Pi, >  <Pi’, ’>

<co P1 || … || Pi || … || Pn oc, >  <co P1 || … || Pi’ || … || Pn oc, ’>
low
<co end || … || end || … || end oc, >  <end, >
27
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [4]:
 Introduzione della relazione binaria Reach e Reach* su P:
(P, Q)  Reach   , ’   tali che <P, > → <P’, ’>
P  if (L=1) {P’} else {skip}
P’  if (L≠1) {L:=2} else {skip}
Q  Reach*(P)   n ≥ 0, 0, …, n-1, 0, …, n-1 t.c <P, 0>  <P1, 0>
possiamo definire: Reach(P) = {P, P’, skip}
<P1, 1>  <P2, 1>
…
Reach*(P) = Reach(P)  {L:=2}
<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)
28
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [5]:
 E’ importante valutare se 2 programmi sono indistinguibili per un low-level
observer (nozione di behavioural equivalence)
I 2 L:=1
programmi sono equivalenti
per un low
level observer
P  H:=1;
e si definisca

Questa
proprietà è catturata dalla nozione di low level
Q  H:=2;
L:=H-1
bisimulation
<H:=1; L:=1, >
<H:=2; L:=H-1, >
low
low
<L:=1; [H/1]>
low
<end, [H/1, L/1]>
<L:=H-1; [H/2]>
high
<end, [H/2, L/1]>
29
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [6]:
 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
’> t.c.essere
<Q, >
 <Q’, ’>
P’ e <Q’,
Q’ devono
equivalenti
per ogni
,    t.c.  =l 
 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
30
Flussi di informazione sicuri in programmi concorrenti –
sintassi e semantica [7]:
2 programmil’esempio
sono low visto
level prima
bisimilar
(i valori di
di applicare
L sono equivalenti)
I Riprendiamo
e vediamo
le definizioni
introdotte
nellastrong
slide precedente:
Ma non sono
low level bisimilar (cambiando    [H/5] si
valori differenti per L).
riflette il 
fatto
Potterrebbero
 H:=1; L:=1
e siCiò
definisca
 che:
 H:=5
 co P || R oc  co Q || R oc
QSia
 RH:=2;
L:=H-1
<H:=1; L:=1, >
<H:=2; L:=H-1, >
low
low
<L:=1; [H/1]>
low
<end, [H/1, L/1]>
<L:=H-1; [H/2]>
high
<end, [H/2, L/1]>
31
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, >
32
Flussi di informazione sicuri in programmi concorrenti –
generalized unwinding condition ed istanziazioni [2]:
<P, > soddisfa l’ unwinding framework se:
high
 <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)
33
Flussi di informazione sicuri in programmi concorrenti –
generalized unwinding condition ed istanziazioni [3]:
 if(H=1) {P
else {P
 La nozione di generalizedP unwinding
è 0il}punto
di1}partenza per definire:
. if(L=1) {L:=2} else {L:=3}
 .L:=1;
unwinding class:P0W(=,
=,
. R)
P1  L:=1;class,
skip;inL:=2;
 E’ possibile istanziare la unwinding
modo da trattare diverse classi di
programmi
concordanti
con il* “noninterference principle”. Ad esempio:
Vale la relazione
P  SIMP
l
 SIMPl class: W(=l, l, →)
 SIMPl*
SIMPl*  SIMPl
class: W(=l, l, Reach*)Q  L:=0
Vale la relazione Q  SIMPl*
*
SiLeconsideri
classi SIMP
rispetto l’operatore di
ora:l  SIMPl noncosono
P||Qcomposizionali
oc
 SIMPl*
composizione parallela
=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
34
Flussi di informazione sicuri in programmi concorrenti –
generalized unwinding condition ed istanziazioni [4]:
di composizionalità:
Teorema
La composizionalità
è una proprietà utile ed importante (è possibile lavorare
con
i sottoprogrammi
la proprietà
all’intero programma)
Siano
(ah, bh) h.l.e. eed
(al,“estendere”
bl) l.l.e. e (P
0, P1, S)  SIMP* allora:
..
 SIMP* class: W(=l, l, Reach*)
..
..
dove

è
una
relazione
binaria
t.c.
<P,
>

<Q, > se  =l  e P l Q
1) skip
2) L:=al, H:=ah, H:=al;
3) P0; P1
SIMP*  SIMPl*  SIMPl
4) if (bl) {P0} else {P1}
 SIMP*
5)
Laifclasse
SIMP*
è
più
restrittiva
delle
classi
precedentemente
introdotte.
(bh) {P0} else
.. {P1} se P0 l P1
Infatti vale che: l  l
6) while (bl) {P0}
awaitSIMP*
(bl) {S}
7)
Inoltre
gode di importanti proprietà composizionali utili per lo sviluppo
di8)tecniche
di verifica
co P0 || automatiche
P1 oc
35
Flussi di informazione sicuri in programmi concorrenti –
Delimited Information Release
 La noninterferenza è una proprietà
troppo
forte per le applicazioni pratiche
P  L:=H1;
H1:=H2
 Necessità di prevedere rilasci, declassificazioni di informazioni segrete
D={H1}
PEsempio:
{H1H1:=H2
> 5, H1
+ H2}un highD=
{Aexp,
Bexp}
 SIMPD*D=
infatti
assegna
value
ad una
variabile degradata
 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*)
36
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…
37
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
38
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
39