基于模拟执行的软件功能规约的安全性验证

软件安全是指软件需要避免由风险因素或条件所导致的事故或损失，它是软件可信的一个重要参考指标。在软件需求分析阶段为软件制定功能与安全方面的需求规约，并验证软件功能符合安全需求则有助于安全关键软件的开发。然而，形式化的功能规约的安全性验证方法（如证明等）在实际工程中不容易被使用，静态分析功能规约的安全性又常常缺乏严格性和准确性。本课题将研究模拟执行软件形式化规约以进行安全性验证的方法。为此，课题将在SOFL形式化规约语言基础上研究软件安全的定义、描述、验证机制，并建立集成软件功能及安全约束的需求规约；研究如何模拟执行软件的形式化规约，并灵活、严格地验证软件功能的安全性。对软件的形式化规约进行模拟执行并进行安全性验证在国内外属创新工作，我们力求从理论上有所突破，并期望研究成果被推广应用到实际项目中，从而使软件产业能更好地应用安全验证方法，使用户获得符合安全需求的软件。

软件安全（Software Safety）是软件可信的一个重要参考指标，它是指软件需要避免由于风险（Hazard）因素或者条件而导致的事故或损失，即软件不仅需要完成它所应该完成的任务，也需要避免在各种风险下可能存在的错误的、危险的行为。特别是在开发安全关键软件（Safety-Critical Software）过程中，工程人员在需要制定软件的功能需求规约，也常常需要分析软件的风险、可能的事故、安全性缺陷、对功能的安全约束等等。实践表明，制定软件安全方面的需求，并验证软件及其功能规约的安全性（即检查软件功能、行为是否满足安全需求），有助于安全关键软件的开发。. 课题主要研究软件及其功能规约中的安全性验证方法。主要研究内容包括：研究软件动态行为方面的安全性需求；研究如何利用形式化工程SOFL（Structured Object-Oriented Formal Language）语言为软件动态行为建模，并制定安全性约束，从而使软件需求规约既具有可读性、可理解性，也可以精确地描述系统行为及其安全需求；研究基于SOFL对软件功能规约进行安全性验证，即动态执行软件功能规约，发现规约中存在的安全性缺陷并予以修正；研究对具体软件进行安全性分析的技术和方法，包括程序指向分析、软件崩溃预测方法、自动化的程序调试断点生成方法等。. 课题主要取得如下研究成果：（1）我们提出一种混成的方法来检验SOFL规约的内部一致性。内部一致性是SOFL规约的一种重要属性。研究的主要思想如下：通过具体或抽象的值来检查一个规约中Process的可满足性，以及通过符号执行和推导技术来检查集成规约的内部一致性，即通过输入驱动规约执行，并使执行中所有过程的前置条件和后置条件均为真，产生并检查输出；（2）我们研究通过方面（Aspect）以描述及集成软件安全性质、适应软件演进的架构语言AspectBreeze。特别是，AspectBreeze利用图文法，保证编织安全方面前后软件架构在演进过程中的一致性；（3）我们提出通过挖掘软件功能场景以预测软件安全缺陷的方法。研究中，我们通过使用k中心点算法聚类函数、生成功能场景，使用C4.5模型预测场景中的软件安全缺陷；（4）我们提出对软件进行安全性分析的方法与技术，包括程序执行路径执行频率的分析技术、软件崩溃预测方法、自动化的程序调试断点生成方法等。