SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 11:35 - 11:50 at Zurich E - ICFP 2020 Papers Chair(s): Stefan K. Muller

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.

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
ICFP 2020 PapersSIGPLAN Papers at Zurich E
Chair(s): Stefan K. Muller Illinois Institute of Technology
10:50
15m
Talk
A General Approach to Define Binders using Matching Logic
SIGPLAN Papers
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Ro┼ču University of Illinois at Urbana-Champaign
DOI
11:05
15m
Talk
Denotational Recurrence Extraction for Amortized Analysis
SIGPLAN Papers
Joseph W. Cutler University of Pennsylvania, Dan Licata Wesleyan University, Norman Danner Wesleyan University
DOI
11:20
15m
Talk
Program Sketching with Live Bidirectional Evaluation
SIGPLAN Papers
Justin Lubin University of California at Berkeley, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI
11:35
15m
Talk
Liquid Information Flow Control
SIGPLAN Papers
Nadia Polikarpova University of California at San Diego, Jean Yang Carnegie Mellon University, Deian Stefan University of California at San Diego, USA, Shachar Itzhaky Technion, Armando Solar-Lezama Massachusetts Institute of Technology, Travis Hance Carnegie Mellon University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers