EAGER: Hyperproperty Abstraction for Information Flow Control

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

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.