Transcript Posta elettronica

Non-interference Properties for
Probabilistic Processes
A Process Algebraic Approach
Alessandro Aldini
joint work with
Mario Bravetti and Roberto Gorrieri
1
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
2
Formal methods and security
 Motivation:
–
–
The Internet provides support for the transmission of
data over communication networks, but is not
designed with the goal of avoiding unauthorized
disclosure of such data.
Cryptography is the solution, but…
•
•
•
•
imported code
mobile agents
malicious non-authenticated accesses
…
raise a supplementary, increasing demand for security
in computer networks.
3
Formal methods and security
 Formal techniques may help to:
– prevent security holes,
– provide a generalized, easily verifiable notion
of security.
Here, we concentrate on the security analysis of
information flow
in systems and, more precisely, how to characterize
the absence of any insecure flow, by applying the
classical idea of non-interference.
4
Non-interference
Non-interference checks the absence of
information flows
through the system, in terms of confidential,
high level
information illegally revealed to someone
without the related access right.
5
Non-interference
 The users of the system are partitioned into
high level users and low level users.
 High and low users interact with the system
through separate interfaces.
 Low user cannot directly observe what high
users do.
 Low users know the exact, complete design of
the system, including the high interface.
 users interact with the system through input
actions (guided by the users) and output actions
(guided by the system).
6
Non-interference
LOW
USERS
Low
interface
High
interface
HIGH
USERS
?
information flow
The interactions of low users with the
system should not be affected by the
behavior of high users
[Gougen & Meseguer ’82]
7
Direct information flow
Low
user
System
High
user
var X = 01
read x
write x := 1
A high value is directly communicated from the
high user to the low user!
8
Indirect information flow
Non-interference seeks to capture also
covert channels
(indirect information flows from high level to low level)
EXAMPLE
Sharing of resources (e.g. memory devices).
High user
create
private file
data.txt
shared memory
data.txt
Low user
create
public file
data.txt
FAIL!
9
Non-interference: an example
High level activity
a, b, c: low level activities
h
a
P
c
b
Information flow from
H to L!
10
Non-interference
Information flow analysis in process algebras:
[Jacob’88, Ryan’91, Focardi & Gorrieri’95, Roscoe’95,
Ryan & Schneider’99]
– Information flow is analyzed by
considering the possibilistic behavior of
the system, i.e. what events are possible.
– Further aspects are not considered, such
as the timing of actions and the
probability distribution of events.
11
Non-interference
– In this talk, we take into consideration the
influence of the high level behavior upon
the probability distribution of the
observable, low level events.
– The motivation is twofold:
• probabilistic covert channels may occur
which are not observable in a purely
nondeterministic setting;
• a quantitative estimate of the information
flowing through the system may be given.
12
Probability & non-interference (1)
The frequency of the possible low
outcomes derived from several
execution runs of the system may
change depending on the interaction
of the high user with the system.
[Gray’92, Sabelfeld & Sands’99, Hankin et al.’00]
13
Probability & non-interference (1)
High level activity
a, b: low level activities
h
a 1 1
2 3
P
b 1 2
2 3
Information flow from
H to L!
14
Probability & non-interference (2)
Interactions of high users with the
system which affect the interactions of
low users may occur with a negligible
probability.
In such a case, the illegal information
flow can be tolerated by the users of
the system.
[Hankin et al.’02]
15
Probability & non-interference (2)
High level activity
a, b: low level activities
h
a 1-e
P
be
Information flow from
H to L…
quite negligible!
16
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
17
A non-deterministic process algebra
 Actions are divided into:
– a set I of input actions a* , b* , …
– a set O of output actions a, b, …
Act = I U O U {t}
 Visible action types are partitioned into two
