Enforcing Dynamic Interference Policy

Noninterference is the mathematical basis for confidentiality analyses. The idea is to ensure that private data will not be observable at a public level. Understood in a strict way noninterference is a too strong property. Standard every day life examples like password checks or message encryption formally break the noninterference property. In this paper we propose a framework in which it is possible to define an interference policy allowing to define safe data declassification. Moreover this policy is dynamic, i.e. the confidentiality level of data may evolve during computation: think at policies in which you want to express that a user has a limited number of guesses or to the sending of a pay-per-view information. We develop a notion of program safety with relation to a dynamic interference policy and give an algorithm (in the form of an abstract evaluation of the program) to check that a program is safe with relation to a dynamic interference policy.