Typing Secure Information Flow: Declassification and Mobility
Ana Almeida Matos · 2006
We address the issue of confidentiality and declassification in a language-based security approach. We study, in particular, the use of refined type and effect systems for statically enforcing flexible information flow policies over imperative higher-order languages with concurrency. A general methodology for defining and proving the soundness of the type and effect system with respect to such properties is presented. We consider two main topics : The long-standing issue of finding a flexible information control mechanism that enables declassification. Our declassification mechanism takes the form of a local flow policy declaration that implements a local information flow policy. The largely unexplored topic of controlling information flow in a global computing setting. Our network model, which naturally generalizes the local setting, includes a notion of domain, and a standard migration primitive for code and resources. New forms of security leaks that are introduced by code mobility are revealed. In both the above settings, to take into account dynamic flow policies we introduce generalizations of non-interference, respectively named the non-disclosure and the non-disclosure for networks policies. Their implementation is supported by a concrete presentation of the security lattice, where confidentiality levels are sets of principals, similar to access control lists.