Liquid information flow control

摘要: We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of data with declarative security policies, and statically automatically verifies application handles according to policies. Moreover, if verification fails, suggests provably correct repair, thereby easing burden implementing policy enforcing code throughout application. The main insight behind is encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking complex, dependent power our repair mechanism via type-driven error localization patch synthesis. Our experience implement three case studies from literature shows (1) sufficiently specify many real-world (2) checker able verify secure programs find leaks in insecure quickly, (3) even leaves out all code, engine within reasonable time.