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

职业：使用非静态信息流策略构建安全应用程序

• 批准号: 1942851
• 负责人: Danfeng Zhang
• 金额: $ 51.39万
• 依托单位: Pennsylvania State Univ University Park
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2023-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1942851&HistoricalAwards=false
• 关键词: CAREER; Building; Secure; Applications; Non

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.

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

项目成果

SpecSafe: detecting cache side channels in a speculative world

• DOI: 10.1145/3485506
• 发表时间: 2021-10
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Robert Brotzman;Danfeng Zhang;M. Kandemir;Gang Tan

Towards a General-Purpose Dynamic Information Flow Policy

迈向通用动态信息流政策

• DOI: 10.1109/csf54842.2022.9919639
• 发表时间: 2022
• 期刊: IEEE 35th Computer Security Foundations Symposium (CSF
• 作者: Li, Peixuan;Zhang, Danfeng
• 通讯作者: Zhang, Danfeng