# LWeb: Information Flow Security for Multi-tier Web Applications

## TL;DR

LWeb is a framework that enforces fine-grained, label-based information flow policies in web applications, combining formal security proofs with practical implementation and modest runtime overhead.

## Contribution

It introduces a novel label-based policy enforcement framework for web apps, formalizes its security properties, and demonstrates practical effectiveness with minimal overhead.

## Key findings

- LWeb enforces dynamic, label-based policies on tables and rows.
- Formal proof of noninterference in Liquid Haskell.
- Modest runtime overhead of 2% to 21%.

## Abstract

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_{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).