A QUANTIFIED MODEL OF SECURITY: A PROGRAMMING LOGIC
A--- The predicate model: definitions
A1-- Generalised predicates
Programs have type G*DIST(L) -> POW(DIST(G*DIST(L))). As usual we
investigate the result sets by calculating the least expected output of a
random variable ("expectation function"). These expectation functions
are the generalised predicates, and examining the result set of a program
we deduce that the generalised predicates should suitably be of type
G*DIST(L) -> Real .
We lift standard ppt predicates A: G*L -> Real by defining the evaluation
ev of such a predicate A over a generalised state (G,D) to be
ev.A.(g,D) := (+ l . D.l * A.g.l) ,
where D is a distribution over the state space L.
Standard ppt predicates though are insufficient to make the distinction
between external and internal semantics. We introduce a new operator, SM
(for "supermin") as follows: for standard predicates A,B define A SM B by
ev.(A SM B).(g,D) := ev.A.(g,D) MIN ev.B.(g,D) .
Notice that this takes the minimum -after- integration over D (that is,
summation as above when the state space is finite), whereas the normal
MIN operator of ppt first minimises statewise over the functions A and B
and -afterwards- applies the integration. The expressions involving SM
are generated (as we shall see) when external nondeterministic choice is
present in the program.
The generalised predicates that seem to be sufficient in this context are
the standard ppt predicates closed under addition, scalar multiplication
and taking SM's. Addition and scalar multiplication are defined as
follows for generalised predicates:
ev.(p*(A SM B) + C).(g,D)
:= p*(ev.A.(g,D) MIN ev.B.(g,D)) + ev.C.(g,D) .
A2-- Testing Programs
We investigate the result set of a program executed from a (generalised)
initial state (g,D). As usual for a (generalised) predicate, post, we
calculate the weighted average with respect to each possible output
distribution and select the minimum value, representing the "worst case"
expected value. Doing that for each possible initial (g,D) generates the
precondition.
In detail the calculations for a single output distribution are made as
follows:
first the postcondition is averaged individually over each row of a
result distribution (see matrix below); then the results for each row are
weighted according to the "external" row distribution; finally those
results are summed.
When the postcondition is -standard- this is equivalent to converting the
distributions of type DIST(G*DIST(L)) to the usual "flattened" form of
type DIST(G*L) and integrating as usual.
For example, consider a "result" function F:DIST(G*DIST(L)) summarised by
the matrix:
(l=0) (l=1)
(g=0) 0.5 0.5 @ 0.25
(g=0) 0.25 0.75 @ 0.25
(g=1) 0.4 0.6 @ 0.5
When used to test against a -standard- ppt postcondition, form the usual
joint distribution over G*L obtained by combining the conditional
distributions. Note (below) how the rows (g=0) are amalgamated --- thus
testing against standard postconditions ignores the difference between
internal and external probabilistic choice. The "flattened" joint
distribution becomes:
(l=0) (l=1)
(g=0) 0.19 0.32
(g=1) 0.2 0.3
A postcondition involving SMs requires a different kind of calculation:
it represents a set of standard postconditions, each of which must be
integrated against the full output distributions and the minimum value
taken.
Define for example
A := [g=0 AND l=1] + [g=1 AND l=0]
B := [g=0 AND l=0] + [g=1 AND l=1]
Then A SM B represents the set of standard postconditions
{ [g=0 AND l=1] + [g=1 AND l=0],
[g=0 AND l=0] + [g=1 AND l=1],
[g=0 AND l=1] + [g=1 AND l=1],
[g=0 AND l=0] + [g=1 AND l=0] } .
The new functions C belonging to the resulting set are those that satisfy
C[g:=g'] equals A[g:=g'] or B[g:=g'] ,
for each value g' of the global variable.
For the matrix above we must calculate the minimum expected output along
each row of the matrix separately for each standard postcondition in the
set. For example for the first row the expected return for each of the
four standard postconditions is the same (value 0.5). For the second and
third rows the minimum occurs at
[g=0 AND l=0] + [g=1 AND l=1] for row 2 (value 0.25)
[g=0 AND l=0] + [g=1 AND l=0] for row 1 (value 0.4).
Thus the total -least- expectation is the weighted sum:
0.5*0.25 + 0.25*0.25 + 0.4*0.5 .
SMs arise because of external nondeterministic choice which cannot take
advantage of the -actual- value of the internal variables, but only its
current distribution. Each possible resolution of an external
nondeterministic choice generates a precondition to be handed on to the
rest of the program, thus each possible precondition must be retained
until the distribution over the internal variables is revealed.
For example the external assignment
g:=0 [] g:=1
applied to the postcondition [g=l] generates two preconditions [0=l] and
[1=l] --- one for each possible resolution of the choice. Given an
initial assigment
l:=0 {1/4} l:=1
(since the external demon has no -absolute- knowledge of l but only of
its distribution) both predicates must be averaged over l's distribution
separately producing
1/4 , 3/4 respectively.
The external demon, only knowing the initial l-distribution, would seek to
minimise the expectation and therefore choose the left branch.
[ Aside --- an internal demon would have complete knowledge of l and be
able to avoid l every time. On application of
wp.(g:=0 {} g:=1)
to the postcondition [g=l] the preconditions [0=l] and [1=l] are combined
with MIN and the expression reduces to zero immediately. ]
A3-- Predicate transformer semantics
We need three operators: wp, iwp, ewp which repectively denote weakest
precondition, internal weakest precondition and external weakest
precondition dealt with separately below. For a complete program, prog,
we will always be interested in calculating ewp.prog.post for some
postcondition post. We will need (see below) to alternate between iwp and
ewp in the case of calculating preconditions for module calls. We denote
an explicit call to an internal operation by CALL, and when this occurs
within a program fragment then internal semantics is used.
Thus ewp.(CALL prog) := iwp.prog.
The five basic rules for reducing expressions are as follows:
(1) Standard wp applies for standard postconditions and deterministic
programs.
(2) For a deterministic program prog,
iwp.prog.(SM x. post)
:= (+g':G . (SM x. wp.prog.(post AND [g=g'])) .
(3) Internal nondeterministic choice is converted to an an external
nondeterministic choice:
ewp.(CALL ({}x. prog(x)))
:= ewp.([]f:L->X. CALL prog(f.l)) .
(4) External probabilistic choice:
ewp.(prog [p] prog').post
:= p*(ewp.prog.post) + ~p*(ewp.prog'.post) .
(5) External nondeterministic choice:
ewp.([]x. prog).post := (SM x. ewp.prog.post) .
B--- The predicate model: Simplifying calculations
The following results are all designed to reduce the complexity of the
expressions. Expressions become complicated when external nondeterminism
and internal probabilistic choice interact, as for example expressions
involving SM are generated by an external nondeterministic choice, and
they can only be reduced later when the internal distribution is
declared.
Knowing when it is possible to remove the SMs from an expression is a
useful technique. The following lemmas describe some rules for
simplification.
Lemma 1 If for all values g',
=====
wp.prog.(post MIN [g=g']) = (wp.prog.post) MIN [g=g']
for any standard postcondition and some deterministic prog then
for that prog
iwp.prog.(SM x.post) = (SM x. wp.prog.post) .
This says that if prog does not assign to g (but may read from it) then
Rule 2 may be simplified by not referring to g explicitly. Intuitively
one reasons that since only the local variables are changed, and there is
no nondeterminism the global variables cannot pass any information
outside the module.
Proof
iwp.prog.(SM x.post)
= "Rule 2"
(+g'. (SM x. wp.prog.(post MIN [g=g'])))
= "hypothesis"
(+g'. (SM x. (wp.prog.post) MIN [g=g']))
= "(A MIN [g=g']) SM (B MIN [g=g']) = (A SM B) MIN [g=g']"
(+g'. (SM x. wp.prog.post) MIN [g=g'])
= (SM x. wp.prog.post) .
@@@
Lemma 2 If there is some function f, depending only on the deterministic
===== program prog (and not on the incoming l-distribution), such that
for all post, g'
wp.prog.(post MIN [g=g']) = [g'=f.g] MIN wp.prog.post
then
iwp.prog.(SM x.post) = (SM x. wp.prog.post) .
This says that if the program can assign to g, but only to a single value
then Rule 2 simplifies --- since the output value of g is always the same
that information cannot be used to deduce more information about the
local variables.
Proof
iwp.prog.(SM x. post)
= "Rule 2"
(+g'. (SM x. wp.prog.(post MIN [g=g'])))
= "hypothesis"
(+g'. (SM x. [g'= f.g] MIN wp.prog.post))
= (+g'.(SM x. wp.prog.post) MIN [g'=f.g])
= "f a function, independent of l, obvious?"
(SM x. wp.prog.post) .
@@@
Note that Lemma 1 is a special case of Lemma 2, when f is the
identity.
In fact Rule 2 simplifies even for nondeterministic programs.
Lemma 3 If either of the conditions of Lemmas 1,2 hold then
=====
iwp.({}y. prog) .(SM x.post) = (SM x. wp.([]y.prog)).
Proof
We present only the calculation for a binary choice. So let prog, prog'
be deterministic programs so that for -any- boolean function, f:L -> B
prog prog'
satisfies the conditions for Lemma 2. We now reason as follows:
iwp.(prog {} prog').(SM x. post)
= "Rule 3, Rule 5"
(SM f:L->B .iwp.(prog prog').(SM x. post))
= "hypothesis, Lemma 2"
(SM f:L->B. (SM x. iwp.(prog prog').post))
= "swap SM"
(SM x. (SM f:L->B .iwp.(prog prog').post))
= "nondet lemma, see below"
(SM x. wp.prog.post MIN wp.prog'.post)
= (SM x. wp.(prog {} prog').post) .
The nondet lemma is stated as follows: for any type T and predicate pre
--- without SM --- referring to f only in the form f.l, we have
(SM f:L->T . pre(f.l)) = (MIN t:T. pre(t)) .
@@@
Any deterministic probabilistic assignment that only changes global
variables can be made externally or internally --- the intuition here is
that probabilistic choice is not influenced by demons, be they internal
or external, and if the local variables remain unchanged no extra
information is passed to the outside. The next lemma is the simplest
instance of this, though the result is more generally true.
Lemma 4 For global variable, g we have
=====
g:=0 {p} g:=1 = g:=0 [p] g:=1
Proof
iwp.(g:=0 {p} g:=1).(SM x. post)
= "Rule 2"
(SM x. wp.(g:=0 {p} g:=1).(post MIN [g=0]))
+ (SM x. wp.(g:=0 {p} g:=1).(post MIN [g=1]))
= "standard ppt"
(SM x. p*post[g:=0]) + (SM x. ~p*post[g:=1])
= p*(SM x. post[g:=0]) + ~p*(SM x. post[g:=1])
= "Rule 4"
ewp.(g:=0 [p] g:=1). (SM x. post) .
@@@
Knowing when standard (ppt) reasoning can be used will be a useful
technique. Clearly if one knows in advance that no expression containing
SM will be generated then standard reasoning can be used throughout. Two
obvious situations are
(A) when all the operations are internal,
(B) when there is no external nondeterministic choice.
But the problem really occurs when internal probabilistic choice and
external nondeterministic choice are present; thus if the internal
variables are never assigned to probabilistically then, once again,
standard reasoning alone should apply. For deterministic programs the
result is again intutitively clear: if the internal state is always a
point distribution then the external demon knows all there is to know.
The condition in Lemma 5 captures the property that the behaviour of the
internal variables is nonprobabilistic.
Lemma 5 For deterministic prog, if wp.prog.[l=l'] is 0 or 1 then
=====
iwp.prog.(SM x. post) = wp.prog.(MIN x. post) .
Proof
iwp.prog.(SM x. post)
= "Rule 2"
(+g'. (SM x. wp.prog.(post MIN [g=g'])))
= "prog is deterministic"
(+g'. (SM x. (+l'. wp.prog.(post MIN [g=g'] MIN [l=l']))))
= "see below"
(+g'.(+l'.(SM x. wp.prog.(post MIN [g=g'] MIN [l=l']))))
= "swap +"
(+l'.(+g'.(SM x. wp.prog.(post MIN [g=g'] MIN [l=l']))))
= "Rule 2"
(+l'. iwp.prog.(SM x. (post MIN [l=l'])
= "post MIN [l=l'] nonzero for single value of l"
(+l'. iwp.prog.(MIN x. (post MIN [l=l'])
= "prog deterministic, Rule 1"
wp.prog.(MIN x. post) .
For the "see below" step we reason as follows:
(SM x. (+l'. wp.prog.(post MIN [g=g'] MIN [l=l'])))
= "[l=l'] nonprobabilistic"
(SM x. (+l'. wp.prog.(post MIN [g=g'] & [l=l'])))
= "prog deterministic, wp.prog is linear and terminating"
(SM x. (+l'. wp.prog.(post MIN [g=g']) & wp.prog.[l=l']))
= "hypothesis"
(SM x. (+l'. wp.prog.(post MIN [g=g']) MIN wp.prog.[l=l']))
= "prog deterministic, hypothesis"
(+l'.(SM x. wp.prog.(post MIN [g=g'])) MIN wp.prog.[l=l']) .
@@@
Lemma 5 also holds for nondeterministic programs.
Lemma 6 If prog, prog' satisfy the hypotheses for Lemma 5 then
=====
iwp.(prog {} prog').(SM x. post)
= iwp.(prog {} prog').(MIN x. post) .
Proof
Apply Rule 3 to convert the program into an external choice over
deterministic programs progprog', where f is a boolean valued
function. Now note that wp.(prog prog').[l=l'] is either 0 or 1 if
wp.prog.[l=l'] and wp.prog'.[l=l']. The result now follows from Lemma 5.
@@@
C--- The predicate model: examples
We rework the examples set out in the relational model, this time using
the logic.
C1-- -Internal- prob is -not- detectable by external nondet.
For the program
CALL l:= (0 {p} 1); g:= (0 [] 1)
we calculate for the postcondition [l<>g]
[l<>g]
= "apply ewp.(g:= (0 [] 1)), Rule 5"
ewp.(g:= 0).[l<>g] SM ewp.(g:= 1).[l<>g]
= "standard ppt, global assignments"
[l<>0] SM [l<>1]
= "apply ewp.(CALL l:=0 {p} l:=1), following Lemma 1"
wp.(l:= (0 {p} 1)).[l<>0]
SM wp.(l:= (0 {p} 1)).[l<>1]
= "apply wp.(l:= (0 {p} 1)) twice"
~p SM p
= "SM reduces to MIN if l not mentioned"
~p MIN p .
The interpretation is that g can guess l with probability at least
p MAX ~p.
C2-- -External- prob -is- detectable by external nondet
For the program
CALL l:= 0 [p] CALL l:= 1;
g:= (0 [] 1) ,
again we test with the postcondition [l<>g]:
[l<>g]
= "apply ewp.(g:= (0 [] 1))
[l<>0] SM [l<>1]
= "apply ewp.(CALL l:= 0 [p] CALL l:= 1), Rule 4"
p*(ewp.(CALL l:= 0).([l<>0] SM [l<>1])
+ ~p*(ewp.(CALL l:= 1).([l<>0] SM [l<>1])
= "lemma 1 twice"
p*([0<>0] SM [0<>1]) + ~p*([1<>0] SM [1<>1])
= "arithmetic"
p*0 + ~p*0
= 0 .
Thus the probability is 0 in this case: the interpretation is that g can
guess l with probability at least 1.
C3-- Mixture of internal and external prob
Consider the program
CALL l:= (0{p}1) [q] CALL l:= (0{r}1);
g:= (0[]1) .
As usual we calculate
[g<>l]
= "apply ewp.(g:= (0[]1))"
[0<>l] SM [1<>l]
= "apply ewp.(CALL l:= (0{p}1) [q] CALL l:= (0{r}1)), Rule 4"
q*(iwp.(l:= (0{p}1)).([0<>l] SM [1<>l]))
+ ~q*(iwp.(l:= (0{r}1)).([0<>l] SM [1<>l]))
= "Lemma 1 twice"
(~p MIN p) [q] (~r MIN r) .
C4-- Internal versus external nondet: sometimes equal.
We show that the two programs
l:= (0 {} 1) and CALL l:= 0 [] CALL l:= 1
give the same result on all postconditions. Thus consider a general
postcondition over l and g, and let B be the Boolean type. We have
iwp.(l:= (0 {} 1).(SM x. post)
= "Rule 3"
ewp.([]f: L->B . CALL l:=0 < f.l > l:=1).(SM x. post)
= "Rule 5"
(SM f: L->B . iwp.(l:=0 < f.l > l:=1).(SM x. post))
= "Lemma 1"
(SM f: L->B . (SM x. post[l:=0] < f.l > post[l:=1]))
= "Swap SM's; nondet lemma"
(SM x. (MIN b:B. post[l:= 0] ** post[l:= 1]))
= (SM x. post[l:= 0] MIN post[l:= 1])
= "post[l:= ?] contains no l"
= (SM x. post[l:= 0] SM post[l:= 1])
= (SM x. post[l:= 0]) SM (SM x. post[l:= 1])
= "Rule 5; Lemma 1"
ewp.(CALL l:= 0 [] CALL l:= 1).(SM x. post) .
[ Aside --- this calculation shows that the logic cannot distinguish
between the two programs, and thus provides one reason for including the
internal convex closure described in the relational section. ]
C5-- Internal versus external nondet: sometimes not equal.
We repeat C4 but this time we allow predicates to be expressions over g,l
and a new local variable, m. This time internal choice can be
distinguished from external. Let post be [l<>m], and calculate:
iwp.(l:= (0 {} 1)).[l<>m]
= (SM f: L*M->B . [l<>m][l:=0] [l<>m][l:=1])
= (SM f: L*M->B . [0<>m] [1<>m])
<= "assume M={0,1}; take f.l.m := (m=0)"
= 0 .
For external choice however we have
ewp.(l:= (0 [] 1)).[l<>m]
= ewp.(CALL l:=0).[l<>m] SM ewp.(CALL l:=1).[l<>m]
= [m<>0] SM [m<>1]
= "again assume M={0,1}"
[m=1] SM [m=0] ,
and evaluating that expression at an initial m-valued distribution
m:=0 {1/2} m:=1
gives for example 1/2, not 0.
C6-- Case analysis over global variables is essential
This example illustrates why we need to introduce an explicit global
variable in Rule 2, even when the postcondition does not refer explicitly
to the global variables.
Consider the program
CALL (l:=0 {0.5} l:=1); CALL g:=l; h:= (0[]1)
where (as usual) l is a local variable and g and h are global. Here we
have a variable h which tries to guess the local variable l. That should
be possible every time: the preceeding statement assigns to g exactly the
value of l, which can then be seen externally. As before we calculate for
the postcondition [h<>l]
[h<>l]
= "apply ewp.(h:= (0[]1))"
[0<>l] SM [1<>l]
= "apply ewp.(CALL g:=l)"
...
In the standard ppt logic, since the post condition contains no explicit
reference to g, and the statement g:=l would leave all variables but g
unchanged, application of wp.(g:=l) has no effect on the postconditon.
With that incorrect use of Rule 2, we would then continue the reasoning
... [0<>l] SM [1<>l]
= "apply ewp.(CALL (l:=0 {0.5} l:=1))"
0.5 ,
which says that the variable h can guess l (and avoid it) only half the
time. This is obviously not the intended meaning since g (a global
variable) copies l exactly, making that information available to an
external demon.
The calculation has failed to introduce the dependence of l's
distribution on the value of g. Continuing now with the correct
application of Rule 2 instead, we have
... (+h',g' . wp.(g:= l).[0<>l AND g=g' AND h=h']
SM wp.(g:= l).[1<>l AND g=g' AND h=h'])
= "apply wp.(g:= l); one-point rule for h'"
(+g' . [0<>l AND l=g'] SM [1<>l AND l=g'])
= "nonzero values occur only for 0<>g' AND 1<>g'"
[0<>l AND 1<>l]
= "apply ewp.(CALL (l:=0 {0.5} l:=1))"
= 0 .
C7-- The `spy' example.
Consider the structure
VAR g: G;
h: L;
MODULE Secure
VAR l: L;
PROC Secrets == l:@ D --- Set l according to distribution D
PROC Spy == g:< G --- Choose g internally nondet from G
END Secure;
Secret;
Spy;
h:< L --- Choose h externally nondet from L, trying to guess l
Module Secure contains a secret l that is set probabilistically by
operation Secrets, representing the overall effect of `secret' activity
inside the module. Variable l is not externally observable.
Operation Spy uses external variable g to pass out information about l;
it does so by making an internal nondeterministic choice from an
arbitrary set G. (Clearly the size of the otherwise arbitrary set G is
related to the amount of information the spy can disclose.)
The externally nondeterministic h:< L --- the enemy --- tries to guess
the value of l, using (implicitly) the information in g passed out by the
spy.
Success for the spy and the enemy depends on their coming to an
arrangement beforehand on the use of their respective nondeterministic
choices. To discover the (maximum) probability of a successful guess we
use postcondition [h<>l] --- we want the spy/enemy to -fail- to guess l,
and so set that as a postcondition --- and calculate as follows:
[h<>l]
= "apply ewp.(h:< L)"
(SM l':L . [l'<>l])
= "apply iwp.(g:< G)"
(SM f:L->G.
(+g':G.
(SM l':L.
wp.(g:= f.l).[l'<>l AND g'=g])))
= "wp of assignment" (1)
(SM f:L->G.
(+g':G.
(SM l':L . [l'<>l AND g'=f.l])))
= "distribute inner SM through +"
(SM f:L->G.
(SM n:G->L.
(+g':G . [n.g'<>l AND g'=f.l])))
= "commute SM's"
(SM n:G->L.
(SM f:L->G.
(+g':G . [n.g'<>l AND g'=f.l])))
= "nondet lemma: see below"
(SM n:G->L.
(MIN g'':G.
(+g':G . [n.g'<>l AND g'=g''])))
= "one-point rule"
(SM n:G->L.
(MIN g'':G . [n.g''<>l]))
= "collapse MIN"
(SM n:G->L . [l NOTIN n.G])
= "introduce L' to replace n.G"
(SM L': POW(L) | #L'<=#G . [l NOTIN L'])
= "assume #G<=#L; exploit taking of minima"
(SM L': POW(L) | #L'=#G . [l NOTIN L']) . (2)
The deferred "nondet lemma" is that for any type T and predicate pre ---
without SM --- referring to f only in the form f.l, we have
(SM f:L->T . pre(f.l)) = (MIN t:T. pre(t)) .
That lemma seems to be an important way of simplifying SM expressions to
those involving just MIN instead.
To conclude, we go one step further from (2), using the lemma
iwp.(l:@ D) = ev.D ,
so that the overall precondition becomes
iwp.(l:@ D).(2)
= "above"
ev.D.(2)
= ev.D.(SM L': POW(L) | #L'=#G . [l NOTIN L']) ,
thus simply the evaluation of (2) over the distribution D. With a bit of
thought (?) that leads us to conclude that the probability of
establishing [h<>l] --- the least guaranteed probability of the spy's
-failing- to guess the secret --- is the sum of all but the #G greatest
probabilities in the (known) distribution D over the (unknown) internal
l.
Thus the probability of the spy's -succeeding- to guess the secret is the
complement of that: the sum of the #G greatest probabilities in D. If D
is uniform --- with each probability 1/#L --- that reduces to just
(#G/#L) MIN 1 ,
where the MIN 1 simply handles the situation in which #G>#L.
As special cases, note that when #G=1 the spy can pass out no
information, and so the probability of a correct guess is 1/#L --- no
better than an oblivious guess; when #G=#L the spy can pass out the exact
value of l, and the probability is then 1.
(What happens when #G=0? Then the statement g:< G is miraculous, and
cannot execute --- and neither can its successor h:< L, giving that the
probability is then 0 because the guess can't even be made.)
[ Aside --- If we return to (1) and strip off the outer quantification
over f, we get
(+g':G . (SM l':L . [l'<>l AND g'=f.l])) ,
in which f is now free. That as a precondition gives the probability of
the enemy's failing to guess l when the spy's policy is given
-explicitly- as a function f (and with our growing familiarity with these
idioms that precondition can almost be written down directly). The
operation becomes
PROC Spy == g:< f.l --- Communicate -something- about l .
Compare the even/odd example C8 below, in which f is given explicitly as
(DIV 2).
Returning now to our current example, we see that the minimisation over f
in (1) is effectively a minimising over all possible `revelation'
functions that the two demons might have agreed beforehand. ]
C8-- The `even/odd' example
Consider the structure
VAR g: [0,N); --- integers from 0 inc. to N exc.
h: [0,2N);
MODULE Secure
VAR l: [0,2N);
PROC Traitor == --- Details below
PROC Spy == g:= l DIV 2 --- Choose g internally nondet from G
END Secure;
Traitor;
Spy;
h:< [0,2n) --- Choose h externally nondet, trying to guess l
Note that it contains no probabilistic statements (and that hence this is
in part a `pure' security example).
Module Secure contains a secret l that is almost entirely exposed by Spy
--- only one bit remains hidden. On the basis of the exposure (into g),
the external h then tries to guess the value of l. For the moment the
behaviour of Traitor is unspecified.
To evaluate h's chance of successful guessing, we calculate as usual from
the postcondition that the guess is -wrong- :
[h<>l]
= "apply ewp.(h:< L)"
(SM l':[0,2N) . [l'<>l])
= "apply iwp.(g:= l DIV 2)"
(+g':[0,N).
(SM l':[0,2N).
wp.(g:= l DIV 2).[l'<>l AND g=g']))
= "wp of assignment"
(+g':[0,N).
(SM l':[0,2N).
[l'<>l AND (l DIV 2)=g']))
= "specialise to just the two effective l' values"
(+g':[0,N).
[2g'<>l AND (l DIV 2)=g'] SM [2g'+1<>l AND (l DIV 2)=g'])
= (+g':[0,N) . [l=2g'+1] SM [l=2g']) , (1)
from which we can see that if the incoming distribution is L, say, a
function from the integers [0,2N) into the probabilities [0,1], then the
probability of establishing [h<>l] is
L.0 MIN L.1
+ L.2 MIN L.3
+...+ L.(2N-2) MIN L.(2N-1) .
Clearly, therefore, if the incoming distribution is uniform (L.k = 1/2N)
then the probability is 1/2 --- just the probability of choosing the
missing low-order bit at random.
Suppose now that a Traitor is inserted into the module who can ensure
that l is even --- we specify that by writing
ewp.Traitor.[odd l] = 0 ,
which does not however require any particular -distribution- of the l
values among the even integers in [0,2n).
[ Aside --- To use the more straightforward specification
ewp.Traitor.[even l] = 1
would in fact be saying too much: it says that the traitor -must- make l
even "every time". The specification we gave says instead that the
traitor -can- ensure that l is even "if/when he wants to", and is weaker.
Pursuing the metaphor, that freedom allows the traitor to permit odd
values of l on occasion, when perhaps he is under suspicion. ]
To analyse the new situation we carry on from (1) above, noting
(1) <= "drop a SM term"
(+g':[0,N) . [l=2g'+1])
= [odd l] ,
so that we can reason overall (2)
ewp.(Traitor; Spy; h:< [0,2N)).[h<>l]
= "sequential composition"
ewp.Traitor.(ewp.(Spy; h:< [0,2N)).[h<>l])
<= "above, and monotonicity of ewp.Traitor"
ewp.Traitor.[odd l]
= "specification of Traitor"
0 ,
so that in fact
ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] = 0 .
The conclusion is that if the traitor -can- ensure that the secret l is
even, then we must assume (with probability 1-0 = 1) that the secret can
be completely compromised.
Note that the looseness of the traitor's specification is important ---
given his situation there may be many other constraints he must satisfy
at the same time.
Finally, consider a traitor who can ensure only that l has probability
2/3 of being even --- he can `bias' its parity, but not completely
control it. Again we specify that `backwards' by
ewp.Traitor.[odd l] <= 1 - 2/3 = 1/3 ,
and the reasoning at (2) would become (only the last step changes)
ewp.(Traitor; Spy; h:< [0,2N)).[h<>l]
= "sequential composition"
ewp.Traitor.(ewp.(Spy; h:< [0,2N)).[h<>l])
<= "above, and monotonicity of ewp.Traitor"
ewp.Traitor.[odd l]
<= "specification of Traitor"
1/3 ,
so that overall
ewp.(Traitor; Spy; h:< [0,2N)).[h<>l] <= 1/3 .
We conclude that the likelihood of the secret's being kept is no more
than 1/3 --- it has thus probability (at least) 2/3 of being revealed.
The analysis would be the same for any bias --- not just 2/3 --- and
would apply whether that bias were towards even or towards odd.
[ Aside --- Concluding on the basis of the example that the secret is
revealed with probability "the maximum of the even/odd biases" is
tempting, but incorrect: since g's value is known at the point the guess
is made (at the point h is chosen), there is more information available
than simply the overall bias. It might be for that particular g value
that the bias is particularly high, for example. Nevertheless we can
return to (1) and reason
(+g':[0,N) . [l=2g'+1] SM [l=2g']) (1)
<= "super-distribute SM through +"
(+g':[0,N) . [l=2g'+1])
SM (+g':[0,N) . [l=2g'])
= [odd l] SM [even l] ,
which is the -minimum- of the two biases --- thus the probability of h's
guessing incorrectly is -no more- than the lesser bias. The probability
of h's guessing correctly is thus shown to be -no less- than the greater
of the two biases.
But (as we saw above), unless the bias is uniform the probability of l's
being guessed is probably greater still, since h can use g's actual value
to inform its guess on each occasion. ]
**