Abstract:

Information-flow control promises strong, end-to-end security. In this talk, I'll present two recent projects that make programming with information-flow control more practical: a new way of writing secure web applications, and a framework for expressive security policies.

Swift is a new, principled approach to building web applications that are secure by construction. Swift automatically partitions application code while providing assurance that the resulting placement of code and data on client and server is secure and efficient. Application code is written as Java-like code, annotated with information flow policies that specify the confidentiality and integrity of information. Using these policies, the compiler partitions a web application into JavaScript code to run on the client, and Java code to run on the server. Code and data are placed to ensure that the specified policies are obeyed, and also to provide good interactive performance. However, security critical code and data are always placed on the server. Swift makes it easier to write secure web applications: the programmer uses just one language, and does not need to worry about the secure or efficient placement of code and data.

Computer systems often have detailed and complicated information security requirements, perhaps derived from legislation, or organizational policy. However, it is difficult to ensure that these requirements are correctly enforced in a system's implementation. We have developed a framework for specifying, reasoning about, and enforcing, two common requirements: declassification and erasure. Declassification occurs when the confidentiality of information is weakened, for example, allowing more people to read. Erasure is the opposite, and occurs when confidentiality is strengthened, for example, allowing fewer people to read, perhaps removing the information from the system entirely. The framework's policies specify when declassification may occur, and when erasure must occur. A security-type system, in conjunction with a trusted runtime system, ensures that the policies are enforced. We have used the policies to implement a secure remote voting service, giving increased assurance that the voting service satisfies its information security requirements.