On declassification and the non-disclosure policy

• Published in: Journal of computer security 2009-01, Vol.17 (5), p.549-597
• Main Authors: Almeida Matos, Ana, Boudol, Gérard
• Format: Article
• Language: English
• ISSN: 0926-227X; 1875-8924
• DOI: 10.3233/JCS-2009-0355

We address the issue of declassification in a language-based security approach. We introduce, in a Core ML-like language with concurrent threads, a declassification mechanism that takes the form of a local flow policy declaration. The computation in the scope of such a declaration is allowed to implement information flow according to the local policy. To take into account declassification, and more generally dynamic flow policies, we introduce a generalization of non-interference, that we call the non-disclosure policy, and we design a type and effect system for our language that enforces this policy. Besides dealing with declassification, our type system improves over previous systems for checking information flow in two directions: first, 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, by ignoring the level of values that are only used for side-effects.