| The increasing digitalization of individual, business, and government information leads to more sensitive information being used in computer systems. This results in the requirement for modern systems to ensure that sensitive information is not leaked. Information flow control is a programming language-based mechanism that focuses on securing the dissemination of information through programs. Information flow type systems aim to statically guarantee that programs do not permit leaks of sensitive information to unauthorized locations.; This dissertation focuses on improving the usability of information flow type systems, and on developing a new technique for proving a static information flow system is correct. We present a static information flow type inference system for Middleweight Java (MJ) that automatically infers information flow labels, thus avoiding the need for a multitude of program annotations. Additionally, policies need only be specified on IO channels, the critical flow boundary. Our type system includes a high degree of parametric polymorphism, necessary to allow classes to be used in multiple security contexts, and to properly distinguish the security policies of different IO channels. To further facilitate the writing of practical programs, we add downgrading constructs to the language that permit minor leaks of information in explicitly allowable instances. We also describe how users can define top-level security policies for programs, allowing the policy to be easily viewed in the API.; We prove a noninterference property for programs that interactively input and output data: changes to high security input data are not visible at low security outputs. We use a new proof technique to show noninterference using a small-step operational semantics that is augmented with a syntactic representation of the type derivation. This shows the strong correlation between the static type system that is guaranteeing program security and the run-time manipulation of data. |
