Information Flow Analysis in Logical Form

12 years 5 months ago
Information Flow Analysis in Logical Form
Abstract. 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 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 a Hoare-like 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. Moreover, given an insecure but terminating program, we show how strongest postconditions can be employed to statically generate failure explanations.
Torben Amtoft, Anindya Banerjee
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAS
Authors Torben Amtoft, Anindya Banerjee
Comments (0)