SaTC: CORE: Small: Techniques for Software Model Checking of Hyperproperties

点击翻译按钮获取中文摘要

Most manufacturers and companies employ a set of security and privacy policies that specify how the data produced by their products can be accessed and propagated. Violation of such policies may result in catastrophic consequences such as breach of public services and safety or compromising highly sensitive data and privacy of citizens. Frequent reports of security exploits and loss of information privacy have unfortunately become everyday occurrences. In the context of confidentiality, one specific technique to obtain assurance is analyzing software source code to identify security flaws, in particular, to detect bad flow of information among users with different security privileges. This project aims at developing algorithms and tools that automatically detect bugs that result in violation of confidentiality through bad flow of information. The results of this project will improve public confidence in the ability of complex systems to operate safely and maintain information confidentiality. The research aims to bring about a paradigm shift in reasoning about security and privacy at software source code level.This project develops push-button software model checking techniques for verification of a rich class of information flow policies. The specification language is based on hyperproperties, a set-theoretic framework to describe security and privacy policies. The project uses HyperLTL, a temporal logic that allows explicit quantification over traces, to formally express hyperproperties. The main objective is to make software model checking possible for hyperproperties. The investigators investigate new theories that allows code-level verification of hyperproperties, as the current semantics of HyperLTL does not allow asynchronous progress among traces. The project develops efficient model checking techniques that cannot be trivially generalized to deal with HyperLTL: partial-order reduction, abstraction/refinement, and bounded model checking. The investigators develop tools that realize these algorithms and will conduct rigorous case studies.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.