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 sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data accor...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2021
|
| Online Access: | https://hdl.handle.net/1721.1/135545 |
| _version_ | 1826201037659176960 |
|---|---|
| author | Polikarpova, Nadia Stefan, Deian Yang, Jean Itzhaky, Shachar Hance, Travis Solar-Lezama, Armando |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Polikarpova, Nadia Stefan, Deian Yang, Jean Itzhaky, Shachar Hance, Travis Solar-Lezama, Armando |
| author_sort | Polikarpova, Nadia |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T11:45:40Z |
| format | Article |
| id | mit-1721.1/135545 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T11:45:40Z |
| publishDate | 2021 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1355452023-12-14T15:07:14Z Liquid information flow control Polikarpova, Nadia Stefan, Deian Yang, Jean Itzhaky, Shachar Hance, Travis Solar-Lezama, Armando Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory 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. 2021-10-27T20:23:56Z 2021-10-27T20:23:56Z 2020 2021-03-23T17:17:58Z Article http://purl.org/eprint/type/JournalArticle https://hdl.handle.net/1721.1/135545 en 10.1145/3408987 Proceedings of the ACM on Programming Languages Creative Commons Attribution 4.0 International license https://creativecommons.org/licenses/by/4.0/ application/pdf Association for Computing Machinery (ACM) ACM |
| spellingShingle | Polikarpova, Nadia Stefan, Deian Yang, Jean Itzhaky, Shachar Hance, Travis Solar-Lezama, Armando Liquid information flow control |
| title | Liquid information flow control |
| title_full | Liquid information flow control |
| title_fullStr | Liquid information flow control |
| title_full_unstemmed | Liquid information flow control |
| title_short | Liquid information flow control |
| title_sort | liquid information flow control |
| url | https://hdl.handle.net/1721.1/135545 |
| work_keys_str_mv | AT polikarpovanadia liquidinformationflowcontrol AT stefandeian liquidinformationflowcontrol AT yangjean liquidinformationflowcontrol AT itzhakyshachar liquidinformationflowcontrol AT hancetravis liquidinformationflowcontrol AT solarlezamaarmando liquidinformationflowcontrol |