软件可信验证自动化技术研究

摘要

缺陷和漏洞广泛存在于各种软件中，难以避免，由其引发的故障很容易给生命财产带来损害，甚至灾难性后果。应对这一问题的有效途径是设计有效合理的自动化的测试方法对软件系统可信度进行充分全面的验证。本论文对软件可信安全性验证研究从静态验证和动态检测两个角度分别着手。
　　首先从静态检测角度，针对安全苛刻性编程标准，提出基于规则匹配的代码静态检测方法。构建易于表述及存储源码信息的源码表示模型，解决C++语言的灵活性和复杂性导致的难以对代码直接进行规则匹配的问题;设计解析树模型和存储转换模型，完成从源代码提取与规则有关的信息翻译为中间表示文件的源码解析过程;设计包含编程安全标准中全部有效规则的规则库模型用于对中间表示文件进行规则匹配和缺陷反馈;通过系统实现和实验验证方法的有效性。
　　然后从动态检测角度，提出一种基于非确定性FSM模型的测试生成和测试验证方法。针对复杂软件系统状态行为转换不确定的问题，提出层次化建模方法，对不确定的状态转移进行聚类和分层建模，将其转化为分层子状态机间确定唯一的状态转移，解决软件设计规格不确定行为难以描述和生成测试用例的问题;提出从正则式模型产生测试集的方法，根据状态机与正则表达式的等价关系，构建状态机模型对应的的正则式模型，给出迁移覆盖算法从正则式模型生成测试集，解决软件系统控制流程中循环部分在用例中难以精确描述的问题;在正则式模型中加入不同触发参数作为用例特征，划分出不同特征的测试集，提高用例的验证能力和测试充分性。
　　静态手段可以在软件开发早期发现程序中的潜在缺陷，及时止损，减少开发中后期的故障率，以较少的成本提高软件可靠性;作为静态手段的补充，动态检测从系统级全局角度发现软件系统的符合性错误、运行时故障、以及静态验证阶段未发现的缺陷，在开发中后期为其可信度和健壮性验证提供进一步有力支持。

目录

声明

摘要

1 绪论

1．1 研究背景和意义

1．2 软件可信验证概述

1．3 相关现状研究

1．4 相关技术综述

1．4．1 静态检测技术

1．4．2 基于FSM的动态测试生成技术

1．5 论文的主要工作

1．6 论文的组织结构

2 基于规则匹配的代码静态分析方法设计

2．1 XML概述

2．2 源码表示模型

2．2．1 文件信息的XML模型构建

2．2．2 语句单元的XML模型构建

2．2．3 标识符单元的XML模型构建

2．2．4 表达式单元的XML模型构建

2．3 源码解析方法

2．3．1 关系型解析树模型

2．3．2 存储模型

2．4 规则匹配方法

2．5 本章小结

3 静态分析系统设计和验证

3．1 开发工具LEX与YACC

3．2 系统总体框架

3．3 实验分析

4 基于非确定性状态机模型的动态测试方法设计

4．1 状态机层次化建模

4．2 正则表达式概述

4．3 状态机到正则表达式的转化

4．4 正则表达式语法规则定义

4．5 正则表达式迁移覆盖算法

4．5．1 低耦合模块的闭包解析算法

4．5．2 高耦合模块的闭包解析算法

4．5．3 综合完备的闭包解析算法

4．5．4 层次状态机的迁移覆盖测试生成

4．5．5 去括号算法

4．6 正则式用例生成与划分

4．6．1 正则式用例动态参数

4．6．2 正则式用例相似度

4．6．3 正则式用例分组

4．7 本章小结

5 动态测试系统设计和验证

5．1 系统框架

5．2 实验分析和小结

结论

参考文献

攻读硕士学位期间发表学术论文情况

致谢