Secure Information Flow by Access Control: A Security Type System of Dual-Access Labels

Programming languages such as Java and C# execute code with different levels of trust in the same process, and rely on a fine-grained access control model for users to manage the security requirements of program code from different sources. While such a security model is simple enough to be used in practice to protect systems from many hostile programs downloaded over a network, it does not guard against information-based attacks, such as confidentiality and integrity violations. We introduce a novel security model, called Dual-Access Label (DAL), to capture information-based security requirements of programs written in these languages. DAL labels extend the access control model by specifying both the accessibility and capability of program code, and use them to constrain information flows between code from different sources. Accessibility specifies the privileges necessary to access the code while capability indicates the privileges held by the code. DAL's security policy places a two-way obligation on both ends of information flow so that they must have sufficient capability to meet the accessibility of each other. Unlike traditional lattice-based security models, our security model offers more flexible information flow relations induced by the security policy that does not have to be transitive. It provides both confidentiality and integrity guarantees while allowing cyclic information flows among code with different security labels, as desired in many applications. We present a generic security type system to enforce possibly intransitive information flow polices, including DAL, statically at compile-time. Such security type system provides a new notion of intransitive noninterference that generalizes the standard notion of transitive noninterference in lattice-based security models.