A QUANTIFIED MODEL OF SECURITY: A RELATIONAL MODEL

A--- The relational model: definitions

A1-- The partitioned state space

Partition the program variables into the global variables g (declared
outside the module, and everywhere accessible) and the local variables l
(declared inside the module, and accessible only to module operations).

Module operations (-internal- operations) do not see the distinction
(since they can access all variables), and regard the state space as the
simple composite g,l. In the usual (ppt) way, therefore, they are
understood as functions of type

(1)			G*L  ->  POW(DIST(G*L)) ,
	
where G,L are the types of g,l, DIST forms distributions and POW forms
powersets. There will be various closure conditions imposed on the POW
above.

Operations outside the module (-external- operations) distinguish
between g and l since, while they have free access to g, they cannot
access l directly. They regard the whole module as a single variable m
(for "module") of type DIST(L) --- thus outside the module one "knows"
the distribution of its internal variables l, but (in general) one does
not know which particular value l has at any time. Writing M for
DIST(L), the type of m, external operations have type

			G*M  ->  POW(DIST(G*M))
			
which, written out, becomes

(2)			G*DIST(L)  ->  POW(DIST(G*DIST(L))) .

We assume in fact that the incoming distributions --- the type M --- are
all "total": they sum to 1 exactly, containing no aborting component.
That is because they are conditional distributions --- a distribution
for l given a particular value of g --- and implicit in "given a
particular value of g" is that termination has occurred. (Nontermination
will be encoded when necessary by a "g-deficit" in the distribution
DIST(G*DIST(L)).)

The knowledge of l's distribution can be exploited -externally- only by
nondeterministic choice, which may choose to set values for external
variables that minimise the probability of their being in some relation
with the internal ones. That knowledge is gained "at runtime" by keeping
track of which internal operations have been called (though one cannot
look inside to see what they actually did), and examining their code to
see what distributions they produce.

[ Aside --- One might argue that similarly the result of internal
-nondeterministic- choices is not directly observable, and thus that the
type M of m should be POW(DIST(L)) rather than simply DIST(L).

The counter-argument, aside from seeking merely to avoid complexity, is
that the internal nondeterministic choices -could- be made visible
externally by the internal demons' publishing beforehand what they
-intend- to do. Thus one assumes that they have. ]

A2-- Internal versus external operations

A program in its entirety, possibly containing a module, is regarded as
an -external- operation and thus has type (2). Since however it
comprises components some of which may be internal (of type (1)), in
forming its overall meaning the two types must be reconciled.

We assume for simplicity (*) that internal operations do not call
external procedures, and proceed as follows.

For each internal operation determine by normal (ppt) means its meaning
is of type (1); for this the external program is completely ignored, and
the module is treated in isolation.

Then convert (described below) the internal operations one-by-one, each
as a whole, from type (1) to type (2) so that they can from that point
on be regarded as external.

Finally determine the meaning of the whole program by combining its
pieces (now all external) according to the "external" semantics of the
program forming operators (external probabilistic choice, external
nondeterminism, sequential composition).

[ Aside --- The effect of the simplifying assumption (*) on the
-algebra- is that we need never consider program expressions in which
external operators occur within internal ones. For example, writing {},
[] for internal, external nondeterminism, we cannot form a program

	(aaa [] bbb) {} (ccc [] ddd) ,
	
and as a result do not have to deal with the "flow-through effect" in
which the two []'s are "polluted" by the {}, becoming {}'s themselves. ]

A3-- External semantics of internal operations

To convert an internal operation, of type

(1)			G*L  ->  POW(DIST(G*L))
			
to the external type

(2)			G*DIST(L)  ->  POW(DIST(G*DIST(L))) ,

first convert the argument G*DIST(L) of (2) to the form DIST(G*L), an
"ordinary" distribution over the unseparated space G*L (in which,
however, only one G-value has non-zero probability).

Then apply the "daggered" (that is, converted to homogeneous form a la
Claire Jones) form of the internal operation to it --- it has type

(3)			DIST(G*L)  ->  POW(DIST(G*L)) ,

and so produces a result of type POW(DIST(G*L)).

Finally, convert each element DIST(G*L) of the result set to the type
DIST(G*DIST(L)) by conditioning on g.

For example, consider the G*L distribution

					l=0  l=1
				
(4)			g=0 	0.2  0.1
			g=1 	0.3  0.2 ,
			
a possible element of a result set of type (3). It is converted to

(5)			(0, (0 {2/3} 1))	@ 0.3
			(1, (0 {3/5} 1))	@ 0.5 ,
			
of type DIST(G*DIST(L)). Note that each L-distribution is total, but
that there is a g-deficit of 1-(.3+.5) = 0.2, indicating 0.2 probability
of abortion.

A4-- External semantics of pure external operations

-Pure- external operations are those that contain no calls on the module
--- they are thus "ordinary" program fragments written in terms of g
alone (with no reference to l). Ordinary (ppt) analysis gives them
meaning of type

(6)			G  ->  POW(DIST(G)) ,

which must be converted to type (2) to be consistent with the presence
of the module.

The conversion is effected simply by noting the incoming L-distribution,
applying the function of type (6) to the incoming g to get an outgoing
g-distribution, and then "re-attaching" that original L-distribution to
each component of the outgoing g distributions.

A5-- Semantics of external probabilistic choice

The effect of probabilistic choice [p] on two distributions sets each of
type

			POW(DIST(G*DIST(L)))
			
is to select elements pairwise (each of type DIST(G*DIST(L)) thus) and
then to combine the distributions weighted by [p] in the usual way.

Note that if p is not a constant (but is a function of the state), it
can be a function only of the global variables g (since it is -external-
probabilistic choice). Since the -initial- value of g is fixed for any
result set, the weight p will be a constant for each occurrence of its
use as above.

A6-- Semantics of external nondeterministic choice

For nondeterministic choice one merely takes the union of the result
sets.

A7-- Closure conditions and their effects

Normal (ppt) closure insists that results sets of distributions are up-,
convex- and Cauchy-closed. Similar conditions are imposed here, but
because of the "two-level" distributions they are slightly more complex.

A7a- Up-closure

If an element of our result set, of type

			DIST(G*DIST(L)) ,
			
has no g-deficit, then (since the l-distributions are total) there is no
"room" for up-closure --- that element is total already. If however
there is a g-deficit, then in the normal way up-closure allows the
probabilities of other G*DIST(L) points in the distribution to increase
to "use it up": call that "g-wise" up-closure. In the example

(5)			(0, (0 {2/3} 1))	@ 0.3
			(1, (0 {3/5} 1))	@ 0.5 ,
			
that would allow an increase to say

(7)			(0, (0 {2/3} 1))	@ 0.4
			(1, (0 {3/5} 1))	@ 0.5 ,
			
in which 0.1 of the aborting behaviour has been used to increase the
probability of (0, (0 {2/3} 1)) from 0.3 to 0.4.

There is however also "general" up-closure. Looking at the equivalent
presentation
					l=0  l=1
				
(4)			g=0 	0.2  0.1
			g=1 	0.3  0.2 ,
			
of example (5) one could use 0.1 of the deficit to produce

					l=0  l=1
				
(8)			g=0 	0.3  0.1
			g=1 	0.3  0.2 ,
			
increasing just the g=l=0 component. Converting that to external form
gives

(9)			(0, (0 {3/4} 1))	@ 0.4
			(1, (0 {3/5} 1))	@ 0.5 ,
			
which differs from (5) and (7) in that the l-component of the first row
has been changed (as well as increasing the row's probability from 0.3
to 0.4).

We impose general up-closure (including g-wise up-closure as a special
case). The "policy" that decision encodes is that external aborting
behaviour is assumed potentially to affect even the -interior- of a
module.

