  We present Lifty, a domain-specific language for data-centric applications
that manipulate sensitive data. A Lifty programmer annotates the sources of
sensitive data with declarative security policies, and the language 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, data dependent policies, and power our
repair mechanism via type-driven error localization and patch synthesis. Our
experience using Lifty to implement three case studies from the literature
shows that (1) the Lifty policy language is sufficiently expressive to specify
many real-world policies, (2) the Lifty type checker is able to verify secure
programs and find leaks in insecure programs quickly, and (3) even if the
programmer leaves out all policy enforcing code, the Lifty repair engine is
able to patch all leaks automatically within a reasonable time.

Programming Languages