Liquid Information Flow Control


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.

Mar 5, 2021 5:00 PM

Nadia Polikarpova is an assistant professor at UC San Diego, and a member of the Programming Systems group. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple years as a postdoctoral researcher at MIT. Nadia’s research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award.