[ Aside --- It does look like up-closure would be simplified if we kept
the distributions always in the (4) rather than the (5) form: for then
it would just be "normal" up-closure of a G*L distribution.
Unfortunately, in general it is possible to have (5)-style distributions
like

(10)		(0, (0 {2/3} 1))	@ 0.5
			(0, (0 {1/3} 1))	@ 0.4 ,
			
in which g-values are repeated. (It is caused by external probabilistic
choice.) The repetition is significant, and would be lost if collapsed
back to the (4)-style. ]

A7b- Convex closure: external

Normally, (external) nondeterministic choice generates --- as well as
the extremes given explicitly --- all possible probabilistic
combinations of the arguments of the choice. Thus one would expect the
result sets

			POW(DIST(G*DIST(L)))
			
to be closed under weighted combination (as in A5) of their elements,
and indeed that closure condition is imposed.

One of its effects is to ensure that external nondeterministic choice is
refined by external probabilistic choice.

A7c- Convex closure: internal

Internal nondeterministic choice should generate all -internal-
probabilistic combinations of its arguments; but when looking at the
external semantics of an operation it is not necessarily evident how it
may have been formed by internal nondeterministic choice. The effect
-externally- of that closure is however that the external result sets
are closed under the following (unary) operator on their elements.

		Take any two (distinct) G*DIST(L) points with the same 
		g-value and "amalgamate" them as shown by this example:

			(0, (0 {3/4} 1))	@ 1/3
			(0, (0 {1/4} 1))	@ 1/2
			
-->			"multiply-in the row probabilities"
			(0, (0 @ 1/4, 1 @ 1/12))
			(0, (0 @ 1/8, 1 @ 3/8))
			
-->			"add the rows"
			(0, (0 @ 3/8, 1 @ 11/24))
			
-->			"normalise"
			(0, 0 [9/20] 1))	@ 5/6.

Internal convex closure is simply forming all such amalgamations, each
generating a new result set in which the two original rows are replaced
by their amalgamation --- and that is imposed as well.

A7d- Cauchy-closure

It's likely that Cauchy-closure occurs naturally.

A7e- Effects of closure

If refinement is taken, as usual, to be subset inclusion of
corresponding result sets, then one effect of closures is to impose
refinements. A more specific effect is to impose equalities.