disjoint sets:
– ATypeL of low level types
– ATypeH of high level types
AType = ATypeH U ATypeL U {t}
18
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
where S, L are in P (AType – {t}).
19
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
0
Null term, denoting a terminated
or deadlocked term.
20
Syntax
P:
0
p.P
P+P
p.P
P
S
P
P
L
A
Prefix operator: executes action p
and then behaves as term P
(p is an output action, an input action,
or an internal action t).
21
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
P+Q
Alternative choice operator:
expresses a non-deterministic choice
between a term P and a term Q
(CCS-style)
22
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
P Q
S
Parallel composition operator:
expresses the concurrent execution of
processes P and Q
(CSP-style)
23
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
PL
Hiding operator:
turns the visible action with type in L
into internal t actions
24
Syntax
P:
0
p.P
P+P
P
S
P
P
L
A
A
Constants are used to define recursive terms
A = P
25
Q : synchronization policy
P
S
a* .P
a is in S:
S
a .P
S
a .P
a* .Q
a* .Q
a*
P
Q
S
a
P
Q
S
a .Q
S
26
Q : synchronization policy
P
S
a is in S:
((a* .P
S
a* .P’)
a
S
S
a .Q
S
Q broadcasts the output action a, while
all the other processes synchronize on
the input action a* (asymmetric
multiway synchronization)
P’)
(( P
a* .P’’)
P’’)
S
Q
S
27
Restriction
The synchronization rule can also express the
restriction of actions.
EXAMPLE
In a*
.P
c .Q (with a = c and a in S)
S
the action a*, constrained to synchronize, cannot be
executed!
We use
P L
to stand for
P
0
L
which cannot execute the actions of P with type in L.
28
Equivalence
 We use equivalence checking to express security
properties: a system S is secure if two subsystems,
suitably derived from S and from the security
definition, are equivalent.
 We need a notion of equivalence to relate terms
which behave the same from the viewpoint of an
external observer.
 Since t actions cannot be seen by any external
observer, and since the definition of security
properties focuses on observable behaviors, we
use a notion of equivalence which abstracts from
internal actions: weak bisimulation equivalence.
29
Equivalence
Note:
G
denotes the set of processes of the calculus
p
p
t
means that a p labeled transitions occurs
means that a p labeled transition (with p visible
action) occurs possibly preceded and followed by a
sequence of internal t transitions
means that zero or more t labeled transitions occur
30
Weak bisimulation:
B
A relation R in G x G is a weak bisimulation iff (P,Q) in R
implies for all p in Act:
• whenever P
Q
p
p
P’, then there exists Q’ such that
Q’ and (P’,Q’) in R
• whenever Q p Q’, then there exists P’ such that
P
p
P’ and (P’,Q’) in R
[Milner’89]
31
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
32
Nondeterministic security properties
 We rephrase in the context of our nondeterministic
