英语原文共 17 页
数据库支持的应用程序的精确、动态信息流
Jean Yang Carnegie Mellon University and Harvard Medical School, USA
Travis Hance Dropbox, USA
Thomas H. Austin San Jose State University, USA
Armando Solar-Lezama Massachusetts Institute of Technology, USA
Cormac Flanagan University of California, Santa Cruz, USA
Stephen Chong Harvard University, USA
摘要
我们提出了一种跨应用程序和数据库进行动态信息流控制的方法。我们的方法减少了所需的策略代码数量，在应用程序和数据库中生成正式的保证，与现有的相关数据库实现协同工作，并可扩展到实际的应用。在本文中，我们提出了一个从应用程序代码和数据库查询中考虑信息流策略的编程模型，为基础的lambda;JDB核心语言提供了动态语义，并证明了语义的终止不敏感、不干涉和策略遵从性。我们在Jacqueline（一个python Web框架）中实现了这些想法，并通过三个应用程序案例研究来证明其可行性：一个课程管理器、一个健康记录系统和一个用于运行学术研讨会的会议管理系统。我们表明，与传统的手工编码策略检查的应用程序相比，Jacqueline应用程序具有1）更小的可信计算基础，2）更少的策略代码行，以及2）合理的、通常可以忽略的日常开支。
类别和主题描述 D.3.3[编程语言]：语言结构和特性
通用术语 框架、安全性
关键词 Web框架，信息流
1、介绍
从社会网络到电子健康记录系统，程序越来越多地处理敏感数据。由于信息泄漏通常是由程序员错误引起的，减少泄漏的一个有希望的方法是减少出现程序员错误的机会。
保护Web应用程序的主要挑战涉及推理应用程序和数据库中敏感数据的流动。根据OWASP报告[42]，错误经常发生在组件边界。实际上，推理敏感数据如何通过应用程序代码和数据库查询进行推理的难度导致系统从HotCRP会议管理系统[3]泄漏到社交网站Facebook [47]。最近的HotCRP错误的补丁涉及跨应用程序代码和数据库查询的策略检查。
信息流控制对于保护应用程序 - 数据库边界很重要[15，18，29，42]。这是因为泄漏通常涉及敏感值的计算结果，而不是敏感值本身。为了减少无意泄漏的机会，我们提出了一种与政策无关的方法[7，48]。使用这种方法，程序员可以从应用程序代码和数据库查询中分解出信息流策略的实现。系统管理策略，无需信任剩余的代码。因此，该程序一次指定每个策略，而不是在整个程序中重复交织的检查。因此，与策略无关的程序需要较少的策略代码。我们在图1中说明了这些差异。
支持Web应用程序的不可知策略编程需要框架在应用程序和数据库之间强制执行信息流策略。如图1所示，标准Web程序使用应用程序运行时和数据库运行。一种对象关系映射（ORM），用于调解两者之间的交互。我们的Web框架使用策略不可知的应用程序运行时和专门的ORM来调解策略不可知的应用程序代码和策略不可知的数据库查询之间的交互。
图1 与策略无关的Web服务器相比，标准Web服务器中的应用程序体系结构
我们的解决方案有三个主要部分：1）支持不可知政策的数据库查询；2）在整个应用程序和数据库中提供正式保证；3）解决实际可行性问题。我们扩展了之前关于Jeeves编程语言[7，48]的工作，该语言为简单的命令式语言定义了一个不可知策略的语义。与基于语言的方法一样，Jeeves的担保仅在Jeeves运行时内扩展。由于Web应用程序出于性能原因依赖于商品数据库，因此与外部数据库的互操作非常重要。接下来的挑战是，以一种既能利用现有数据库实现又能提供强有力保证的方式，支持数据库查询的不可知策略编程。
我们提供了分面数据库，用于支持策略不相关的数据库查询。Jeeves运行时基于查看输出的用户的权限执行不同的计算。由于可能事先不知道查看器，因此运行时使用分面执行来模拟同时执行。分面值是一个值的运行时表示，它可能因执行而不同。从语义上讲，分面数据库存储分面值并执行分面查询执行。我们展示了如何使用分面对象关系映射（FORM）来使用关系数据库嵌入分面值，并且令人惊讶的是，仅通过操纵元数据来支持分面查询执行。FORM管理复杂的依赖关系，允许策略查询它保护的数据。
接下来我们展示了与分面数据库的互操作产生了强有力的保证。我们使用关系运算符扩展Jeeves的核心语言，以创建lambda;JDB核心语言。我们为lambda;JDB提供动态分面执行语义，并证明终止不敏感的非干扰和策略合规性。形式化与使用现有数据库实现的实现策略紧密对应，同时产生简明的证明。
为了支持实际应用，我们制定了“Early Pruning”优化。虽然模拟多次执行对于推理是合乎需要的，但是在实践中探索多次执行可能是昂贵的。“Early Pruning”优化允许程序使用程序假设来安全地探索更少的执行。此优化对于Web应用程序特别有用，其中通常可以使用会话用户来预测查看器。使用“Early Pruning”性能甚至可能比手动编码检查更好，因为运行时可以只检查策略一次而不是在整个执行过程中重复检查。
最后，我们证明了实际可行性。我们介绍Jacqueline，一个基于Python的Django [1]框架的Web框架。我们使用Jacqueline构建了几个应用案例研究，包括我们为部署学术研讨会而部署的会议管理系统。案例研究表明，使用Jacqueline，政策是本地化的，政策代码的规模较小。因此，安全审核可以关注本地化的策略规范，而不必查看整个代码库。我们还证明了Jacqueline有合理的，通常可以忽略不计的开销。对于一个案例，Jacqueline实现比使用手动编码策略的实现更好。
总之，我们做出以下贡献：
bull;政策不可知的Web编程。我们提出了一种方法，允许程序员将信息流策略从其余的Web程序中分解出来，并依靠Web框架动态地执行这些策略。
bull;分面数据库。我们提出了分面数据库来支持策略无关的关系数据库查询。我们提出了一种分面对象关系映射（FORM）策略，用于使用现有的关系数据库实现。
bull;面向数据库支持的应用程序的分面执行。我们展示了分面数据库与分面应用程序运行时的互操作，方法是为lambda;JDB核心语言提供动态语义，并证明终端不受干扰和符合策略。
bull;早期修剪优化。我们通过形式化优化来解决性能问题，证明它保持了策略遵从性，并证明它显著降低了管理费用。
bull;实际可行性论证。我们介绍了Jacqueline Web框架，并通过几个应用程序案例研究展示了其表现力和性能。我们与手工执行的策略进行了比较，结果表明，Jacqueline不仅减少了策略代码的行数，而且策略执行具有合理性。
我们的方法减少了程序员出错的机会，提供了强有力的形式保证，而且实际上是可行的。
2、介绍性示例
使用我们的策略不可知的Web框架，程序员只实现一次与数据模式相关联的每个信息流策略，而不是在代码库中重复执行。我们设计了Jacqueline，使它的编程与Django的编程尽可能相似。在Jacqueline中，应用程序运行时映射和对象关系映射动态地操作敏感值和策略，这样程序员就可以省略重复的检查。
考虑使用社交日历应用程序。假设Alice和Bob为Carol安排一个惊喜派对，下周二晚上7点在施洛斯·达格斯图尔。他们应该能够创建一个事件，使信息只对客人可见。卡罗尔应该看看她下周二晚上7点有什么活动，但不是派对。其他人可能会看到，在Schloss Dagstuhl有一个私人活动，但没有活动细节。
我们演示了如何使用Jacqueline实现这个例子，Jacqueline是我们基于Django [1]的新Web框架，它是一个模型-视图-控制器框架。在标准MVC框架中，模型描述数据，视图描述前端页面呈现，控制器实现其他功能。对象关系映射（ORM）支持统一的对象表示。在Jacqueline中，该模型还指定了信息流策略。分面对象关系映射（FORM）还支持敏感值和策略的统一表示。 Jacqueline与政策无关：除了政策之外，Jacqueline计划看起来像是一个无政策的Django计划。
程序员和框架之间的分工如下：程序员将信息流策略与数据模式中的字段、Jeeves库支持的Python子集中的代码关联起来，并且仅通过Jacqueline API访问数据库。框架跟踪应用程序和数据库之间的敏感值和策略，以生成符合策略的输出。在我们的攻击模型中，用户是不可信的，我们假设程序员不是恶意的。
我们打算用这个例子来解释策略不可知的Web编程的语义。我们将在后面的章节中讨论实现和优化问题。
2.1 Jacqueline的模式和政策
在Jacqueline的策略不可知编程模型中，程序员负责指定信息流策略，应用程序运行时和对象关系映射负责跟踪敏感值的流，以生成符合这些策略的输出。程序员将每个信息流策略指定一次，与模型中的数据模式相关联。我们在图2中显示了事件和事件来宾数据对象的示例模式。Jacqueline模式定义字段名、字段类型和可选策略。我们用字段名称、位置、时间和描述定义事件类。到第5行，这看起来像一个标准的Django模式定义。
图2 日历事件的Jacqueline模式部分
2.1.1秘密价值和公共价值
Jacqueline中的一个敏感值封装了一个秘密（高度机密性）视图，该视图仅对具有足够权限的观众和公众可用（低保密性）可供其他观众观看的视图。Jacqueline允许敏感值作为秘密值或公共值，具体取决于查看上下文（即用户查看页面）。
实际字段值是秘密视图，程序员必须另外定义计算公共视图的方法。在第9行中，我们定义了jacqueline_get_public_name方法，计算名称字段的公共视图。如果权限禁止查看者查看敏感名称字段，那么名称字段将在所有计算（包括数据库查询）中表现为“私有事件”。此函数将当前行对象（事件）作为参数，允许使用行字段计算公共值。Jacqueline ORM使用命名约定（即Jacqueline_get_public prefix）来查找计算公共视图的适当方法。
2.1.2规定政策
在Jacqueline中，程序员指定的信息流策略保护敏感值的流。在第21行中，我们实现了字段名称和位置的策略，如decorator的标签_所示。策略是一种方法，它采用两个参数，即当前行对象（事件）和与查看页面的用户相对应的查看器（ctxt）。我们的策略查询EventGUest表（第25行）以确定查看器是否与事件关联。
如果没有Jacqueline，程序员就需要实现一个等价的函数，并在使用位置值时调用它。使用Jacqueline，程序不再需要显式地执行这些策略检查，因为Jacqueline的ORM和应用程序运行时确保了策略的强制执行。Jacqueline通过对创建值时的事件值和输出时的系统状态执行此策略来处理可变状态。
2.2分面执行
Jacqueline使用增强的应用程序运行时来跟踪敏感值的秘密和公共视图以及敏感值的计算结果。一旦程序员将策略与敏感数据字段相关联，程序的其余部分可能与策略无关。我们在Jacqueline中使用与Django相同的方式调用create：
carolParty = Event. objects. create( name=”Carolrsquo;s surprise party”,location=”Schloss Dagstuhl”, ...)
为了管理策略，Jacqueline FORM为敏感字段创建分面值。对于名称字段，框架创建分面值lt;k ? 'Carolrsquo;s surprise party' : 'Private event'gt;，其中k是一个新的布尔标签，用于保护秘密实际字段值和从get_public_name方法计算的公共方面。运行时最终根据策略和查看器分配标签值。我们在第3节中描述了FORM如何在关系数据库中存储分面值。
运行时通过评估每个方面来评估分面值。评估“Alice event” str（alice.events）会产生由同一标签保护的结果分面值：
lt;k ? 'Alicersquo;s events: Carolrsquo;s surprise party': 'Alicersquo;s events: Private event 'gt;
活动的嘉宾将看到“卡罗尔的惊喜派对”作为爱丽丝活动列表的一部分，而其他人只会看到“私人活动”。分面执行通过所有派生值，条件和变量赋值传播标签，以防止间接和隐式流。
Jacqueline为数据库查询执行分面执行，防止间接流经过以下查询：
Event. objects. filter(location='Schloss Dagstuhl')
如果carolParty是数据库中唯一的事件，则过滤器查询的分面执行会产生一个分面列表lt;m？[car
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