In the examples to follow some of the implications of the closures are
explored. For the moment note that we have, for example,

		internal nondet		[=		internal prob
		external nondet		[=		external prob
		internal nondet		[=		external nondet, hence
		internal nondet		[=		external prob
		external prob		[=		internal prob, hence
		external nondet		[=		internal prob.
		
Summarising the above gives

		internal nondet		[=		external nondet
		external prob		[=		internal prob
		either nondet		[=		either prob.
		

B--- The relational model: examples

B1-- -Internal- prob is -not- detectable by external nondet

Consider the program

	VAR g:{0,1};
	...
	MODULE M
	  VAR l:{0,1};
	  ...
	  PROC A ==	 l:= (0 {p} 1)
	  ...
	END M;
	...
	M.A; g:= (0 [] 1)

in which (from the module structure) an internal probabilistic
assignment is followed by an external nondeterministic choice. With
normal ppt semantics, the assignment to g would "see" the current value
of l and could, for example, always act to make them equal; with the
modular semantics, the g assignment cannot see l and so they could be
made equal only with some probability.

With the relational semantics, we have first

	(g,0 {q} 1)
--> "expand into g,l distribution"
	(g,0) {q} (g,1)
--> "apply l:= (0 {p} 1)"
	((g,0) {p} (g,1)) {q} ((g,0) {p} (g,1))
--> "idempotence"
	(g,0) {p} (g,1)
--> "collapse"
	(g, 0 {p} 1) ,

in which clearly we have gone the long way round --- it is to be
expected that the assignment l:= (0 {p} 1) would simply set the
l-distribution component to the explicitly-given 0 {p} 1.

Thus the -external- semantics of M.A is

	(g,L)  -->	{ (g, 0 {p} 1) @ 1} .

Continuing with g:= (0 [] 1) we have

	(g, 0 {p} 1)
--> "applying g:= 0, omitting @1"
	{ (0, 0 {p} 1) }

and (g, 0 {p} 1)
--> "applying g:= 1"
	{ (1, 0 {p} 1) }

so that, taking the union we have the overall result that the program
above takes (g,L) to

	{ (0, 0 {p} 1), (1, (0 {p} 1) } ,

a result set containing two elements (both point distributions over
G*DIST(L)) --- and the one which the demon will choose depends on our
postcondition. If are hoping that "g cannot guess l" we would use
postcondition g<>l, for which the first element (0, 0 {p} 1) gives ~p
(that is, 1-p) and the second element gives p; the overall result is
then

	p MIN ~p ,

which we interpret as the minimum guaranteed probability that the module
structure above prevents g guessing l.
	 
B2-- -External- prob -is- detectable by external nondet

Consider now the program

		VAR g:{0,1};
		...
		MODULE M
		  VAR l:{0,1};
		  ...
		  PROC A0 ==  l:= 0
		  PROC A1 ==  l:= 1
		  ...
		END M;
		...
		A0 [p] A1; g:= (0 [] 1)

in which the assignments are made, as before, to the local variable l
-and- there is no trace in the global state of which assignment was made
(whether A0 or A1 was called). The prob choice between them, however, is
external.

The external semantics of A0 is

	(g,L) --> (g,0) ,

in which the 0 denotes the point distribution of l at 0. Similarly for
A1 we have

	(g,L) --> (g,1) ,

and external prob then forms the result set

	{ (g,0) [p] (g,1) }

containing -one- element. Internal convex closure however adds a second
element, giving overall

	{ (g,0) [p] (g,1) , (g, 0 {p} 1) }

for the external semantics of A0 [p] A1.

The effect of the statement g:= (0 [] 1) on the second component was
calculated in B1 --- it was { (0, 0 {p} 1), (1, (0 {p} 1) }. For the
first, however, we get

	{ (0,0), (0,1) } from the (g,0) component, and
	{ (1,0), (1,1) } from the second component,

which "[p]-d" together all four ways gives

	{ (0,0) [p] (1,0),
	  (0,0) [p] (1,1),
	  (0,1) [p] (1,0),
	  (0,1) [p] (1,1) }

and which from closure (internal and external) contains many other
components as well. Concentrating specifically on the postcondition
g<>l, however, the component (second above)

	(0,0) [p] (1,1)

gives 0, showing that in this case we cannot rely at all on g's not
being able to guess l.

We conclude that although g cannot see the assignment being made to l,
and although there is no evidence left in the external state of that
assignment, nevertheless g -did- see which of A0 or A1 was called and
--- from their code --- can deduce the value of l accordingly.

B3-- Mixture of internal and external prob

Write {} and {p} for internal nondet and prob respectively, retaining []
and [p] for the external versions, and consider the program

		l:= (0 {p} 1)  [q]	l:= (0 {r} 1);
		g:= 0 [] 1
		
in which as usual g is trying to guess l (so that we will apply
postcondition g<>l), and l is set by an external prob choice between two
internal prob choices.

Starting with the general (g,L) and ignoring closure we have

	l:= (0 {p} 1)	-->		{ (g, (0 {p} 1)) }
	l:= (0 {r} 1)	-->		{ (g, (0 {r} 1)) }, hence
	
	l:= (0 {p} 1)  [q]	l:= (0 {r} 1)
	-->
	{ (g, (0 {p} 1)) [q] (g, (0 {r} 1)) } .
	
Then applying g:= 0 [] 1 --> gives

	{ (0, (0 {p} 1)), (1, (0 {p} 1)) }
	[q]
	{ (0, (0 {r} 1)), (1, (0 {r} 1)) }

=	{ (0, (0 {p} 1)) [q] (0, (0 {r} 1)) ,
	  (0, (0 {p} 1)) [q] (1, (0 {r} 1)) ,
	  (1, (0 {p} 1)) [q] (0, (0 {r} 1)) ,
	  (1, (0 {p} 1)) [q] (1, (0 {r} 1)) }.
	  
The minimum value of g<>l over those four possibilities is

		(~p)q + (~r)(~q)
	MIN (~p)q + r(~q)
	MIN pq + (~r)(~q)
	MIN pq + r(~q)
	
=	(p MIN ~p) [q] (r MIN ~r).

Taking for example

		l:= (0 {1/3} 1)	 [1/2]	l:= (0 {2/3} 1);
		g:= 0 [] 1 ,
		
in which p=1/3, q=1/2, r=2/3, we have 1/3 for the probability of
establishing g<>l --- thus that g can guess l in 2/3 of the cases. It
does so by observing the resolution of the external [1/2] (even though
it sets no external variables), and then choosing the more likely value
--- at probability 2/3 --- on that side, thus 1 on the left and 0 on the
right.

Note that normal (ppt) reasoning gives 1 for the probability that g can
guess l (since everthing is observable), and that the "matrix model"
gives 1/2 for that probability, since in that case the first statement
is equivalent to the assignment

		l := (0 {1/2} 1) .
		
That is because the matrix model does not distinguish internal and
external operations (and so treats [1/2] as {1/2}, whence the subsequent
collapse to the simple prob choice above): it distinguishes only
internal and external variables.

The current example thus distinguishes the three models.

B4-- Internal versus external nondet: closure gives equality

We now compare the two programs,

		l:= (0 {} 1)
and		l:= (0 [] 1) ,

the first using internal, and the second external nondet, but in both
cases making only internal assignments.

The first statement generates from initial (g,L) the result set

(*)		{ p: [0,1].	 (g, (0 {p} 1)) } ,
		
in which the convex closure represented by p is inherited from the
convex closure of the -internal- semantics for the statement.

The second statement generates the result set

(+)		{ p: [0,1].	 (g,0) [p] (g,1) } ,
		
if we take external convex closure into account (but not yet internal).

Once closure is applied fully --- external to (*) and internal to (+)
--- we find that the result sets are the same, and thus that external
and internal nondet are not distinguished in this case.

We justify that by arguing that the only information that could be
passed out of the module by the internal l:= (0 {} 1) is information
about the -initial- states of its variables l --- however since l is
completely overwritten by the statement, that information is of no use
externally, and in particular offers no advantage over the external l:=
(0 [] 1) in making deductions about the module's internal state.

B5-- Internal versus external nondet: "extra" variables

Reconsider the programs

		l:= (0 {} 1)
and		l:= (0 [] 1) ,

but this time supposing there is a second internal variable m. In this
case we would expect the statements to differ, since the internal nondet
can observe m but the external can't.

Write the incoming state, containing a distribution over l,m jointly, as

		(g, ((0,0) {p} (0,1))  {q}	((1,0) {r} (1,1))) .
		
The first command gives

		({ (g, (0,0)) , (g, (1,0) }	 {p}  { (g, (0,1)) , (g, (1,1) })
		{q}
		({ (g, (0,0)) , (g, (1,0) }	 {r}  { (g, (0,1)) , (g, (1,1) })
		
which, if multiplied out, gives 8 terms. The second command gives just
the two terms

		{ (g, ((0,0) {p} (0,1))	 {q}  ((0,0) {r} (0,1))) ,
		  (g, ((1,0) {p} (1,1))	 {q}  ((1,0) {r} (1,1))) } ,
		  
which simplifies to

		{ (g, (0,0 {pq+r(~q)} 1)) ,
		  (g, (1,0 {pq+r(~q)} 1)) }
		  
in each of which the final value for l is definite, but the initial
distribution for m is retained.

The probability that "l has guessed m" is evaluated by choosing
postcondition l<>m. In the first case, that gives 0 because one of the 8
terms is

		(g, (0,0) {pq+r(~q)}  (1,1)) ;
		
in the second case it gives

(*)		pq+r(~q) MIN (~p)q+(~r)(~q) .
		
[ Aside --- One could argue that the above distinction is meaningless,
since equality of l and m can't be distinguished from the outside
anyway; but that is avoided by including a module operation

		b:= (l<>m)
		
that assigns to the external Boolean b. In the first case (internal
nondet) one cannot assume anything about the final value of b; in the
second case, however, one would have the non-zero probability (*) of b's
being TRUE. ]

C--- The relational model: generalities

C1-- Preserving standard reasoning internally

Since the internal semantics of (internal) commands is "straight ppt"
(followed, as explained in A3 by conversion to external semantics),
ordinary reasoning is wholly preserved while reasoning inside a single
module operation.

An important point, though, is that there is no -external- semantics for
-internal- operators --- which would in fact be a more conventional
approach. That is, one would have just one semantic space (rather than
the two here), and for each primitive command (neither probabilistic nor
nondeterministic) and basic operator (prob, or nondet) both an
-internal- and -external- version. Which version applied would be
determined simply by whether the command or operator was inside or
outside the module; the semantics of a program would be calculated ---
in the usual way --- by combining the meanings of its constituents.

Examples B1 and B2 show why it's hard to take that simple approach. If
there were an external semantics for internal nondet (for example), then
the -external- semantics of

		l:= (0 {p} 1)				(example B1)
		
would be some {p}-determined combination of the external semantics of

		l:= 0
	and l:= 1
	
separately. And it would have to differ from the [p]-determined
combination illustrated in example B2, since otherwise B1 and B2
themselves wouldn't differ.

If we go on to assume (is this justified?) that therefore the external
semantics of

(@)			l:= (0 {p} 1); g:= (0 [] 1)
		
is a {p}-determined combination of

(*)			l:= 0; g:= (0 [] 1)
(+)		and l:= 1; g:= (0 [] 1) ,
	
which would for example be the case in a conventionally styled wp-based
semantics, then there is a problem: both (*) and (+) have 0 probability
of establishing g<>l, while (@) has probability p MIN ~p of doing so ---
thus the {p}-combination would have to combine 0 and 0 to get p MIN ~p.
Yet applied to two copies of (*) (instead of one each of (*) and (+)),
it would have to remain at 0.

It may be possible, but it does seem elusive.

C2-- Preserving standard reasoning externally

Once the modules commands have been (internally) analysed, and converted
to external semantics, to what extent can the program --- now entirely
external, but with a variable m for the whole module along side its own
(global) variables --- be treated with standard ppt reasoning?

The answer seems to be "not entirely" --- the internal structure of m
can't be completely ignored.

The reason is internal convex closure: every internal command (converted
to external) produces result sets with the property that if
(g,m0)@p0 and (g,m1)@p1 occur in the set, then there is another set in
which the two have been replaced by the single

	(g,m0)@p0  "+"  (g,m1)@p1 ,
	
where the "+" is the "amalgamation" at A7c.

Luckily (but it needs to be checked carefully), we seem to have the
following:

	*	all internally-generated external commands are closed.
	*	all purely external primitive commands are closed.
	*	closure is preserved by the external operators.
	
The external operators are prob choice, nondet and (ignored up to now)
sequential composition. If the above is true, then all ppt identities
may be carried over into the external reasoning --- but there may be
more that apply to the modules specifically.

Sequential composition is in fact the only operator that -can- be
applied to the external semantics of internal commands, and it should
give the same answer as the internal version, since

		PROC A1 ==	body1;
		PROC A2 ==	body2
		
		(externally) A1; A2
		
should be the same as

		PROC A0 ==	body1; body2
		
		(externally) A0 .
		
Thus if -it- did not preserve internal convex closure, there would be
some very interesting issues raised.