A Per Model of Secure Information Flow in Sequential Programs.
This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature and connections to other forms of program analysis. The approach is inspired by (and in the deterministic case equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We also show how the per approach can handle nondeterminism for a first-order language, by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics. We illustrate the usefulness of the compositional nature of the security specifications by presenting a straightforward correctness proof for a simple type-based security analysis.
Introduction
1.1 Motivation
You have received a program from an untrusted
source. Let us call it company M. M promises to
help you to optimise your personal financial invest-
ments, information about which you have stored in
a database on your home computer. The software
limited time), under the condition that
you permit a log-file containing a summary of your
usage of the program to be automatically emailed
back to the developers of the program (who claim
they wish to determine the most commonly used
features of their tool). Is such a program safe
to use? The program must be allowed access to
your personal investment information, and is allowed
to send information, via the log-file, back to
M. But how can you be sure that M is not obtaining
your sensitive private financial information
by cunningly encoding it in the contents of the
innocent-looking log-file? This is an example of
the problem of determining that the program has
secure information flow. Information about your
sensitive "high-security" data should not be able
to propagate to the "low-security" output (the log-
file). Traditional methods of access control are of
limited use here since the program has legitimate
access to the database.
This paper proposes an extensional semantics-based
formal specification of secure information-flow
properties in sequential programs based on
representing degrees of security by partial equiv-
Department of Computer Science, Chalmers University
of Technology and the University of G-oteborg,
fandrei,daveg@cs.chalmers.se
alence relations 1 . The specification clarifies and
unifies a number of specific correctness arguments
in the literature, and connections to other forms
of program analysis. The approach is inspired
by (and equivalent to) the use of partial equivalence
relations in specifying binding-time analysis
[HS91], and is thus able to specify security properties
of higher order functions and "partially confidential
data" (e.g. one's financial database could
be deemed to be partially confidential if the number
of entries is not deemed to be confidential even
though the entries themselves are). We show how
the approach can be extended to handle nondeter-
minism, and illustrate how the various choices of
powerdomain semantics affects the kinds of security
properties that can be expressed, ranging from
termination-insensitive properties (corresponding
to the use of the Hoare (partial correctness) pow-
erdomain) to probabilistic security properties, obtained
when one uses a probabilistic powerdomain.
1.2 Background
The study of information flow in the context of systems
with multiple levels of confidentiality was pioneered
by Denning [Den76, DD77] in an extension
of Bell and LaPadula's early work [BL76]. Den-
ning's approach is to apply a static analysis suitable
for inclusion into a compiler. The basic idea
is that security levels are represented as a lattice
(for example the two point lattice PublicDomain -
TopSecret ). The aim of the static analysis is to
ensure that information from inputs, variables or
processes of a given security level only flows to out-
Equivalence relation is symmetric and transitive
but not necessarily reflexive
puts, variables or processes which have been assigned
a higher or equal security level.
Semantic Foundations of Information
Flow Analysis
In order to verify a program analysis or a specific
proof a program's security one must have a formal
specification of what constitutes secure information
flow. The value of a semantics-based specification
for secure information flow is that it contributes
significantly to the reliability of and the
confidence in such activities, and can be used in
the systematic design of such analyses. Many approaches
to Denning-style analyses (including the
original articles) contain a fair degree of formalism
but arguably are lacking a rigorous soundness
proof. Volpano et al [VSI96] claim to give the
first satisfactory treatment of soundness of Den-
ning's analysis. Such a claim rests on the dissatisfaction
with soundness arguments based on an
instrumented operational e.g., [-rb95] or denotational
semantics e.g., [MS92], or on "axiomatic"
approaches which define security in terms of a program
logic [AR80] without any models to relate
the logic to the semantics of the programming lan-
guage. The problem here is that an "instrumented
semantics" or a "security logic" is just a definition,
not subject to any further mathematical justifica-
tion. McLean points out [McL90] in a related discussion
about the (non language-specific) Bell and
LaPadula model:
One problem is that
LaPadula security properties] constitute
a possible implementation of security,
rather than an abstract specification
of what all secure systems must satisfy.
By concerning themselves with particular
controls over files inside the computer,
rather than limiting themselves to the relation
between input and output, they
make it harder to reason about the re-
This criticism points to more abstract, extensional
notions of soundness, based on, for example, the
idea of noninterference introduced in [GM82].
Semantics-based models of Information
Flow
The problem of secure information flow, or "non-
interference" is now quite mature, and very many
specifications exist in the literature - see [McL94]
for a tutorial overview. Many approaches have
been phrased in terms of abstract, and sometimes
rather ad hoc models of computation. Only more
recently have attempts been made to rephrase and
compare various security conditions in terms of
well-known semantic models, e.g. the use of labelled
transition systems and bisimulation semantics
in [FG45]. In this paper we consider the
problem of information-flow properties of sequential
systems, and use the framework of denotational
semantics as our formal model of compu-
tation. Along the way we consider some relations
to specific static analyses, such as the Security
Lambda Calculus [HR98] and an alternative semantic
condition for secure information flow proposed
by Leino and Joshi [LJ98].
1.3

