Policies and mechanisms for secure information release

Security assurance is an important challenge for modern computing. Intentional information release (declassification) is often crucial for such assurance. Security-critical systems demand expressive policies for information release that are beyond what conventional security models may offer. This thesis studies practical and theoretical aspects of information release. It starts with a case study of implementation a declassification-intensive security protocol in a security-typed language. This, largest up to the publication date, case study suggests patterns for secure programming and demonstrates the multifaceted nature of declassification: from near-innocent relabeling of a ciphertext to dangerous release of secret keys. As confirmed by the case study, declassifications of encrypted data before sending it on a public channel are ubiquitous in security protocols. These declassifications are justified by the usage of strong encryption primitives and secret encryption keys. The thesis introduces cryptographically-masked flows that enable reasoning about information flow in the presence of encryption, decryption, and key generation. We propose a type system that enforces security for a small imperative language with cryptographic primitives, which prevents dangerous program behavior such as giving away a secret key or confusing keys and non-keys. This approach is exemplified with secure implementations of cryptographic protocols. To facilitate reasoning about released keys, the thesis suggests an attacker-centric model of gradual release. The attacker’s knowledge is modeled by the sets of possible secret inputs as functions of publicly observable events. Among the latter we distinguish special release events; the essence of gradual release is that the knowledge must remain constant between releases. Gradual release turns out to be a powerful foundation for release policies, which we demonstrate by formally connecting revelation-based and encryption-based declassification. We also show how gradual release can be enforced by security types and effects. Addressing one aspect of declassification while leaving out the others would not be quite adequate. We present a policy that allows expressing both what is released and where in code it should be released. Moreover, we show that a security type system from the literature (which was designed for treating the what aspect) in fact enforces the combination of what and where policies