基于多形态时钟输入输出迁移系统的安全软件测试研究

发布时间：2018-05-29 06:09

本文选题：多形态时钟 + 标号迁移系统　；参考：《华东师范大学》2017年博士论文

【摘要】：缺乏系统的科学的测试体系是一直以来影响安全软件测试可信度的根本问题。在现有的工程实践中,测试是实验性行为的认知和实施方案普遍存在,威胁着系统的安全性并且这一问题随着安全软件需求量的激增,职责范围的外延,规模的扩大和复杂度的提高变得越来越严重。因此,构造高效可信的安全测试方法和工具已经成为安全软件行业不可回避的挑战。本文以构建安全软件的安全性测试理论框架及其应用为主要研究目标,针对安全软件苛求质量的实际需求,以形式化测试为基础,根据安全软件的典型特征,从设计符合其特点的建模语言开始,构建了统一安全性验证和安全性测试的理论框架。该理论框架立足于研发安全软件的全流程而非纯粹测试的立场,在保证测试方法本身正确性的同时,设计了通过测试也可以证明软件实现是安全的理论框架和相应的测试序列生成方法,主要贡献体现在:1.定义了多形态时钟时间模型,设计了多形态时钟输入输出迁移系统,给出了相应语法和语义的形式化定义,提出了将时间模型从系统行为模型中分离出来的安全软件建模方法;2.提出了统一的安全性验证与测试序列生成理论框架。该理论框架站在安全软件全流程而非单一测试的角度,将对规约设计的安全性验证与软件实现的安全性测试融合在同一个理论框架中,证明了如果某个实现通过了基于满足安全性属性模型所生成的测试序列集合,那么该实现也满足期望的安全性属性的结论,并给出了相应的测试序列生成方法;3.构建了多形态时钟输入输出迁移系统的安全性测试方法,定义了多形态时钟输入输出一致性关系,设计了相应的符号测试方法。并在此基础上,为了满足安全软件防护能力测试的需求,进一步提出了采用规约变异的测试方法计算安全软件的故障测试序列集合,定义了基于安全故障模型的变异算子,给出了基于弱变异思想的诱导规则,设计了k周期诱导算法。为了展示方法的可行性,本文以某实际车载列车自动防护软件系统为例说明了基于多形态时钟输入输出迁移系统的安全测试理论在安全软件系统中的具体应用。
[Abstract]:The lack of systematic and scientific testing system is the fundamental problem that affects the reliability of security software testing. In existing engineering practice, testing is a widespread cognitive and implementation scheme of experimental behavior, threatening the security of the system and increasing the demand for security software and the extension of the scope of responsibility. The enlargement of scale and the increase of complexity become more and more serious. Therefore, the construction of efficient and credible security testing methods and tools has become an unavoidable challenge in the security software industry. The main research goal of this paper is to construct the security testing theory framework and its application of security software, aiming at the practical requirement of demanding quality of security software, based on formal testing, according to the typical characteristics of security software. Starting with the design of modeling language which conforms to its characteristics, the theoretical framework of unified security verification and security testing is constructed. The theoretical framework is based on the position of developing the whole process of security software rather than pure testing, while ensuring the correctness of the test method itself. It can also be proved by testing that the software implementation is a safe theoretical framework and a corresponding test sequence generation method. The main contribution is reflected in: 1. The multi-morphological clock time model is defined, the multi-morphological clock input / output migration system is designed, the formal definitions of syntax and semantics are given, and the security software modeling method is proposed, which separates the time model from the system behavior model. A unified theoretical framework for security verification and test sequence generation is proposed. The theoretical framework is based on the whole process of security software rather than a single test, and combines the security verification of protocol design and the security test of software implementation in the same theoretical framework. It is proved that if an implementation passes the set of test sequences generated based on the satisfied security attribute model, then the implementation also satisfies the expected security attribute, and the corresponding test sequence generation method is given. The security test method of multi-morphological clock input / output migration system is constructed. The consistency relationship of multi-morphological clock input and output is defined and the corresponding symbol testing method is designed. On this basis, in order to meet the requirements of security software protection capability testing, a test method of protocol mutation is proposed to calculate the fault test sequence set of security software, and a mutation operator based on security fault model is defined. The induction rule based on weak mutation is given, and the k-period induction algorithm is designed. In order to demonstrate the feasibility of the method, this paper illustrates the application of the security test theory based on the multi-form clock input and output migration system in the security software system, taking an actual on-board train automatic protection software system as an example.
【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2017
【分类号】：TP311.53

【相似文献】