Overview

The rest of the paper is organised as follows.
Section 2 shows how the per-based condition for
soundness of binding times analysis is also a
model of secure information flow. We show
how this provides insight into the treatment
of higher-order functions and structured data.
Section 3 shows how the approach can be
adapted to the setting of a nondeterministic
imperative language by appropriate use of a
powerdomain-based semantics. We show how
the choice of powerdomain (upper, lower or
convex) affects the nature of the security condition

Section 4 focuses on an alternative semantic
specification due to Leino and Joshi. Modulo
some technicalities we show that Leino's condition
- and a family of similar conditions -
are in agreement with, and can be represented
using our form of specification.
Section 5 considers the problem of preventing
unwanted probabilistic information flows in
programs. We show how this can be solved
in the same framework by utilising a probabilistic
semantics based on the probabilistic
powerdomain [JP89].
Per Model of Information
Flow
In this section we introduce the way that partial
equivalence relations (pers) can be used to model
dependencies in programs. The basic idea comes
from Hunts use of pers to model and construct abstract
interpretations for strictness properties in
higher-order functional programs [Hun90, Hun91],
and in particular its use to model dependencies
in binding-time analysis [HS91]. Related ideas already
occur in the denotational formulation of live-
variable analysis [Nie90].
2.1 Binding Time Analysis as Dependency
Analysis
Given a description of the parameters in a program
that will be known at partial evaluation time
(called the static arguments), a binding-time analysis
must determine which parts of the program
are dependent solely on these known parts
(and therefore also known at partial evaluation
time). The safety condition for binding time analysis
must ensure that there is no dependency between
the dynamic (i.e., non-static) arguments and
the parts of the program that are deemed to be
static. Viewed in this way, binding time analysis
is purely an analysis of dependencies. 2
Dependencies in Security In the security
field, the property of absence of unwanted dependencies
is often called noninterference, after
[GM82]. Many problems in security come down
to forms of dependency analysis. For example, in
the case of confidentiality, the aim is to show that
the outputs of a program which are deemed to be
of low confidentiality do not have any dependence
2 Unfortunately, from the perspective of a partial evalua-
tor, BTA is not purely a matter of dependencies; in [HS95]
it was shown that the pure dependency models of [Lau89]
and [HS91] are not adequate to ensure the safety of partial
evaluation.
on inputs of a higher degree of confidentiality. In
the case of integrity (trust ), one must ensure that
the value of some trusted data does not depend on
some untrusted source.
Some intuitions about information flow Let
us consider a program modelled as a function from
some input domain to an output domain. Now
consider the following simple functions mapping inputs
to outputs: snd : D \Theta E ! E for some sets (or
domains) D and E, and shift and test, functions in
N \Theta N ! N, defined by
Now suppose that (h; l) is a pair where h is some
high security information, and l is low, "public do-
main", information. Without knowing about what
the actual values h and l might be, we know about
the result of applying function snd will be a low
value, and, in the case that we have a pair of num-
bers, the result of applying shift will be a pair with
a high second component and a low first component

