Lifty

Lifty is 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.

Paper

Lifty has appeared at ICFP'20 [conference version] [extended version]

Source code

The source code is publicly available here

Examples

We have assembled a set of small but challenging benchmarks that showcase what you can do with Lifty. Click on the links below to observe Lifty in action via our web interface.

• Tiny verification examples
• The EDAS leak
• EDAS: multiple patches
• EDAS: self-referential policies
• Search papers by author
• Sort papers by score
• Broadcast
• The HotCRP password leak
• The AirBnB phone number leak
• The James Comey leak