Third European Symposium on Research in Computer Security (ESORICS 94)
Compile-time Detection of Information Flow in Sequential Programs
Jean-Pierre Banâtre, Ciaran Bryce, Daniel Le Métayer
Keywords : formal verification, program analysis, verification tools, computer security, information flow
Abstract : We give a formal definition of the notion of information flow for a simple guarded command language. We propose an axiomatisation of security properties based on this notion of information flow and we prove its soudness with respect to the operational semantics of the language. We the identify the sources of non determinism in proofs and we derive in successive steps an inference algorithm which is both sound and complete with respect to the inference system.
(Pages 55-73)