Reference from ESORICS proceedings

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)

Proceedings table of contents