Note that the function test does not enjoy the
same security property that snd does, since although
it produces a value which is constructed
from purely low-security components, the actual
value is dependent on the first component of the
input. This is what is known as an indirect information
flow [Den76].
It is rather natural to think of these properties
as "security types":
high \Theta low ! low
high \Theta low ! high \Theta low
test : high \Theta low ! high
But what notion of "type", and what interpretation
of "high" and "low" can formalise these more
intuitive type statements? Interpreting types as
sets of values is not adequate to model "high" and
"low". To track degrees of dependence between inputs
and outputs we need a more dynamic view of a
type as a degree of variation. We must vary (parts
of) the input and observe which (parts of) the output
vary. For the application to confidentiality we
want to determine if there is possible information
leakage from a high level input to the parts of an
output which are intended to be visible to a low
security observer. We can detect this by observing
whether the "low" parts of the output vary in any
way as we vary the high input.
The simple properties of the functions snd and
shift described above can be be captured formally
by the following formulae:
Indeed, this kind of formula forms the core of
the correctness arguments for the security analyses
proposed by Volpano and Smith et al [VSI96,
SV98], and also for the extensional correctness
proofs in core of the Slam-calculus [HR98].
High and Low as Equivalence Relations We
show how we can interpret "security types" in general
as partial equivalence relations. We will interpret
high(for values in D) as the equivalence relation
All D , and low as the relation
all
x All D x 0 (3)
x
For a function f binary relations
iff
For binary relations P , Q we define the relation
Now the security property of snd described by (1)
can be captured by
and (2) is given by
2.2 From Equivalence Relations to Pers
We have seen how the equivalence relations All and
may be used to describe security "properties"
high and low . It turns out that these are exactly
the same as the interpretations given to the notions
"dynamic" and "static" given in [HS91]. This
means that the binding-time analysis for a higher-order
functional language can also be read as a security
information-flow analysis. This connection
between security and binding time analysis is already
e.g. [Thi97] for a comparison of
a particular security type system and a particular
binding-time analysis, and [DRH95] which shows
how the incorporation of indirect information flows
from Dennings security analysis can improve binding
time analyses).
It is worth highlighting a few of the pertinent
ideas from [HS91]. Beginning with the equivalence
relations All and Id to describe high and
low respectively, there are two important extensions
to the basic idea in order to handle
structured data types and higher-order functions.
Both of these ideas are handled by the analysis
of [HS91] which rather straightforwardly extends
Launchbury's projection-based binding-time analysis
[Lau89] to higher types. To some extent [HS91]
anticipates the treatment of partially-secure data
types in the SLam calculus [HR98], and the use of
logical relations in their proof of noninterference.
For structured data it is useful to have more refined
notions of security than just high and low ;
we would like to be able to model various degrees
of security. For example, we may have a list of
records containing name-password pairs. Assuming
passwords are considered high , we might like
to express the fact that although the whole list
cannot be considered low , it can be considered as a
(low \Theta high)list. Constructing equivalence relations
which represent such properties is straightforward
see [HS91] for examples (which are adapted directly
from Launchbury's work), and [Hun91] for a
more general treatment of finite lattices of "bind-
ing times" for recursive types.
To represent security properties of higher-order
functions we use a less restricted class of relations
than the equivalence relations. A partial equivalence
relation (per) on a set D is a binary relation
on D which is symmetric and transitive. If P is
such a per let jP j denote the domain of P , given
by
Note that the domain and range of a per P are
both equal to jP j (so for any x; y 2 D, if x P y
then x P x and y P y), and that the restriction
of P to jP j is an equivalence relation. Clearly, an
equivalence relation is just a per which is reflexive
equivalence relations over
various applicative structures have been used to
construct models of the polymorphic lambda calculus
(see, for example, [AP90]). As far as we are
aware, the first use of pers in static program analysis
is that presented in [Hun90].
For a given set D let Per(D) denote the partial
equivalence relations over D. Per(D) is a meet
semi-lattice, with meets given by set-intersection,
and top element All .
Given pers P 2 Per(D) and Q 2 Per(E), we
may construct a new per (D - E) 2 Per(D ! E)
defined by:
If P is a per, we will write x : P to mean x 2 jP j.
This notation and the above definition of P - Q
are consistent with the notation used previously,
since now
Note that even if P and Q are both total (i.e.,
equivalence relations), P - Q may be partial. A
simple example is All -
we know that given a high input, f returns a low
output. A constant function -x:42 has this prop-
erty, but clearly not all functions satisfy this.
2.3 Observations on Strictness and Termination
Properties
We are interested in the security properties of functions
which are the denotations of programs (in a
Scott-style denotational semantics), and so there
are some termination issues which should address.
The formulation of security properties given above
is sensitive to termination. Consider, for example,
the following
Clearly, if the argument is high then the result
must be high. Now consider the security properties
of the function g ffi f where g the constant function
We might like to consider that g has
low . However, if function application
is considered to be strict (as in ML) then g is not in
Hence the function g ffi f does not have security type
high ! low (in our semantic interpretation). This
is correct, since on termination of an application
of this function, the low observer will have learned
that the value of the high argument was non-zero.
The specific security analysis of e.g. Smith and
Volpano [SV98] is termination sensitive - and this
is enforced by a rather sweeping measure: no
branching condition may involve a high variable.
On the other hand, the type system of the SLam
calculus [HR98] is not termination sensitive in gen-
eral. This is due to the fact that it is based on a
call-by-value semantics, and indeed the composition
could be considered to have a security
type corresponding to "high ! low ". The correctness
proof for noninterference carefully avoids
saying anything about nonterminating executions.
What is perhaps worth noting here is that had they
chosen a non-strict semantics for application then
the same type-system would yield termination sensitive
security properties! So we might say that
lazy programs are intrinsically more secure than
strict ones. This phenomenon is closely related to
properties of parametrically polymorphic functions
[Rey83] 3 . From the type of a polymorphic function
one can predict certain properties about its behaviour
- the so-called "free theorems" of the type
[Wad89]. However, in a strict language one must
add an additional condition in order that the theorems
hold: the functions must be bottom-reflecting
3 Not forgetting that the use of Pers in static analysis
was inspired, in part, by Abadi and Plotkin's Per model of
polymorphic types [AP90]
?). The same side condition
can be added to make the e.g. the type system of
the Slam-calculus termination-sensitive.
To make this observation precise we introduce
one further constructor for pers. If R 2 Per(D)
then we will also let R denote the corresponding
per on D? without explicit injection of elements
from D into elements in D? . We will write R?
to denote the relation in Per(D? ) which naturally
extends R by ? R ?.
Now we can be more precise about the properties
of g under a strict (call-by-value) interpreta-
which expresses that g
is a constant function, modulo strictness. More informatively
we can say that that
which expresses that g is a non-bottom constant
function.
It is straightforward to express per properties in
a subtype system of compositional rules (although
we don't claim that such a a system would be in
any sense complete). Pleasantly, all the expected
subtyping rules are sound when types are interpreted
as pers and the subtyping relation is interpreted
as subset inclusion of relations. For the abstract
interpretation presented in [HS91] this has
already been undertaken by e.g. Jensen [Jen92] and
Hankin and Le M'etayer [HL94].
3 Nondeterministic Information
Flow
In this section we show how the per model of security
can be extended to describe nondeterministic
computations. We see nondeterminism as an important
feature as it arises naturally when considering
the semantics of a concurrent language (al-
though the treatment of a concurrent language remains
outside the scope of the present paper.)
In order to focus on the essence of the problem
we consider a very simplified setting - the analysis
of commands in some simple imperative language
containing a nondeterministic choice operator. We
assume that there is some discrete (i.e., unordered)
domain St of states (which might be viewed as
finite maps from variables to discrete values, or
simply just a tuple of values).
3.1 Secure Commands in a Deterministic
Setting
In the deterministic setting we can take the denotation
of a command C, written JCK, to be a function
in [St ? we mean the
set of strict and continuous maps between domains
D? and E? . Note that we could equally well take
the set of all functions in St ! St ? , which is isomorphic

Now suppose that the state is just a simple partition
into a high-security half and a low-security
half, so the set of states is the product St high \Theta
St low . Then we might define a command C to be
secure if no information from the high part of the
state can leak into the low part:
C is secure
Which is equivalent to saying that JCK : (All \Theta
since we only consider strict
functions. Note that this does not imply that JCK
terminates, but what it does imply is that the termination
behaviour is not influenced by the values
of the high part of the state. It is easy to see that
the sequential composition of secure commands is
a secure command, since firstly, the denotation of
the sequential composition of commands is just
the function-composition of denotations, and sec-
ondly, in general for functions
and R 2 Per(F ) it is easy to verify the soundness
of the inference rule:
3.2 Powerdomain Semantics for Nonde-
A standard approach to giving meaning to a non-deterministic
language - for example Dijkstra's
guarded command language - is to interpret a
command as a mapping which yields a set of re-
sults. However, when defining an ordering on the
results in order to obtain a domain, there is a
tension between the internal order of State ? and
the subset order of the powerset. This is resolved
by considering a suitable powerdomain structure
[Plo76, Smy78]. The idea is to define a preoreder
on the finitely generated subsets 4 of S? in terms of
the order on their elements. By quotienting "equiv-
alent sets" one obtains a partial ordering, each depending
on a different view of what sets of values
should be considered equivalent. Consider the following
three programs (an example from [Plo81])
In the "Hoare" or partial correctness interpretation
the first two programs are considered to be equal
since, ignoring nontermination, they yield the same
sets of outcomes. This view motivates the definition
of the Hoare or lower powerdomain, P L [St ? ].
In the "Smyth" or total correctness interpreta-
tion, programs (2) and (3) are considered equal
(equally bad!) because neither of them can guarantee
an outcome. In the general case this view motivates
the Smyth or upper powerdomain, P U [St ?
[Smy78].
In the "Egli-Milner" interpretation (leading to
the convex or Plotkin powerdomain in the general
case) all three programs are considered to have distinct
denotations.
The three powerdomains are built from a domain
D by starting with the finitely generated (f.g.)
subsets of D? (those non-empty subsets which are
either finite, or contain ?), and a preorder on these
sets. Quotienting the f.g. sets using the associated
equivalence relation yields the corresponding do-
main. We give each construction in turn, and give
an idea about the corresponding discrete powerdo-
main P[St ? ].
ffl Upper powerdomain The upper ordering on
f.g. sets u, v, is given by
In this case the induced discrete powerdomain
is isomorphic to the set of finite non-empty
subsets of St together with St ? itself,
ordered by superset inclusion.
y. Here the induced discrete
powerdomain P L [St ? ] is isomorphic to
4 If a set is infinite then it must contain ?.
the powerset of St ordered by subset inclusion.
This means that the domain [St
is isomorphic to all subsets of St \Theta St - i.e.
the relational semantics.
and u - L v. This is also known as the Egli-
Milner ordering. The resulting powerdomain
is isomorphic to the f.g. subsets of
A few basic properties and definitions on pow-
erdomains will be needed. For each powerdo-
main constructor P[\Gamma] define the order-preserving
which takes each
element a 2 D into (the powerdomain equivalence
class of) the singleton set fag. For each function
there exits a unique extension
of f , denoted f   where f
which is the unique mapping such that
In the particular setting of the denotations of
commands, it is worth noting that JC 1
K would
be given by:
K:
3.3 Pers on Powerdomains
Give one of the discrete powerdomains, P[St ? ], we
will need a "logical" way to lift a per P
to a per in Per(P[St ? ]).
Definition 1 For each R 2 Per(D? ) and each
choice of power domain P[\Gamma], let P[R] denote the
relation on P[D? ] given by
It is easy to check that P[R] is a per, and in particular
that P[Id D?
Henceforth we shall restrict our attention to
the semantics of simple commands, and hence the
three discrete powerdomains P[St ? ].
Proposition 1 For any f 2 [St
any R, S 2 Per(St ? ),
From this it easily follows that the following inference
rule is sound:
3.4 The Security Condition
We will investigate the implications of the security
condition under each of the powerdomain in-
terpretations. Let us suppose that, as before the
state is partitioned into a high part and a low part:
high \Theta St low . With respect to a particular
choice of powerdomain let the security "type"
high \Theta low ! high \Theta low denote the property
In this case we say that C is secure. Now we explore
the implications of this definition on each of
the possible choices of powerdomain:
1. In the lower powerdomain, the security condition
describes in a weak sense termination-
insensitive information flow. For example, the
program
(h is the high part of the state) is considered
secure under this interpretation but the termination
behaviours is influenced by h (it can
fail to terminate only when
2. In the upper powerdomain nontermination is
considered catastrophic. This interpretation
seems completely unsuitable for security unless
one only considers programs which are
"totally correct" - i.e. which must terminate
on their intended domain. Otherwise, a possible
nonterminating computation path will
mask any other insecure behaviours a term
might exhibit. This means that for any program
C, the program C 8 loop is secure!
3. The convex powerdomain gives the appropriate
generalisation of the deterministic case in
the sense that it is termination sensitive, and
does not have the shortcomings of the upper
powerdomain interpretation.
4 Relation to an Equational
Characterisation
In this section we relate the Per-based security condition
to a proposal by Leino and Joshi [LJ98].
Following their approach, assume for simplicity we
have programs with just two variables: h and l
of high and low secrecy respectively. Assume that
the state is simple a pair, where h refers to the first
projection and l is the second projection.
In [LJ98] the security condition for a program
C is defined by
where "=" stands for semantic equality (the style
of semantic specification is left unfixed), and HH is
the program that "assigns to h arbitrary values" -
aka "Havoc on H". We will refer to this equation as
the equational security condition. Intuitively, the
equation says that we cannot learn anything about
the initial values of the high variables by variation
of the low security variables. The postfix occurrences
of HH on each side mean that we are only
interested in the final value of l. The prefix HH
on the left-hand side means that the two programs
are equal if the final value of l does not depend on
the initial value of h.
In relating the equational security condition to
pers we must first decide upon the denotation of
HH . Here we run into some potential problems
since it is necessary in [LJ98] that HH always
terminates, but nevertheless exhibits unbounded
nondeterminism. Although this appears to pose
no problems in [LJ98] (in fact it goes without
mention), to handle this we would need to work
with non-continuous semantics, and powerdo-
mains for unbounded nondeterminism. Instead, we
side-step the issue by assuming that the domain of
h, St high , is finite.
Secondly we must find common ground for our
semantic interpretation. It is not the style of semantic
definition that is important (viz. operational
vs denotational vs axiomatic), but rather
the interpretation of nondeterminism itself. Leino
and Joshi consider two styles of interpretation with
different treatments of nondeterminism: the relational
interpretation (corresponding to the choice
of the lower powerdomain) and the wlp/wp seman-
tics, which corresponds to the convex powerdomain
interpretation. Leino and Joshi claim that considering
a relational semantics, the security condition
is equivalent to a notion used elsewhere in the lit-
erature. As we shall see, the relational semantics
interpretation of the security condition allows programs
to leak information via their termination be-
haviour, so this observation is not entirely correct.
4.1 Equational Security and Projection
Analysis
A first observation is that the the equational security
condition is strikingly similar to the well-known
form of static analysis for functional programs
known as projection analysis [WH87]. Given
a function f , a projection analysis aims to find projections
(continuous lower closure operators on the
domain) ff and fi such that
For (generalised) strictness analysis and dead-
variable analysis, one is given fi, and ff is to be
determined; for binding time analysis [Lau89] it is
a forwards analysis problem: given ff one must determine
some fi.
For strict functions (e.g., the denotations of
commands) projection analysis is not so readily ap-
plicable. However, in the convex powerdomain HH
is rather projection-like, since it effectively hides
all information about the high variable; in fact it
is an embedding (an upper closure operator) so the
connection is rather close.
4.2 The equational security condition is
subsumed by the per security conditio

Hunt [Hun90] showed that projection properties of
the form fi could be expressed naturally
as a per property of the
for equivalence relations derived from ff and fi by
relating elements which get mapped to the same
point by the corresponding projection.
Using the same idea we can show that the per-
based security condition subsumes the equation
specification in a similar manner.
We will establish the following:
Theorem 1. For any command C
iff
high \Theta low ! high \Theta low :
The idea will be to associate an equivalence relation
to the function HH . More generally, for any
command C let ker(C), the kernel of C, denote
the relation on P[St ?
Define the extension of ker(C) by
A ker   (C) B () JCK
Recall the per interpretation of the type signature
of C.
high \Theta low ! high \Theta low
Observe that (All \Theta Id) since for any
The proof of the theorem is based on this observation
and on the following two facts:
Let us first prove the latter fact by proving a
more general statement similar to Proposition 3.1.5
from [Hun91] (the correspondence between projections
and per-analysis). Note that we do not use
the specifics of the convex powerdomain semantics
here, so the proof is valid for any of the three
choices of powerdomain.
Theorem 2. Let us say that a command B is
idempotent iff JB; JBK. For any commands
C and D, and any idempotent command B
Proof.
and JB; C; DKs 1
. Thus s 1
implies that
, since JBKs 1
, and
by idempotence, which
implies
Corollary. Since JHH K is idempotent we can
conclude that
It remains to establish the first fact.
Theorem 3. P[All \Theta
Proof.
Suppose A P[All \Theta need to show
JHH K
bottom-reflecting
((): For the other direction assume JHH K
JHH K   B.
Thus, the equational and per security conditions
in this simple case are equivalent.
5 A Probabilistic Security Conditio

There are still some weaknesses in the security condition
when interpreted in the convex powerdo-
main when it comes to the consideration of non-deterministic
programs. In the usual terminology
of information flow, we have considered possibilistic
information flows. The probabilistic nature of
an implementation may allow probabilistic information
flows for "secure" programs. Consider the
program
This program is secure in the convex powerdomain
interpretation since regardless of the value of h, the
value of l can be any value in the range 99g.
But with a reasonably fair implementation of the
nondeterministic choice and of the randomised as-
signment, it is clear that a few runs of the program,
for a fixed input value of h, could yield a rather
clear indiction of its value by observing only the
possible final values of l:
- from which we might reasonably conclude that
the value of h was 2.
To counter this problem we consider probabilistic
powerdomains [JP89] which allows the probabilistic
nature of choice to be reflected in the semantics
of programs, and hence enables us to capture
the fact that varying the value of h causes a
change in the probability distribution of values of
l.
In the "possibilistic" setting we had the denotation
of a command C to be a function in [St ? !
In the probabilistic case, given an input
to C not only we keep track of possible outputs, but
also of probabilities at which they appear. Thus,
we need to consider a domain E [St ? ] of distributions
or evaluations over St ? . The denotation of
C is going to be a function in [St
Let us first present the general construction of
probabilistic powerdomain. If D is an inductively
complete partial order (ipo for short, it has lubs
of directed subsets, and it is countable), then the
probabilistic powerdomain of evaluations E [D] is
built as follows. An evaluation on D, -, is a function
from D to [0; 1] such that
E [D] to be the set of evaluations on D partially
ordered by - iff 8d 6= ?: -d -d.
Define the point-mass evaluation j D (x) for an
ae
0; otherwise.
A series of theorems from [JP89] proves that
is an ipo with directed lubs defined
pointwise, and with a least element
To lift a function f :
we define the extension of f by
The structure (E [D]; j D (x);  ) is a Kleisli triple.
and thus we have a canonical way of composing the
probabilistic semantics of any two given programs.
are
such. Then the lifted composition (g   ffi f)   can be
computed by one of the Kleisli triple laws as g   ffif   .
The next step towards the security condition is
to define how pers work on probabilistic powerdo-
mains. Recall the definition for pers on powerdo-
mains introduced in section 3. If R 2 Rel(D) then
for
To lift pers to E [D] we need to consider a definition
which takes into consideration the whole of
each R-equivalence class in one go.
Define the per relation E [R] on E [D] for - 2
where [d] R , as usual, stands for the R\Gammaequivalence
class which contains d. Naturally, -
As an example, consider E[(All \Theta Id) ? ] Two distributions
- and - in (All \Theta Id) ? ! [0; 1] are equal
if the probability of any given low value l in the
left-hand distribution, given by
h -(h; l), is equal
to the probability in the right hand distribution,
namely
To make sure we have built a stronger security
model, let us prove that the Egly-Milner power-
domain security condition follows from the probabilistic
powerdomain one. In other words,
Theorem 4. Suppose R and S are equivalence
relations on D. For any command C we have
R -E [S] implies JCK C
Proof. For some a; b 2 D let
deduce a R b =)
-e. What we need
to prove is a R b =) JCK C a P C [S] JCK C b. So,
assume a R b and let us show that
Take any x 2 JCK C a. Observe, that -x ? 0,
since if x is a possible output of program C run on
data a, then the probability of getting this output
must be greater then 0. Therefore,
-e. There must exist a y 2 [x] S such that
-y ? 0. Thus, y is a possible output of program
C run on data b, and y 2 JCK C b. y 2 [x] S implies
Let us derive the probabilistic powerdomain security
condition for the case of two variables h and
l and domain . C is secure iff
l
l
-e
low :-? &
h 02St high
So, a command C is secure iff
and
h2St high
h2St high
for any i l
h and o l . Intuitively the equation
means that if you vary i h the distribution of low
variables (the sums provide "forgetting" the highs)
does not change.
Let us introduce probabilistic powerdomain semantics
definitions for some language constructs.
Here we omit the E-subscripts to mean the probabilistic
semantics. Given two programs
such
that JC 1
the composition of two program semantics
is defined by
The semantics of the uniformly distributed nondeterministic
choice
is defined by
Consult [JP89] to get a full account on how to define
the semantics of other language constructs.
Example. Recall the program
Let us check the security condition on it. Take
The left-hand
side is
whereas the right-hand side is
So, the security condition does not hold and the
program must be rejected.
We recently became aware of probabilistic security
type-system due to Volpano and Smith [VS98]
with a soundness proof based on a probabilistic
operational semantics. Although the security
condition that they use in their correctness argument
is not not directly comparable - due to
the fact that they consider parallel deterministic
threads and a non-compositional semantics - we
can easily turn their examples into nondeterministic
sequential programs with the same probabilistic
behaviours, and it seems (although we have not
checked all of the details) that their examples can
all be verified using our security condition.
6 Conclusions
There are many possible extensions to the ideas
we have sketched, and also many limitations. We
consider a few:
Multi-level security There is no problem with
handling lattices of security levels rather than the
simple high-low distinction. But one cannot expect
to assign any intrinsic semantic meaning to
such lattices of security levels, since they represent
a "social phenomenon" which is external to the
programming language semantics. In the presence
of multiple security levels one must simply formulate
conditions for security by considering information
flows between levels in a pairwise fashion
(although of course a specific static analysis is able
to do something much more efficient).
Downgrading and Trusting There are operations
which are natural to consider but which
cannot be modelled in an obvious way in an extensional
framework. One such operation is the
downgrading of information from high to low without
losing information - for example representing
the secure encryption of high level information.
This seems impossible since an encryption operation
does not lose information about a value and
yet should have type high ! low - but the only
functions of type high ! low are the constant func-
tions. An analogous problem arises with -rbaek
and Palsberg's trust primitive if we try to use pers
to model their integrity analysis [-P97].
Operational Semantics We are not particularly
married to the denotational perspective
on programming language semantics. There are
also interesting operational formulations of pers
on a higher-order language, based on partial-
bisimulations. We hope to investigate these further

Constructing Program Analyses Although
the model seems useful to compare other formali-
further work is needed to show that it can
assist in the systematic design of program analyses.
Concurrency Handling nondeterminism can be
viewed as the main stepping stone to formulating
a language-based security condition for concurrent
languages, but this remains a topic for further
work.



--R

A per model of polymorphism and recursive types.
An axiomatic approach to information flow in programs.
Secure Computer Systems: Unified Exposition and Multics Interpretation.

A lattice model of secure information flow.
Semantic foundations of binding-time analysis for imperative programs
A classification of security properties for process algebra.
Security policies and security models.

The SLam calculus: Programming with secrecy and integrity.
Binding Time Analysis: A New PERspec- tive
A semantic model of binding times for safe partial evaluation.
PERs generalise projections for strictness analysis.
Abstract Interpretation of Functional Languages: From Theory to Practice.
Abstract Interpretation in Logical Form.
A probabilistic powerdomain of evaluations.
Projection Factorisations in Partial Evaluation.
A semantic approach to secure information flow.
The specification and modeling of computer security.
models.
A security flow control algorithm and its denotational semantics correctness proof.



A powerdomain con- struction
"Pisa Notes"
Types, abstraction and parametric polymorphism.
Journal of Computer and Systems Sciences
Secure information flow in a multi-threaded imperative language
University of Nottingham (submitted for publication)
Probabilistic noninterference in a concurrent language.
A sound type system for secure flow anal- ysis
Theorems for free.
Projections for strictness analysis.
--TR

--CTR
Kyung Goo Doh , Seung Cheol Shin, Detection of information leak by data flow analysis, ACM SIGPLAN Notices, v.37 n.8, August 2002
Pablo Giambiagi , Mads Dam, On the secure implementation of security protocols, Science of Computer Programming, v.50 n.1-3, p.73-99, March 2004
Stephen Tse , Steve Zdancewic, Translating dependency into parametricity, ACM SIGPLAN Notices, v.39 n.9, September 2004
Sebastian Hunt , David Sands, On flow-sensitive security types, ACM SIGPLAN Notices, v.41 n.1, p.79-90, January 2006
Nick Benton , Peter Buchlovsky, Semantics of an effect analysis for exceptions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
Aslan Askarov , Andrei Sabelfeld, Localized delimited release: combining the what and where dimensions of information release, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
Anindya Banerjee , Roberto Giacobazzi , Isabella Mastroeni, What You Lose is What You Leak: Information Leakage in Declassification Policies, Electronic Notes in Theoretical Computer Science (ENTCS), 173, p.47-66, April, 2007
Gilles Barthe , Leonor Prensa Nieto, Formally verifying information flow type systems for concurrent and thread systems, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA
Nick Benton, Simple relational correctness proofs for static analyses and program transformations, ACM SIGPLAN Notices, v.39 n.1, p.14-25, January 2004
Roberto Giacobazzi , Isabella Mastroeni, Abstract non-interference: parameterizing non-interference by abstract interpretation, ACM SIGPLAN Notices, v.39 n.1, p.186-197, January 2004
Mads Dam, Decidability and proof systems for language-based noninterference relations, ACM SIGPLAN Notices, v.41 n.1, p.67-78, January 2006
Torben Amtoft , Anindya Banerjee, A logic for information flow analysis with an application to forward slicing of simple imperative programs, Science of Computer Programming, v.64 n.1, p.3-28, January, 2007
Steve Zdancewic , Andrew C. Myers, Secure Information Flow via Linear Continuations, Higher-Order and Symbolic Computation, v.15 n.2-3, p.209-234, September 2002
Heiko Mantel , Andrei Sabelfeld, A unifying approach to the security of distributed and multi-threaded programs, Journal of Computer Security, v.11 n.4, p.615-676, 01/01/2004
Andrew C. Myers , Andrei Sabelfeld , Steve Zdancewic, Enforcing robust declassification and qualified robustness, Journal of Computer Security, v.14 n.2, p.157-196, January 2006
Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005
powerdomains;semantics;noninterference;confidentiality;partial equivalence relations;security;probabilistic covert channels