Information Flow Analysis.

In [20], we specify an information flow analysis for a simple imperative language, using a Hoare logic. The logic facilitates static checking of a larger class of programs than can be checked by extant type-based approaches in which a program is deemed insecure when it contains an insecure subprogram. The logic is based on an abstract interpretation of program traces that makes independence between program variables explicit. Unlike other, more precise, approaches based on Hoare logic, our approach does not require a theorem prover to generate invariants. We demonstrate the modularity of our approach by showing that a frame rule holds in our logic.

In [7], we extend the results of [20] to handle also nontermination sensitive information flow analysis, and show how the logic gives rise to a (provably correct) algorithm for forward slicing.

In [18], we modify the logic of [20] to handle object-oriented languages; to reason about aliasing, ubiquitous in such languages, the information flow logic is built on top of a logic for abstract locations (just as any analysis for higher order functional programs is built on top of a control-flow analysis). The logic enjoys “small” specifications, so as to facilitate modular reasoning; these can be combined by a frame rule. Under certain assumptions, it is possible to compute “strongest postconditions”. Our language permits programmer assertions, in the style of ESC/Java.

In [17], we present an alternative approach to information flow analysis of sequential heap manipulating programs. We use “object flow invariants” to express the information flow properties an object must satisfy; such an invariant may be temporarily violated while an object is being updated but must be restored at the end (when the “scope” of the object is closed). Hence there is no need for explicit reasoning about aliasing. In general, information flow properties are expressed using assertions that are conditional in that they depend on standard Hoare assertions being satisfied. We define an algorithm VCgen which from a program and its desired postcondition generates a precondition which is strong enough to establish the postcondition. VCgen must be supplied with object flow invariants as well as with flow invariants for loops; if these invariants are not strong enough then the verification conditions generated by VCgen cannot be satisfied. The current analysis is intraprocedural.

In [16], we employ the techniques of [17], extended to an interprocedural setting, to enhance the SPARK information flow annotation language with conditional information flow contracts. Unlike [17], we now have a method for automatically inferring loop flow invariants; therefore contracts can be compositionally checked and inferred (the SPARK subset of Ada deliberately omits constructs that are difficult to reason about, such as heap objects; hence we do not need to worry about inferring flow invariants for such). We report on the use of this framework for a collection of SPARK examples; our experiments are based on an implementation that allows various degrees of assertion simplification.

In [14], we extend [16] so as to enable precise compositional specification of information flow in programs with arrays. This has substantial practical impact since SPARK does not allow dynamic allocation of memory and hence, to implement complex data structures, makes heavy use of arrays. These have previously been treated as indivisible entities; flows that involve only particular locations of an array had to be abstracted into flows on the whole array. The main technical novelty of [14] is an algorithm for inferring universally quantified contracts for for loops. We demonstrate the expressiveness of the enhanced contracts, and the effectiveness of the automated verification algorithm, on realistic embedded applications.

In [13], we extend the framework of [14] so that the algorithm for verifying source code compliance to an information flow contract emits formal certificates of correctness, to be checked by the Coq proof assistant. For a core subset of the source language, we have proved in Coq that if a program can be given a certificate which is well-typed then the program does indeed satisfy the semantic information flow properties specified by the certificate.