calculus some of the security properties defined in
[Focardi & Gorrieri’95].
33
a. 0 + h.b. 0
Low user standpoint:
High user does
not interact
a
High user
interacts
a
t
b
34
Nondeterministic Non-interference
(int)
Intuition: a system P is secure iff the behavior of
P observable by a low user does not depend
on the high interactions.
Formally:
P
ATypeH
B
P
ATypeH
For each low behavior observable when the high
user does not interact with the system, we have an
equivalent low behavior observable when the high
user executes high actions, and viceversa.
35
Examples
Low user viewpoint
without high
interactions
a. 0 + h.b. 0
a. 0
a. 0
a. 0
+ h. 0
with high
interactions
B
B
a. 0 + t.b. 0
a. 0
+ t. 0
36
Examples
Low user viewpoint
without high
interactions
a. 0 + h.a. 0
P = a.Q
Q = h.Q + b. 0
a. 0
with high
interactions
a. 0 + t.a. 0
B
a
b
B
t
a
b
37
a.0 + h.h.a. 0
Low user standpoint:
High user does
not interact
?
High user
interacts
t
a
a
Nondeterministic non-interference
is not enough!
t
a
38
Nondeducibility on Composition
(comp)
Intuition: a system P is secure iff the behavior of
P observable by a low user is invariant with
respect to the interaction of any high user.
Formally:
P
ATypeH
B
(( P P ) S )
S
ATypeH
for any:
high process P and
high communication interface S
39
Example
without high
interactions
interacting with
h* . 0
a. 0 + h.h.a. 0
a. 0
B
h* .0
(a. 0 + h.h.a.0 )
h
a
B
a
t
40
t.a.0 + h.a. 0 + b. 0
Low user standpoint:
High user does
not interact
High user
interacts
t
b
a
…but the event b
informs the low user
that the high user did
not interact
Nondeducibility on Composition
is not enough!
41
Strong Nondeducibility on Composition
(scomp)
Intuition: the low user should not distinguish
which, if any, high level event has occurred at
some point in the past.
Formally:
For any P1 derivative of P and for any P2 s.t.
P1
p
P2
p high action
we have
P1
ATypeH
B
P2
ATypeH
42
Example (1)
P
P
h
= t.a.0 + h.a. 0 + b. 0
a. 0
P AType
H
= t.a.0 + b. 0
B
a. 0
P is not scomp-secure
43
Example (2)
h,k: high
a,b: low
t.a.0 + h* .a. 0 + t.b.0 + k* .b. 0
after a high interaction
with action h:
a. 0
B
without high interactions:
t.a.0 + t.b.0
B
after a high interaction
with action k:
b. 0
44
Inclusion relations
int
comp
scomp
45
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
46
A probabilistic process algebra
 algebraic operators are enriched with
