We explore the idea of integrating security policies into the programming environment and the run-time system. A programming language that incorporates security policies can help programmers reason about the security of the software they are building. We examine how this approach works in the context of the security- typed programming language Jif, which allows programmers to express both information flow policies for confidentiality and integrity, and access control policies. The compiler and run-time system use this added information to enforce strong security properties such as noninterference and robustness.

A variety of language mechanisms make this approach expressive enough to build real software: support for rich language features such as objects and exceptions, automatic inference of security policies, constrained parameterization over security policies, and dependent types that capture security policies determined at run time.

Mechanisms are needed for relaxing confidentiality and integrity policies, but noninterference no longer holds once these mechanisms are used. What can we say about security? We show that a robustness property captures the idea that the adversary cannot cause information to become visible to itself.

Integrating security policies into the program yields an opportunity to raise the level of abstraction at which we build software. Modern applications are difficult to build securely. They are distributed applications, so applications need to be secure even when the adversary partially controls the network and perhaps also some of the host machines running the application. Yet programming these applications also requires attention to a host of low-level details that obscure program logic.

By exposing security policies to the compiler and run-time system, it becomes possible for these layers to automatically synthesize security enforcement mechanisms such as partitioning and replication of code and data, digital signatures and encryption, and network protocols. The result is not only a higher level of abstraction for building secure software, but also stronger assurance that the security mechanisms being used do enforce the security requirements of the application.

We look at how different kinds of policies—for confidentiality and integrity—can be used automatically to drive the compilation of high-level annotated code into target code that employs a variety of security mechanisms. This approach can be used to make web applications easier to build securely and efficiently.