一句话：提出 LWeb，将 LIO 信息流控制与 Yesod 结合，在数据库 Web 应用中执行标签策略并机器化证明无干扰。
针对数据库支持的 Web 应用缺乏端到端信息流安全的问题，LWeb 将 Haskell 的 LIO IFC 库与 Yesod Web 框架结合：把 LIO 核心抽取为 monad transformer LMonad 并应用于 Yesod 核心 monad，同时扩展 Yesod 的表定义 DSL 和查询功能，以支持并执行基于标签的表级和行级动态策略。作者用 λLWeb 演算形式化其本质，并在 Liquid Haskell 中机器化证明无干扰，这也是首个在 Liquid Haskell 中完成的理论证明。案例为 Build it, Break it, Fix it 竞赛网站，含 40 张表；运行时开销 2% 到 21%，可信代码库从整个应用缩减到应用代码的 1%，计入 LWeb 后整体为 21%。
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 λ 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).
@article{paperbot635,
title = {LWeb: information flow security for multi-tier web applications},
author = {James Parker and Niki Vazou and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290388}
}