A logic for information flow analysis with an application to forward slicing of simple imperative programs

We specify an information flow analysis for a simple imperative language, using a Hoare-like 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 a “prelude” semantics which makes independence between program variables explicit. Unlike other, more precise, approaches based on Hoare logics, 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. Finally, we show how our logic can be applied to a program transformation, namely, forward slicing: given a derivation of a program in the logic, with the information that variable image is independent of variable image, the slicing transformation systematically creates the forward image-slice of the program: the slice contains all the commands independent of image. We show that the slicing transformation is semantics preserving.