TWC: Option: Small: Automatic Software Model Repair for Security Policies

提高网络安全性取决于我们保证系统在正常情况下以及系统受到一些随机事件或安全威胁干扰时提供预期功能的能力。由于以下几个因素，提供这样的保证通常是复杂的，例如由用户需求引起的系统需求的变化，暴露于原始设计中未考虑（或不相关）的新威胁模型，或者在系统生命周期中识别错误或漏洞。该项目的目的是开发自动化技术——提供关于正确性的合理信心——将现有的软件模型转换为既满足现有功能又满足期望的安全性需求的新模型。开发生成满足现有功能和新安全需求的模型的算法带来了新的挑战，因为现有的基于跟踪的属性不能满足几个安全属性。基于跟踪的属性的一个特征是，如果一个模型满足基于跟踪的属性，并且通过删除一些不希望的行为来限制它，那么修改后的模型仍然满足基于跟踪的属性。因此，添加基于跟踪的属性可以通过删除违反该属性的行为来实现。由于基于跟踪的属性不能表示多个安全属性，因此该项目将利用一种新的形式化方法，即超属性，它概括了基于跟踪的属性，并可用于对安全需求进行建模。特别地，一个超属性由一组基于跟踪的属性组成，为了满足这个超属性，修复后的程序需要显示“all?”这些属性中的行为。为了开发合理地为它们开发的模型提供保证的算法，本项目将首先关注使用超属性形式化常用的安全需求。它将执行复杂性分析，以评估向现有模型添加不同安全属性的复杂性。为了减轻复杂性高的情况，它将开发启发式算法(1)确定是否可以通过添加相关的更强的基于跟踪的属性来添加给定的超属性，以及(2)确定添加给定属性更有效的超属性子集。这项工作还将导致开发利用复杂性瓶颈的高效算法和工具。因此，建议的项目的结果将通过以自动化的方式修复安全缺陷和漏洞来增强软件系统的保证。

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.