CAREER: Automated Analysis of Security Hyperproperties

职业：安全超属性的自动分析

• 批准号: 1553548
• 负责人: Rohit Chadha
• 金额: $ 43.6万
• 依托单位: University of Missouri-Columbia
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-07-01 至 2023-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1553548&HistoricalAwards=false
• 关键词: CAREER; Automated; Analysis; Security; Hyperproperties

Computer programs and cryptographic protocols are increasingly being used to access confidential and private information on the Internet. Due to their complex nature, they often have subtle errors that can be exploited by malicious entities. As security flaws can have serious consequences, it is important to ensure that computer programs and cryptographic protocols achieve their security objectives. As such systems have a large (potentially infinite) number of states due to presence of malicious adversaries and the concurrent nature of Internet, `pen and paper' reasoning about their correctness is challenging. In addition to the state explosion, reasoning about correctness is also challenging within the context of security because standard security objectives such as confidentiality and privacy turn out to be hyperproperties. The challenge lies in the fact that when reasoning about hyperproperties, one has to reason about correctness of the set of all executions of a system as a whole instead of correctness of individual executions. Therefore, the development of techniques to automate this reasoning is of vital importance, and is the research focus of this project. Formally, hyperproperties generalize properties that are used to express safety and liveness guarantees in classical automated verification. A property is a set of allowable executions. A system violates a property if it exhibits an execution that is not allowed. In contrast, security objectives such as confidentiality, non-interference, privacy, and anonymity are hyperproperties. A hyperproperty is a collection of allowable sets of executions. A system violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. Current state-of-the art automated tools for verifying security guarantees do not scale very well as they are often aimed at certain security guarantees and often make restrictive assumptions on the systems. This project aims to develop new scalable state-of-the-art techniques in automated verification of hyperproperties by undertaking primarily three research tasks. First, we will develop and implement new symbolic algorithms for verifying finite-state systems against an expressive set of hyperproperties. The second task shall be devoted to scaling the analysis by a novel combination of automated analysis and automated counterexample generation designed specifically for hyperproperties. Finally, we shall establish theoretical results that shall reduce the problem of verifying cryptographic protocols in the presence of unbounded message sizes and nonces to the finite case. The research aims of the proposal will be paired with curriculum development at the University of Missouri where a new concentration in security will be introduced in the undergraduate curriculum that will integrate security design with software development. The results of this project will be integrated in the courses, and the project will support both undergraduate and graduate student research.

计算机程序和加密协议越来越多地被用于访问互联网上的机密和私人信息。由于其复杂的性质，它们通常具有可被恶意实体利用的细微错误。由于安全漏洞可能会产生严重后果，因此确保计算机程序和加密协议实现其安全目标非常重要。由于存在恶意对手和互联网的并发性，这种系统具有大量（可能是无限的）状态，因此关于其正确性的“笔和纸”推理具有挑战性。除了状态爆炸之外，在安全环境中对正确性的推理也是一个挑战，因为标准的安全目标，如机密性和隐私性，都是超属性。 挑战在于这样一个事实，即当推理超属性时，人们必须推理整个系统的所有执行的集合的正确性，而不是单个执行的正确性。因此，开发自动化推理的技术是至关重要的，也是本项目的研究重点。形式上，超属性概括了经典自动验证中用于表达安全性和活性保证的属性。属性是一组允许的执行。如果一个系统展示了一个不被允许的执行，它就违反了一个属性。相比之下，保密性、不干涉、隐私和匿名等安全目标是超属性。超属性是允许的执行集的集合。如果系统的执行集不在超属性指定的集合中，则系统违反了超属性。目前用于验证安全保证的最先进的自动化工具不能很好地扩展，因为它们通常针对某些安全保证，并且通常对系统进行限制性假设。该项目旨在通过主要开展三项研究任务，开发新的可扩展的最先进技术，用于自动验证超属性。首先，我们将开发和实现新的符号算法来验证有限状态系统对一组表达的超属性。第二个任务将致力于通过自动分析和自动反例生成的新组合来扩展分析，该分析是专为超性质设计的。最后，我们将建立理论上的结果，应减少的问题，验证密码协议的存在下，无限的消息大小和随机数的有限情况下。 该提案的研究目标将与密苏里州大学的课程开发相结合，在该大学，将在本科课程中引入新的安全集中，将安全设计与软件开发相结合。 该项目的结果将被整合到课程中，该项目将支持本科生和研究生的研究。

项目成果

Modelchecking Safety Properties in Randomized Security Protocols. In: Nigam V. et al. (eds) Logic, Language, and Security.

随机安全协议中的模型检查安全属性。

• DOI: 10.1007/978-3-030-62077-6_12
• 发表时间: 2020
• 期刊: and Security (Lecture Notes in Computer Science
• 作者: Matt S. Bauer, Rohit Chadha

On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs

• DOI: 10.1109/lics52264.2021.9470708
• 发表时间: 2021-04
• 期刊: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• 作者: Rohit Chadha;A. Sistla;Mahesh Viswanathan

Strongly bounded termination with applications to security and hardware synthesis

强有界终止与安全和硬件综合应用

• DOI: 10.1145/3406089.3409029
• 发表时间: 2020
• 期刊: Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development
• 作者: Reynolds, Thomas;Harrison, William L.;Chadha, Rohit;Allwein, Gerard
• 通讯作者: Allwein, Gerard

Deciding accuracy of differential privacy schemes

• DOI: 10.1145/3434289
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: G. Barthe;Rohit Chadha;Paul Krogmeier;A. Sistla;Mahesh Viswanathan

Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

• DOI: 10.1145/3343508
• 发表时间: 2019-10
• 期刊: ACM Transactions on Computational Logic (TOCL)
• 作者: G. Bana;Rohit Chadha