EAGER: Hyperproperty Abstraction for Information Flow Control

EAGER：信息流控制的超属性抽象

• 批准号: 1649894
• 负责人: David Naumann
• 金额: $ 10.48万
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1649894&HistoricalAwards=false
• 关键词: EAGER; Hyperproperty; Abstraction; Information; Flow

Due to increasing cyber-attacks, software developers and analysts need better tools. Among the most important tools are programs that analyse other programs to evaluate security and privacy requirements, to detect vulnerabilities, and in general to predict a program's potential behavior. The theory of computation says these analysis problems are impossible to solve in their general form. Effective analyses rely on approximations, that is, simplified models of program behavior, the theory of which is known as abstract interpretation. This theory is widely used as basis for the design of analysis algorithms. Most existing analyses are for so-called trace properties, which pertain to individual program executions. Security and privacy requirements like confidentiality are about the flow of information in programs, which pertains to correlations between multiple executions. This project uses methods of mathematical semantics and formal logic to develop theory and algorithms for information flow analysis. The theory of abstract interpretation is being extended beyond trace properties, to encompass so-called hyperproperties which involve correlations among multiple behaviors of a program. On this basis, new algorithms are being created and evaluated. The main impact of this project will be to enable researchers and commercial tool developers to implement more sophisticated, comprehensive, and effective analyses for information flow in software. This will lead to improved software quality and protection against attacks, and ultimately increased trustworthiness of cyberspace. The theory developed in this project will contribute to growing science of security which will improve cybersecurity education and workforce training.

由于网络攻击的增加，软件开发人员和分析人员需要更好的工具。其中最重要的工具是分析其他程序以评估安全和隐私需求、检测漏洞以及通常预测程序潜在行为的程序。计算理论说，这些分析问题不可能以一般形式解决。有效的分析依赖于近似，即程序行为的简化模型，其理论被称为抽象解释。这一理论被广泛用作分析算法设计的基础。大多数现有的分析都是针对所谓的跟踪属性的，它与单个程序的执行有关。安全和隐私需求（如机密性）与程序中的信息流有关，这与多次执行之间的相关性有关。本项目使用数学语义学和形式逻辑的方法来发展信息流分析的理论和算法。抽象解释理论正在扩展到超越跟踪属性，包括所谓的超属性，它涉及到程序的多个行为之间的相关性。在此基础上，新的算法正在被创建和评估。这个项目的主要影响将是使研究人员和商业工具开发人员能够为软件中的信息流实现更复杂、全面和有效的分析。这将提高软件质量和抵御攻击的能力，并最终提高网络空间的可信度。在这个项目中发展的理论将有助于发展安全科学，这将改善网络安全教育和劳动力培训。

项目成果

Assuming you know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies

假设您知道：表达流策略的关系注释的认知语义

• 发表时间: 2018
• 期刊: IEEE Computer Security Foundations Symposium
• 作者: Chudnov, Andrey;Naumann, David
• 通讯作者: Naumann, David

Hypercollecting semantics and its application to static analysis of information flow

超集合语义及其在信息流静态分析中的应用

• DOI: 10.1145/3093333.3009889
• 发表时间: 2017
• 期刊: ACM SIGPLAN Notices
• 作者: Assaf, Mounir;Naumann, David A.;Signoles, Julien;Totel, Éric;Tronel, Frédéric
• 通讯作者: Tronel, Frédéric

A Logical Analysis of Framing for Specifications with Pure Method Calls

纯方法调用规范框架的逻辑分析

• DOI: 10.1145/3174801
• 发表时间: 2018
• 期刊: ACM Transactions on Programming Languages and Systems
• 影响因子: 1.3
• 作者: Banerjee, Anindya;Naumann, David A.;Nikouei, Mohammad
• 通讯作者: Nikouei, Mohammad

Spartan Jester: end-to-end information flow control for hybrid Android applications

Spartan Jester：混合 Android 应用程序的端到端信息流控制

• 发表时间: 2017
• 期刊: IEEE Mobile Security Technologies (MoST
• 作者: Sexton, Julian;Chudnov, Andrey;Naumann, David A.
• 通讯作者: Naumann, David A.