On Typing Information Flow

Abstract. We investigate the issue of typing confidentiality in a languagebased information-flow security approach, aiming at improving some previously proposed type systems, especially for higher-order languages with mutable state `a la ML. We show that the typing of terminations leaks can be largely improved, by particularizing the case where the alternatives in a conditional branching both terminate. Moreover, we also provide a quite precise way of approximating the confidentiality level of an expression, that ignores the level of values used for side-effects only.

• Type: Conference
• Year: 2005
• Where: ICTAC
• Authors: Gérard Boudol
• Keywords: ICTAC 2005, Information-flow Security Approach, Mutable State, Terminations Leaks