Abstract:
We investigate the issue of typing confidentiality in a language-based
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.