Tue 25 Aug 2020 04:15 - 04:30 at ICFP Asia 2 - Asia 2 Chair(s): Alan Jeffrey
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.
Mon 24 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
14:30 - 16:30 | |||
14:30 15mTalk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
14:45 15mTalk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
15:00 15mTalk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
15:15 15mTalk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
15:30 15mTalk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
15:45 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
16:00 15mTalk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
16:15 15mTalk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached |
Tue 25 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
02:30 - 04:30 | |||
02:30 15mTalk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
02:45 15mTalk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
03:00 15mTalk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
03:15 15mTalk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
03:30 15mTalk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
03:45 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
04:00 15mTalk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
04:15 15mTalk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached |