基于模型检测的C语言安全信息流研究

论文摘要

计算机技术的飞速发展带来了很多网络安全上的问题,迫切需要发展信息安全技术。在信息安全中,信息流安全的检测无法用传统的安全方法实现,只能通过安全信息流特性的检测来实现。因此为了控制端到端访问的信息流,需要检测多层安全级系统中程序的访问是否满足安全信息流特性。现在大部分安全信息流的研究集中在对java字节码和汇编码上。当前安全信息流的检测分为两类:一类是基于类型的方法;另一类是基于语义的方法。就检验的结果而言,基于语义的方法要优于基于类型的方法。本文采用基于语义的方法在安全信息流的检测上进行了以下研究。1.将安全信息流的研究移植到新的领域中。研究中将安全信息流研究和模型检测方法相结合,对C语言程序安全信息流的信息保密性进行检测。研究按照建模——特性描述——检测的流程。本文分析了安全信息流中的信息保密性要求,研究了C语言的执行特征,根据这些使用抽象解释方法得出相应的C语言的具体语义然后进行抽象得到能够建模的抽象语义。在语义生成之后,对生成的语义和C语言的标准语义的一致性进行验证,给出引理并且证明了具体语义和抽象语义的正确性;从而证明了对C语言程序建模的正确性。同时分析信息保密性的要求和信息泄露的产生原因,得出对应这些信息保密性的CTL公式。2.根据C语言信息保密性的研究,深入剖析满足信息保密性的状态图的路径特征和状态特征;分析状态中变量对安全特性的影响。对状态数据结构进行优化,减少状态数据结构中的变量;对C语言的if和while语句的语义进行优化,减少建模后状态图的状态数目的同时合并无意义的分支和循环,生成线性序列的状态图。最后将这种优化应用到对信息保密性的研究中去。按基于语义方法得出对应的抽象语义,对应着线性状态图特征信息保密性的分析并生成信息保密性的LTL公式。3.对C语言安全信息流分析研究进行实现,并且以实例来分析比较1,2中使用的方法。通过实例结果说明改进方法优于未改进的方法。

论文目录

• 摘要
• Abstract
• 第1章 引言
• 1.1 研究背景
• 1.2 国内外研究现状
• 1.2.1 安全信息流研究及分类
• 1.2.2 基于类型方法的研究
• 1.2.3 基于语义方法的研究
• 1.2.4 安全信息流研究和模型检测的结合
• 1.2.5 两种方法的比较
• 1.3 研究内容简介
• 1.4 小结
• 第2章 基础知识
• 2.1 模型检测
• 2.2 时序逻辑
• 2.2.1 线性时序逻辑LTL
• 2.2.2 计算树时序逻辑CTL
• 2.3 抽象解释
• 2.4 小结
• 第3章 C 语言信息保密性研究
• 3.1 C 语言信息保密性
• 3.2 多层安全级系统的格模型
• 3.3 C 语言和标准语义
• 3.4 C 语言具体收集语义
• 3.5 C 语言抽象语义
• 3.6 语义一致性和抽象转换系统描述
• 3.7 安全性分析和CTL 公式
• 3.7.1 信息保密特性分析
• 3.7.2 信息保密性CTL 公式表示
• 3.8 小结
• 第4章 优化方法研究C 语言信息完整性
• 4.1 优化方法和信息完整性研究
• 4.1.1 可优化部分
• 4.1.2 信息完整性研究
• 4.2 优化方法中的C 语言语义
• 4.2.1 标准语义
• 4.2.2 具体收集语义
• 4.2.3 改进的抽象语义
• 4.3 信息完整性分析和LTL 公式
• 4.3.1 信息完整性分析
• 4.3.2 信息完整性LTL 公式表达
• 4.4 小结
• 第5章 系统实现和性能比较
• 5.1 系统实现
• 5.1.1 基本框架
• 5.1.2 数据结构和模块函数
• 5.2 实验结果和性能比较
• 5.3 小结
• 第6章 结论和展望
• 6.1 结论
• 6.2 展望
• 参考文献
• 致谢
• 个人简历、在学期间发表的学术论文与研究成果