Increasing cyber security depends on our ability to guarantee that the system will provide the expected functionality under normal circumstances as well as if the system is perturbed by some random events or security threats. Providing such guarantee is often complicated due to several factors such as changes in system requirements caused by user demands, exposure to a new threat model that was not considered (or not relevant) in the original design, or identifying bugs or vulnerabilities during a system life cycle. The purpose of the project is to develop automated techniques --that provide justifiable confidence about correctness-- to transform an existing software model into a new model that satisfies both the existing functionality and the desired security requirements.
Developing algorithms that generate models that satisfy existing functionality and new security requirements poses new challenges due to the fact that existing trace-based properties do not suffice for several security properties. A characteristic of trace-based properties is that if a model satisfies a trace-based property and it is restricted by removing some undesired behaviors then the revised model still satisfies that trace-based property. Hence, adding a trace-based property can be achieved by removing behaviors that violate it. Since trace-based properties cannot express several security properties, this project will utilize a new formalism, hyperproperties, that generalizes trace-based properties and can be used for modeling security requirements. In particular, a hyperproperty consists of a set of trace-based properties and to satisfy that hyperproperty it is required that the repaired program exhibit `all? behaviors in one of these properties.
To develop algorithms that justifiably provide assurance about models developed by them, this project will first focus on formalizing commonly used security requirements using hyperproperties. It will perform complexity analysis to evaluate the complexity of adding different security properties to an existing model. To mitigate cases where the complexity is high, it will develop heuristics and algorithms that (1) identify whether adding the given hyperproperty can be achieved via adding a related stronger trace-based property, and (2) identify a subset of hyperproperties where adding the given property is more efficient. This work will also result in the development of efficient algorithms and tools that utilize the complexity bottlenecks. Thus, the results of the proposed project will enhance assurance of software systems by repairing security flaws and vulnerabilities in an automated fashion.
