Abstract
Some information is more confidential than others, or more trustworthy than others. Information flows must therefore be restricted to ensure that confidential information is not divulged, and that incorruptible information is not corrupted. To achieve this, it's not enough to control access to IT resources; you need to implement confidentiality policies, such as those of Bell and LaPadula, or integrity policies, such as those of Biba. We have studied how to control the flow of information through a program, either dynamically, by checks during program execution, or statically, using type systems or program logic applied once and for all to the program. We have introduced the notion of non-interference, a semantic characterization of the absence of illegal flows, and sketched out how to extend it to the declassification of confidential data and the approval of untrusted data.
