LWeb: Information Flow Security or Multi-tier Web Applications
LWeb: Information Flow Security or Multi-tier Web Applications
复制标题
DOI：
10.1145/3290388
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Hicks, Michael
中科院分区：
文献类型：
--
作者：
Parker, James;Vazou, Niki;Hicks, Michael
本文介绍了LWEB，这是一个框架，用于在使用数据库中实施基于标签的信息流策略。简而言之，LWEB将Lio Haskell IFC执法库与Yesod Web编程框架结合。该实现有两个部分。首先，我们将LIO的核心提取到单子变压器（Lmonad）中，然后将其应用于Yesod的核心单元。其次，我们扩展了Yesod的表定义DSL和查询功能，以允许在表上定义和执行基于标签的策略，并在查询处理过程中执行它们。 LWEB的政策语言具有表现力，允许动态的每一行政策。我们将LWEB在Lambda（LWEB）微积分中的本质形式化，并在液体haskell中机械化了非干预的证明。该机械化构成了在液体haskell中进行的第一个元攻击。我们还使用LWEB构建了一个托管构建，打破它，修复IT面向安全的编程比赛的实质网站。该网站涉及40个数据表和复杂的政策。与手动检查安全策略相比，LWEB施加了一个适中的运行时开销，在2％至21％之间。它将可信赖的代码库从整个应用程序减少到应用程序代码的1％，而总体代码的21％（在计数lweb时也）。
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).