Liquid Information Flow Control

Abstract

Modern applications handle sensitive user data in complex ways, subject to increasingly complex security policies. A promising approach to enforcing these policies is to use Information Flow Control (IFC) frameworks, which separate policy specification from the application code and automatically enforce policies either dynamically (at run time) or statically (at compile time). While static enforcement is desirable because it catches errors early and avoids run-time overhead, existing static IFC frameworks either lack support for expressive data-dependent policies (necessary in modern applications), or require manual proofs or annotations to be strewed throughout the application code. In this talk I will present Lifty, a static IFC framework that overcomes the limitations of existing static approaches. A Lifty programmer annotates the sources of sensitive data with expressive, data-dependent security policies, and Lifty statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application. The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex policies, and power our repair mechanism via type-driven error localization and patch synthesis.