A Semantic Approach to Secure Information Flow
http://gatekeeper.dec.com/pub/DEC/SRC/technical-notes/abstracts/src-tn-1997-032.html
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.
----
adam@cs.caltech.edu
Children have such a mystical sense of presence because of the way they
meld their physical perceptions into their imaginations (green field
consciousness).
-- Gayl Lepore