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

TWC：选项：小：安全策略的自动软件模型修复

• 批准号: 1318678
• 负责人: Sandeep Kulkarni
• 金额: $ 44.88万
• 依托单位: Michigan State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1318678&HistoricalAwards=false
• 关键词: TWC; Option; Small; Automatic; Software

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.

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