一句话：提出 Lifty，用 liquid types 静态验证敏感数据信息流策略，并自动合成修复补丁。
针对处理敏感数据的数据中心应用，开发者需手工编写策略执行代码，难以保证信息流合规。Lifty 是一种领域特定语言：程序员在数据源上标注声明式安全策略，语言用 liquid types 静态、全自动验证应用是否遵守策略，并能检查复杂且依赖数据的策略。若验证失败，Lifty 通过类型驱动的错误定位与补丁合成给出可证明正确的修复。三个文献案例表明：其策略语言足以表达多种真实策略，类型检查器能快速验证安全程序并发现泄漏，即使移除全部策略执行代码，修复引擎也能在合理时间内自动修补所有泄漏。
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.
@article{PolikarpovaSYIH20,
title = {Liquid information flow control},
author = {Nadia Polikarpova and Deian Stefan and Jean Yang and Shachar Itzhaky and Travis Hance and Armando Solar-Lezama},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408987}
}