Information-flow security policies are an appealing way of specifying confidentiality and integrity policies in information systems. Most previous work on language-based security has assumed that programs run in a closed, managed environment and that they use potentially unsafe constructs, such as declassification, to interface to external communication channels, perhaps after encrypting data to preserve its confidentiality. This situation is unsatisfactory for systems that need to communicate over untrusted channels or use untrusted persistent storage, since the connection between the cryptographic mechanisms used in the untrusted ent and the abstract security labels used in the trusted language environment is ad hoc and unclear. This paper addresses this problem in three ways: First, it presents a simple, security-typed language with a novel m called packages that provides an abstract means for creating opaque objects and associating them with security labels; well-typed program...
Jeffrey A. Vaughan, Steve Zdancewic