A semantic security model.

I Find Karma (adam@cs.caltech.edu)
Mon, 22 Dec 1997 15:11:21 -0800

K.M. Rustan Leino is a really smart guy in formal methods who was once
my officemate here at Caltech. He's at DEC SRC now, and in October
he wrote this cool paper with Rajeev Joshi that I just discovered:

A Semantic Approach to Secure Information Flow


The paper takes the classic problem of secure information flow (as
solved in the 1970s by Denning's lattice model based on Bell/La Padula)
and approaches it from a different mathematical characterization: the
semantic notion of program equality. They use a relational semantics to
establish program correctness with respect to secure information flow,
and they use the weakest precondition semantics for mechanical security
verification. The model is general enough to help with reasoning about
several kinds of communication channels, without using previous
techniques such as compiler data flow analysis and security typing.

The cool thing about the weakest precondition semantics is that it
allows Leino and Joshi to derive a first-order predicate whose validity
implies that no one can deduce any secure information solely from the
publically-witnessed input, output, and termination behaviors.
Furthermore, their approach seems novel both in its handling of
nondeterminism and in its analysis of termination behavior.

The abstract for the paper:

> A classic problem in security is the problem of determining whether a
> given program has secure information flow. Informally, this problem may
> be described as follows: Given a program operating on public and private
> variables, check whether observations of the public variables before and
> after execution reveal any information about the initial values of the
> private variables. Although the problem has been studied for several
> decades, most of the previous approaches have been syntactic in nature,
> often using type systems and compiler data flow analysis techniques to
> analyze program texts. This paper presents a considerably different
> approach to checking secure information flow, based on a semantic
> characterization of security. A semantic approach has several desirable
> features. Firstly, it gives a more precise characterization of security
> than that possible by conservative methods based on type
> systems. Secondly, it applies to any programming constructs whose
> semantics are definable; for instance, nondeterminism and exceptions
> pose no additional problems. Thirdly, it can be applied to reasoning
> about indirect leaking of information through variations in program
> behavior (e.g., whether or not the program terminates). The method is
> also useful in the context of automated verification, since it can be
> used to develop a mechanically-assisted technique for checking whether
> the flow of a given program is secure.

I'm a big believer in Rustan's semantic approaches to objects and to
exception handling, so encountering this paper was a pleasant surprise.


Children have such a mystical sense of presence because of the way they
meld their physical perceptions into their imaginations (green field
-- Gayl Lepore