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

大多数制造商和公司都采用一套安全和隐私策略，指定如何访问和传播其产品产生的数据。违反这些政策可能导致灾难性后果，例如破坏公共服务和安全或损害高度敏感的数据和公民隐私。不幸的是，安全漏洞和信息隐私丢失的频繁报告已成为日常事件。在保密性方面，获得保证的一种具体技术是分析软件源代码以识别安全缺陷，特别是检测具有不同安全权限的用户之间的不良信息流。该项目旨在开发自动检测错误的算法和工具，这些错误通过不良信息流导致违反保密性。该项目的成果将提高公众对复杂系统安全运行和维护信息保密能力的信心。该研究旨在为软件源代码级别的安全和隐私推理带来范式转变。该项目开发了按钮式软件模型检查技术，用于验证丰富的信息流策略。规范语言是基于hyperproperties，一套理论框架来描述安全和隐私政策。该项目使用HyperLTL，一种允许在痕迹上显式量化的时态逻辑，以正式表达超属性。主要目标是使软件模型检查可能的hyperproperties。研究人员研究了允许代码级验证hyperproperties的新理论，因为HyperLTL的当前语义不允许跟踪之间的异步进展。该项目开发了有效的模型检查技术，不能简单地推广到处理HyperLTL：部分降阶，抽象/细化和有界模型检查。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.