CAREER: Automated Analysis of 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.