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.