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

SaTC：核心：小型：超属性软件模型检查技术

基本信息

批准号：
2100989
负责人：
Borzoo Bonakdarpour
金额：
$ 27.54万
依托单位：
Michigan State University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-08-16 至 2022-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2100989&HistoricalAwards=false
关键词：
SaTC CORE Small Techniques Software

项目摘要

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.

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

项目成果

期刊论文数量（5）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Gray-box monitoring of hyperproperties with an application to privacy

通过隐私应用对超属性进行灰盒监控

DOI：
10.1007/s10703-020-00358-w
发表时间：
2021
期刊：
Formal Methods in System Design
影响因子：
0.8
作者：
Stucki, Sandro;Sánchez, César;Schneider, Gerardo;Bonakdarpour, Borzoo
通讯作者：
Bonakdarpour, Borzoo

Model checking hyperproperties for Markov decision processes

马尔可夫决策过程的模型检查超属性

DOI：
10.1016/j.ic.2022.104978
发表时间：
2022
期刊：
Information and Computation
影响因子：
1
作者：
Dobe, Oyendrila;Ábrahám, Erika;Bartocci, Ezio;Bonakdarpour, Borzoo
通讯作者：
Bonakdarpour, Borzoo

Bounded Model Checking for Hyperproperties

DOI：
10.1007/978-3-030-72016-2_6
发表时间：
2021-03-01
期刊：
Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
0
作者：
Hsu TH;Sánchez C;Bonakdarpour B
通讯作者：
Bonakdarpour B

Controller Synthesis for Hyperproperties

DOI：
10.1109/csf49147.2020.00033
发表时间：
2020-01-01
期刊：
2020 IEEE 33RD COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2020)
影响因子：
0
作者：
Bonakdarpour, Borzoo;Finkbeiner, Bernd
通讯作者：
Finkbeiner, Bernd

Finite-Word Hyperlanguages

有限词超语言

DOI：
发表时间：
2021
期刊：
15th International Conference on Language and Automata Theory and Applications (LATA
影响因子：
0
作者：
Bonakdarpour, Borzoo;Sheinvald, Sarai
通讯作者：
Sheinvald, Sarai