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 soundness with respect to the operational semantics of the language. We then 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.
CITATION STYLE
Banâtre, J.-P., Bryce, C., & Le Métayer, D. (1994). Compile-time detection of information flow in sequential programs (pp. 55–73). https://doi.org/10.1007/3-540-58618-0_56
Mendeley helps you to discover research relevant for your work.