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）一个错误诊断模块，当程序违反指定的非静态策略时，它提供有用的反馈。这项研究还将开发并开源一个集成了这三个新颖组件的新工具链，使得使用非静态信息流策略指定、验证和调试实际应用程序变得可行。该奖项反映了 NSF 的法定使命，并被认为是值得的。通过使用基金会的智力优势和更广泛的影响审查标准进行评估来提供支持。

项目成果

Towards a General-Purpose Dynamic Information Flow Policy

迈向通用动态信息流政策

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

SpecSafe: detecting cache side channels in a speculative world

SpecSafe：在推测世界中检测缓存侧通道

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