CAREER: Building Secure Applications with Non-Static Information Flow Policies

计算机系统中的许多安全问题可以从信息流的角度来理解：私有和不受信任的数据以及从它们派生的数据永远不应该流向计算机系统中的非预期通道。在现实世界的系统中，这种安全顾虑通常会随着时间的推移而变化。例如，允许支付系统在交易期间使用信用卡详细信息，但在交易完成后不应保留任何信用卡详细信息记录。安全问题的动态特性使得使用非静态信息流策略构建、验证和调试应用程序变得具有挑战性。因此，许多安全敏感应用的信息流策略目前要么根本没有指定，要么被以特别的方式处理，导致实际应用中存在大量的可信计算基础和许多安全漏洞。该奖项调查了一项旨在改变程序员理解、指定、验证和调试非静态信息流策略的方式的综合研究和教育计划。它包含三个组件来解决使用非静态策略构建安全应用程序的关键障碍：(1)依赖策略提供了一个简单、声明和统一的非静态策略视图，包括动态策略、降级策略和擦除策略，这些策略目前都是形式化的，并使用未连接的语义目标进行检查；(2)Const，用于分析应用程序中的非静态策略的约束语言；(3)错误诊断模块，当程序违反指定的非静态策略时，它提供有用的反馈。这项研究还将开发和开源一个集成了三个新组件的新工具链，使指定、验证和调试具有非静态信息流策略的真实应用程序成为可能。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Many security concerns in computer systems can be understood in terms of information flows: private and untrusted data, as well as data derived from them, should never flow to unintended channels in a computer system. In real-world systems, such security concerns typically change over time. For example, a payment system is allowed to use credit card details during a transaction, but it should not retain any record of credit card details once the transaction is complete. The dynamic nature of security concerns makes it challenging to build, verify and debug applications with non-static information flow policies. Consequently, the information flow policies of many security-sensitive applications are currently either unspecified at all, or being treated in an ad-hoc manner, resulting in large trusted computing bases and many security bugs in real applications. This award investigates an integrated research and education plan designed to transform the way that programmers understand, specify, verify and debug non-static information flow policies. It contains three components to address the key obstacles of building secure applications with non-static policy: (1) Dependent policy gives a simple, declarative and unified view of non-static policies, including dynamic policy, downgrading policy and erasure policy that are currently formalized and checked with unconnected semantic goals, (2) CONST, a constraint language for analyzing non-static policies in applications, and (3) An error diagnosis module that provides useful feedbacks when a program violates the specified non-static policy. This research will also develop and open-source a new toolchain that integrates the three novel components, making it feasible to specify, verify and debug real applications with non-static information flow policy.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.