Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 15:21 - 15:43 at Sala I - Security and Information Flow Chair(s): David Walker

This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod’s core monad. Second, we extend Yesod’s table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb’s policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the $\lambda_{\mathit{LWeb}}$ calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).

Slides (POPL19 Slides.pdf)465KiB

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:21 - 16:27: Security and Information FlowResearch Papers at Sala I
Chair(s): David WalkerPrinceton University
15:21 - 15:43
LWeb: Information Flow Security for Multi-Tier Web Applications
Research Papers
James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park
Link to publication DOI Media Attached File Attached
15:43 - 16:05
From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper
Research Papers
Marco VassenaChalmers University of Technology, Alejandro RussoChalmers University of Technology, Sweden, Deepak GargMax Planck Institute for Software Systems, Vineet RajaniMPI-SWS, Deian StefanUniversity of California San Diego
Link to publication DOI Media Attached File Attached
16:05 - 16:27
Modalities, Cohesion, and Information Flow
Research Papers
Alex KavvosWesleyan University
Link to publication DOI Pre-print File Attached