probabilistic information:
P:
0
p.P
p
P+ P P
p
P
S
p
P
a
A
S in P (AType - {t}), a in AType - {t}, and p in ]0,1[
 a mixture of the classical generative and
reactive models of probability is adopted.
47
Input actions as reactive actions
1.
2.
The type a of the action to be performed is chosen
by the environment.
The system chooses an action a* according to the
probability distribution associated to the input
actions of type a.
• Transitions are divided into
a* 1
b* 2
b* 1
3
P
3
Q
type bundles
• The choice within a bundle is
purely probabilistic
• The choice among bundles is
nondeterministic (guided by the
environment)
• The sum of the probabilities
within a bundle is to be 1
48
Output (and internal) actions as
generative actions
The system autonomously decides the action to be
performed according to the probability distribution
associated to the enabled output actions.

a 1
6
b 1
2
b 1
3
• Transitions are grouped in a
single bundle
• The sum of the probabilities
within the bundle is to be 1
49
A mixed generative/reactive model
A single generative bundle contains all the output
transitions which can be executed by the system.
 We have several reactive bundles, one for each
action type.

reactive
bundle b
b* 2
3
b* 1
3
1
a 1
6
b 1
2
[Segala’95,
Stark et al.’97]
c*
b 1
3
generative
bundle
50
Probabilistic choice
p
a + b expresses a probabilistic choice between
two output actions: a is chosen with
probability p while b is chosen with
probability 1-p.
p
a* + a* the same!
p
a* + b*
p
a + b*
the choice is nondeterministic:
p is not considered (usually we omit it).
51
Example: mixed choice
p
q
r
( a + b* ) + ( c + b* )
a
c
1-q
q
b* q
b* 1 - q
 parameters p and r are not used because they are attached
to operators which refer to nondeterministic choices
 parameter q guides the probabilistic choice between the
two generative actions a and c and between the two reactive
actions of type b
52
Probabilistic parallel composition
p
P || Q
S
performs the actions of P and Q by following:
1. the synchronization policy described in the
nondeterministic case,
2. the probabilistic mechanism described for the choice
operator, as in ACP [Baeten et al.’95]
Note: the probabilities of the actions which can be
executed by the composed system are normalized
[van Glabbeek et al.’95].
53
Probabilistic parallel composition
p
q
(a + b) ||
c
S
• if a,b,c are not in S, then the system can execute the
output action a with probability pq, the action b with
probability p(1-q), or the action c with probability 1-p.
• if a and b are not in S and c is in S, then the system
can execute output actions of the lefthand process only,
i.e. a with probability q or b with probability 1-q.
• if a and c are not in S and b is in S, then the system
can execute the action a of the lefthand process with
probability p or the action b of the righthand process
with probability 1-p.
54
Probabilistic parallel composition
p
q
(a + b) || 0
L
• All the actions of the lefthand process which belong to the
synchronization set L cannot be executed! Parameter p is
not used.
• The probabilities of the remaining executable actions are
redistributed so that the overall probability of each bundle
is still 1.
• Example: if a is in L, then the system can execute the
action b only with probability 1.
p
We use
P L
to stand for
P
0
L
for any p
55
Probabilistic hiding
Case 1
q
P = a + b (probabilistic choice between
two visible actions)
P
p
a
q
= t + b
(probabilistic choice between
an internal action and a visible
action)
The choice is already probabilistic, therefore
parameter p of the hiding operator is not considered!
56
Probabilistic hiding
Case 2
q
P = a + b (nondeterministic choice
*
P
p
a
p
= t + b
between two visible actions –
parameter q is not considered)
(probabilistic choice between
an internal action and a visible
action)
A nondeterministic choice becomes a probabilistic
choice: parameter p of the hiding operator is needed!
57
Probabilistic hiding
P
p
a
 Parameter p is used to turn nondeterministic choices
between reactive actions of type a and generative actions into
probabilistic choices between internal actions t and generative
actions.
 This corresponds to the execution of a synchronization
between a* and an action a performed by the environment that
gives rise to an internal action t.
 In this way, the hiding operator turns open systems, which
can interact with the environment, into closed systems, which
are fully specified.
58
Equivalence
 We introduce a notion of probabilistic weak
bisimulation.
 The classical weak transition is replaced by the
probability of reaching classes of equivalent states.
Note:
G
denotes the set of processes of the calculus
GAct denotes the set of generative actions
RAct denotes the set of reactive actions
t*a denotes the set of sequences t*a if a is a
generative visible action and the set of
sequences t* if a = t
59
Probabilistic weak bisimulation:
PB
A relation R in G x G is a probabilistic weak bisimulation
iff whenever (P,Q) is in R then for all C in
G /R:
• Prob(P,t*a,C) = Prob(Q,t*a,C) for all a in GAct
• Prob(P,a*,C) = Prob(Q,a*,C) for all a* in RAct
[Baier & Hermanns’97]
60
PB
: an example
t, 1/3
a, 1/2
b, 1/2
a, 1/3
b, 1/3
The two systems are equivalent.
61
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
62
Security analysis and probability
 We extend the definition of the nondeterministic
security properties in our probabilistic setting.
 NOTE: we consider probabilistic processes which
are well defined, i.e. the probability of observing,
at some point in the future, a visible action cannot
tend to zero.
63
Probabilistic Non-interference
(intpr)
Intuition: a system P is secure iff the
probabilistic low view of P is not altered by
the probabilistic behavior of the high users.
Formally (denoted h1…hP the high level action
types which syntactically occur within P):
P
ATypeH
PB
P
p1 … pP
h1
hP
for any sequence of probabilities p1…pP in ]0,1[
64
An Example
.5
.5
P = t.(t.a + h.b) + t.b
hiding
high events
restricting
high events
t
t .5
t .5
.5
b
t .5 .5 t
a
a,b: low
h: high
b
B
PB
t
.5
t
b
a
65
Probabilistic Non-interference
ATypeH
PB
P
p1
… pp
h1
hP
A
In
P
p1…pP in ]0,1[
the universal quantification over all possible probability
distributions of the hidden reactive high actions is needed to
verify the influence of the high activities upon the low view.
EXAMPLE
q
P = h .a + (t.a + b)
*
In the probabilistic setting, the nondeterministic choice
The nondeterministic
can be probabilistically resolved
by the high user which
interacts with the system, thus
altering
probability of
process
P istheint-secure
observing the low event a (b).
q
p
q
(t.a + b)
t.a + (t.a + b) for any choice of p in ]0,1[
PB
66
Probabilistic Non-interference
EXAMPLE
P = h .a + a
*
The low view of P is represented by the execution of
the low action a with probability 1. The high user
which solves the nondeterministic choice in P cannot
alter such a view.
a
PB
p
t.a + a
for any choice of p in ]0,1[
67
Probabilistic Non-interference
EXAMPLE
p
q
P = (a + a.b) + a.h.b
a, pq
a, (1-q)
a, (1-p)q
b, 1
h, 1
b, 1
 The nondeterministic
version of P is int-secure
 If the high user interacts,
then the probability of
observing the sequence a.b
is 1-pq.
 If the high user does not
interact, then the probability
of observing the sequence
a.b is (1-p)q.
 P is not intpr-secure!
68
Probabilistic Non-interference
A pure probabilistic covert channel
[Sabelfeld & Sands’00]
low variable l := high variable h OR random value
High values and random values belong to the same domain:
 In
setting,
the choice
betweenof

In aa nondeterministic
probabilistic setting,
if wesince
observe
the frequency
two different
assignments
is left
the possible
low outcomes
of the
lowunderspecified
level variable,and
thensince
we
the set
of low
outputs
does not change with or without high
may
infer
the high
behavior:
EXAMPLE
interactions, the system is considered to be secure.
l := h +.7 random value
(and we assume h=1)
may give rise, after repeated executions of the system, to the
sequence of outcomes:
0,1,1,1,3,1,2,1,1,1,1,4,0,1,1,1,3,1,1,1
69
Probabilistic Non-interference
Similarly, in our process algebraic setting we may consider
the following system:
p
q
r
P = (a + b) + h.(a + b)
 If the high user interacts, then the probabilistic
choice between the low actions a and b is guided by
parameter q.
 If the high user does not interact, then the
probabilistic choice between the low actions a and b is
guided by parameter p.
 The system is int-secure iff p = q.
 NOTE: the nondeterministic version of process P is
S-secure (with S in {int,comp,scomp}).
70
Probabilistic Non-deducibility on
Composition (comppr)
P
ATypeH
PB
(( P
p
P)
{h1,…,hk}
p1 pk
…
h1 hk
)
ATypeH
for any:
high user P, high communication interface
{h1,…,hk}, probabilities p,p1,…,pk in ]0,1[
71
comppr: example
p
1-p
p
p
P = (t.(a + h) + t.(a + t)) + k.a
h,k: high level types – a: low level type
• P is intpr-secure
• Intuitively, the high user can:
1. block the execution of the action k
2. wait for the internal probabilistic choice
3. accept (block) the execution of the action h
• Formally, by taking the high user P = h . 0 and the
*
synchronization set {h,k}, it turns out that P is not
comppr-secure
72
Strong comppr (scomppr)
As in the nondeterministic case, a stronger
formulation of the comppr property is given in
order to avoid the universal quantification
over all possible high level users.
For any P1 derivative of P and for any P2 s.t.
P1
p, p
P2
p in ATypeH , p in ]0,1]
we have
P1
ATypeH
B
P2
ATypeH
73
Inclusion Relations
intpr
comppr
scomppr
74
Inclusion Relations
Given a nondeterministic security property SP and
its probabilistic counterpart SPpr then we have
SPpr C SP
meaning that if P is SPpr-secure, then the
nondeterministic version of P is SP-secure.
75
Inclusion Relations
int
intpr
comp
.Q
scomp
comppr
.
P
scomppr
76
Outline
 Information flow analysis
 A nondeterministic calculus
 Non-interference for nondeterministic
processes
 A probabilistic calculus
 Non-interference for probabilistic processes
 Non-interference and probabilities
77
Probability & Non-interference
High level activity
a, b: low level activities
h
a 1-e
P
be
Information flow from
H to L…
quite negligible!
78
Probability & Non-interference
 Probabilistic information can be employed to
quantify the probability associated to each
information flow, thus allowing the modeler to
estimate the probability of observing insecure
behaviors.
 Relaxed notions of security properties may allow
to consider as secure systems those systems where
the probability of observing an information flow is
negligible.
 Weak bisimulation is too sensitive and does not
allow to relate probabilistic processes which behave
almost the same.
79
Bisimulation with e-precision (
We pass to a relaxed definition of bisimulation
which is able to tolerate small e-fluctuations.
PBe
)
A relation R in G x G is a probabilistic weak bisimulation
with e-precision iff whenever (P,Q) is in R then for all C in
G /R:
• |Prob(P,t*a,C) - Prob(Q,t*a,C)| < e
for all a in GAct
• |Prob(P,a*,C) - Prob(Q,a*,C)| < e
for all a* in RAct
80
PBe
: example
As we have seen, the system
p
q
P = (a + a.b) + a.h.b
is not intpr-secure.
However, if q is a value close to 0, then the low
level outcome of repeated executions of the
system changes according to negligible
fluctuations with or without the interaction of
the high user.
Formally, P is intpr-secure if we employ as the notion
of equivalence the
PBe
81
PBe
: example (2)
p
q
P = h.a + t.(b + h.b)
h, p
a, 1
insecure
component
t, 1-p
h, q
b, 1
b, 1-q
secure
component
Q
82
PBe
: example (2)
p
q
P = h.a + t.(b + h.b)
 The probability of reaching the secure component Q is 1-p
 The probability of reaching the insecure component is p
