复杂需求场景驱动的软件安全防护模型检测技术研究

Safety is the most important property for high dependable systems,such as in aerospace, transportation and nuclear energy areas, whose actual operational scenarios is very complex, in order to ensure the whole system's safety, some methods and technologies should be adopted for system's safety analysis and design. Conventional methods for safety analysis and assurance technology have problems in terms of correctness and efficiency. It is prone to make errors because the result of safety analysis and software design are come from natural language, and the manual work is very labor intensive and time consuming. Model checking is an effective way to verify and analyze whether behaviors of the system meet its properties. Using Model checking methods and fault injection techniques can improve consistency and correctness for safety process throughout the system's safety lifecycle. Yet existed methods for fault injection and model checking mainly think about single faults injection and qualitative safety analysis, seldom do with fault injection for multiple faults and quantitative safety analysis, so the procedure for safety analysis and the result for safety verification is inadequate. It is difficult to build formal model according to system requirement specification, and the problems for state space explosion in model checking is prone to happen. In our subject, we research model checking methods on safety analysis and automatic formal design model generation for safety critical system,whose safety features and actual operational scenarios system are considered, by definition of a unified semantic framework and consistent analysis for system requirement scenarios, a method for automatic generating formal system model from requirement scenarios is provided, in order to analyze the safety property for safety critical system, we propose suitable model checking algorithm, and provide corresponding fault injection-based model checking methods according to different type of fault failure mode, then automatically form the minimal cut sets of fault trees and get formal safety requirements, finally, according to safety requirements, modification and refinement is adopted for system requirement scenarios step by step, the formal design model is formed and consistent with the safety requirements, it can be used for safety design model of safety criticial system. some relevant supporting software tools for proposed model checking and fault injection algorithms are developmented, and dynamic simulation for formal safety design model is provided. Through the studies in the project, some theoretical and methodological guidance is offered for the technologies on safety assurance, such as safety analysis and assessment of safety critical system, the improvement for system dependability, automatic safety requirements acquisition and formal safety design model generation, which can enrich the method for model-based system formal development.

在航空航天、交通运输等高可信系统领域，系统的实际运营场景非常复杂，其安全性至关重要，如何对系统进行安全防护并确保其运营安全日益成为关注焦点。传统的安全性分析方法与安全保障技术都不能从根本上确保系统安全，模型检测是验证和分析系统行为属性的有效途径，但目前的模型检测技术存在形式化建模难、安全性分析不充分、状态空间爆炸、通用性与实用性不强等问题。本课题根据安全苛求系统的安全性特点与复杂需求场景，研究统一语义框架下的系统形式化模型自动生成方法，提出适合于系统安全性分析的通用模型检测算法，并针对不同的故障模式，提出相应的故障注入算法与系统安全性分析方法，自动获得形式化安全需求与软件安全性设计的形式化模型，并研制相应的支撑工具软件。本课题的研究为安全苛求系统的安全防护、安全性分析与评估、系统可信性的提高、安全需求与软件设计模型的获取提供理论指导与技术支撑，丰富了基于模型的高可信软件形式化开发方法。

以高可信系统的安全性分析与验证为研究对象，研究模型检测方法及相应算法、系统的安全性保障方法与高可信性性能的提高，在交通运输、航空航天、网络信息系统安全等领域具有重要的实际意义和应用价值，取得如下主要成果：.1、对基于迁移的广义Büchi自动机模型进行扩展，提出了基于启发式on-the-fly的扩展TGBA模型检测算法，其通用性更强，判空检测的有效性更优，在通常情况下，时空性能均较优，为安全苛求系统的安全性验证提供了切实可行的解决途径。.2、为了解决形式化验证中存在的形式化建模难的问题，并考虑到复杂多变的实际运营场景，提出基于多场景分析的系统形式化建模方法。.3、提出基于多故障的模型检测安全性分析流程和基于多故障注入的模型检测算法，使系统的安全性分析更全面。.4、研究了高层次时序电路的可靠性评估方法，提出了触发器可靠度计算的F-PTM 方法、基于差错概率传播模型的门级电路可靠度计算方法，有利于安全苛求系统中的电路结构设计、芯片的关键制造工艺的优化，电路开发费用和生产成本的降低。.5、研究无人机飞行领域中存在的路径不确定性问题与系统性能影响，提出一种基于概率模型检测的无人机路径优化建模方法，减少了操作员的工作量，提高了无人机的工作效率与安全性，为无人机飞行安全模型的建立提供有效途径。.6、提出一种基于概率模型检测的工作站集群故障修复方法，能大幅度减少维修过程所需时间，提高了维修效率和系统的容错性，为提升高可信工作站集群的系统性能提供了新思路。.7、物联网通常是一个集计算、通信和控制于一体的智能子系统。提出基于时间自动机的物联网组合服务建模方法，具有较好的实用性。.8、研究系统在网络空间环境下的安全防护方法，提出基于攻击路径和PCA算法的报警关联方法、面向IaaS云平台的用户异常行为检测方法、基于DTW距离度量函数的DTW-TA轨迹匿名算法、k-匿名改进模型下的LCSS-TA轨迹匿名算法、基于节点分割的权重序列隐私保护研究等方法，为网络信息系统的安全保障提供有效途径。