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