Given e > p, we have:
P
ATypeH
PBe
P
r
h
for any r in ]0,1[
In particular:
t, 1
Q
t, e
PBe
a, 1
t, 1-e
for any Q
Q
83
Quantifying information flows
Systems which need an estimation of the illegal
information flows:
 PROBABILISTIC ALGORITHMS.
Among the possible behaviors of the algorithm
we also have an unwanted, insecure behavior
which usually is executed with a probability
close to 0.
EXAMPLES:
 probabilistic non-repudiation
 asynchronous Byzantine agreement
84
Conclusion
1. The process algebraic approach to probabilistic
non-interference is a natural, conservative
extension of the nondeterministic noninterference theory.
2. Probabilistic information can be employed to
quantify information flow.
85
Conclusion
Future work
Analysis of probabilistic cryptographic protocols:
• generalized, easily verifiable notion of
security
Extension of the calculus with message handling
and cryptography:
• relaxation of the assumption of perfect
cryptography
86
References
1.
2.
3.
4.
5.
Aldini, M. Bravetti "An Asynchronous Calculus for Generative-Reactive
Probabilistic Systems" in Proc. of the 8th Int. Workshop on Process
Algebra and Performance Modeling (PAPM’00), Rolim et al. Ed., pp.
591-605, Carleton Scientific, Geneve, 2000
A. Aldini "Probabilistic Information Flow in a Process Algebra " in Proc.
of the 12th Int. Conference on Concurrency Theory (CONCUR'01),
Springer LNCS 2154, pp. 152-168, Aalborg, 2001
A. Aldini "On the Extension of Non-interference with Probabilities" in the
2nd ACM SIGPLAN and IFIP WG 1.7 Workshop on Issues in the Theory
of Security (WITS'02), Portland, Oregon, 2002
A. Aldini, R. Gorrieri "Security Analysis of a Probabilistic Nonrepudiation Protocol" in Proc. of the 2nd Joint Int. Workshop on Process
Algebra and Performance Modelling, Probabilistic Methods in
Verification (PAPM-PROBMIV'02), Springer LNCS 2399, pp. 17-36,
Copenhagen, 2002
A. Aldini, M. Bravetti, R. Gorrieri "A Process Algebraic Approach for the
Analysis of Probabilistic Non-interference" Tech. Rep. UBLCS-2002-02,
University of Bologna (Italy), 2002
87
Thank you!
http://www.cs.unibo.it/~aldini
~bravetti
~gorrieri
{aldini,bravetti,gorrieri}@cs.unibo.it
88