隐通道可计算性的研究

论文摘要

作为一项重要的评估指标,美国国防部的TCSEC准则和ISO的CC标准都对隐通道做出了明确地规定,即软件要获得B2或EAL5及以上级的安全认证,必须要通过不同强度的隐通道分析。隐通道分析由三部分工作组成:搜索、审计和消除。在经历了二十世纪八、九十年代的繁荣期后,近些年隐通道的研究进展趋缓。造成这种现象的一个重要原因是基础研究与应用研究脱节,由于一直没有完整的形式化描述体系作为理论基础、以及相应的数学工具作为研究手段,隐通道应用领域中的研究工作自然难以快速发展。给出隐通道的形式化定义,建立适用于隐通道计算的数学工具,并以此为基础推导隐通道的性质、研究隐通道分析中的各项工作,是本文的主要内容,也是隐通道基础研究的重要组成部分。本文的主要工作可以概括为两大部分:（1）隐通道可计算性的研究;（2）在隐通道可计算性研究基础上展开的应用研究。首先,本文通过研究可信系统的相关要素,分析隐通道的工作机理,给出了隐通道的一种形式化定义,并据此推导出了隐通道的一般属性、可计算属性、以及存在的最小条件等性质;进一步地,通过在隐通道集合的内部引入二元运算关系,建立了一个代数系统。根据隐通道空间拓扑结构的变化,通过使用这个代数系统,能够直接计算出可计算属性值的相应变化。其次,针对在实践中观察到的TCSEC准则关于隐通道审计标准的不足,通过综合使用带宽、势差、工作时间、敏感参数等多项可计算指标,研制了一个新的审计标准α-IA。新标准在兼容TCSEC相关标准的同时,能够根据用户的具体需求从不同角度去刻画隐通道的威胁。进一步地,在隐通道代数系统的基础上,我们对新审计标准的计算方法作了详细讨论。再次,根据在可计算性研究中已经证明出的隐通道存在的最小条件,对已知的静态隐通道搜索和消除方法进行了分类研究,总结了每种方法的基本思想和简要操作步骤,并讨论了它们各自的优点与不足。进一步地,针对静态方法的不足,提出了非静态的隐通道搜索和消除方法。与基于系统项级描述或源代码分析的静态方法不同,这类新方法要求在系统的运行状态下实行,现阶段它们既可以独立地使用,也可以作为静态方法的补充。一般地,非静态方法的总体成本低于相应的静态方法。搜索是隐通道审计和消除的工作依据,鉴于搜索环节的重要性,文中还对通用的全自动隐通道搜索问题进行了研究,并证明了这是一个不可判定问题,即不存在一个算法能在有限的时间里搜索出任意程序中含有的任何隐通道。这告诉我们不可能依赖单个程序,一劳永逸地解决所有的隐通道搜索问题。最后,根据在可计算性研究中建立的隐通道形式化定义,模拟隐通道的工作机理,开发了一个隐通道的仿真系统。通过设计使用不同的通信协议,比较全面地对隐通道进行了仿真,测试了隐通道的带宽、抗干扰等项指标。通过仿真试验还观察到了一些在静态分析中观察不到的隐通道性质,文中对这些性质的成因做了分析。在文章结尾处,我们提出隐通道的语义分析是未来隐通道研究的重要方向。本文的主要创新点是:（1）给出了隐通道的形式化定义,并在此基础上推导了隐通道的性质,建立了一个用于隐通道计算的代数系统。这为隐通道的形式化研究提供了理论基础和数学工具。早期的隐通道研究,多是依据实际问题提出特定的隐通道处理方法,因此这些方法看起来是彼此孤立的、且缺乏必要的理论基础。在这种情况下,隐通道的研究不仅无法从形式化的高度展开,而且只能依赖于试验和观察去发现新的隐通道性质并检验相关处理方法的正确性。（2）研制了一个新的隐通道审计标准。该标准在兼容TCSEC相关标准的基础上,能根据用户的需求,从多个角度去刻画隐通道的威胁。TCSEC使用纯粹的带宽指标来审计隐通道的威胁,带宽越高、威胁越大。这种方法的缺陷是没有综合考虑隐通道其它属性对系统安全造成的危害。例如有两个隐通道,它们的带宽都是200 bits/s,其中一个将保密信息从“绝密”级泄露到“公开”级,而另一个却只是将保密信息从“绝密”级泄露到“机密”级,显然两者对系统安全的威胁并不真正相同。类似的情况还有,如果其中一个仅工作了1秒钟,而另一个却工作了1小时,那又该如何评价它们的威胁?在TCSEC准则关于隐通道的审计标准中,没有回答这些问题。（3）提出了非静态的隐通道搜索和消除方法。静态的隐通道搜索与消除方法,是建立在系统顶级描述或源代码分析基础之上的方法,它们在使用的过程中容易找到一些在实际系统中并不存在的伪非法信息流,而消除这些伪非法信息流不仅会造成系统运行效率的不必要下降,而且会消耗有限的人力、物力资源。非静态的隐通道搜索与消除方法,是在系统动态运行的过程中,根据我们在可计算性研究中推导出的隐通道存在的最小条件去搜索或消除隐通道。因为这类方法是在系统的运行状态下操作的,所以与相应的静态方法相比,它不需要对系统中每种可能的信息流做出合法性判断,而只是分析系统中实际存在的信息流,这样就降低了分析工作的复杂程度,提高了效率。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 隐通道的概念
• 1.2 隐通道的成因
• 1.3 隐通道的分类
• 1.3.1 存储隐通道的实例
• 1.3.2 时间隐通道的实例
• 1.3.3 混合隐通道的实例
• 1.4 国内外的研究现状
• 1.4.1 定义
• 1.4.2 搜索
• 1.4.3 审计
• 1.4.4 消除
• 1.5 本文的主要工作
• 1.6 本文的组织结构
• 第二章 隐通道的形式化定义
• 2.1 可信系统的相关要素
• 2.1.1 安全策略
• 2.1.2 安全模型
• 2.1.2.1 BLP安全模型
• 2.2 隐通道机理的分析
• 2.2.1 信息传导相关要素的定义
• 2.2.2 隐通道元的定义
• 2.2.3 隐通道元之间的依赖关系
• 2.3 隐通道的形式化定义
• 2.4 隐通道形式化描述举例
• 2.5 本章小结
• 第三章 隐通道的性质及其代数系统
• 3.1 隐通道的一般属性
• 3.2 隐通道存在的最小条件
• 3.3 隐通道的可计算属性
• 3.4 隐通道代数系统的定义
• 3.4.1 隐通道集合上的二元关系
• 3.4.2 隐通道的代数系统
• 3.5 隐通道代数系统的运算法则
• 3.5.1 结合律
• 3.5.2 交换律
• 3.6 本章小结
• 第四章 基于可计算性研究的隐通道审计
• 4.1 带宽作为唯一审计参数的局限性
• 4.2 隐通道威胁审计的量化指标
• 4.2.1 隐通道的威胁度和威胁率
• 4.2.2 等效隐通道
• 4.3 隐通道审计的IA（Integrated Audit）标准
• 4.4 隐通道威胁率的计算
• 4.5 隐通道威胁度的计算
• 4.6 带有敏感参数的α-IA标准
• 4.6.1 α-IA标准
• 4.6.2 关于敏感参数的讨论
• 4.7 本章小结
• 第五章 基于可计算性研究的静态隐通道搜索与消除方法分析
• 5.1 基于可计算性研究的搜索方法及其分类
• 5.1.1 成对搜索发送方和接收方的搜索方法
• 5.1.2 检查共享资源的搜索方法
• 5.1.3 检查信息流向的搜索方法
• 5.2 基于可计算性研究的消除方法及其分类
• 5.2.1 打破时间同步的消除方法
• 5.2.2 取消共享资源的消除方法
• 5.3 关于静态隐通道搜索与消除方法的讨论
• 5.4 本章小结
• 第六章 基于可计算性研究的非静态隐通道搜索与消除方法的开发
• 6.1 非静态的隐通道搜索方法
• 6.1.1 静态隐通道搜索方法的一个缺陷
• 6.1.2 IMS搜索算法
• 6.1.2.1 矩阵的构造
• 6.1.2.2 Broker
• 6.1.2.3 搜索算法
• 6.1.2.4 带宽估算
• 6.1.3 IMS算法的正确性
• 6.1.4 IMS的应用举例
• 6.1.4.1 隐通道的设计
• 6.1.4.2 IMS算法的应用结果
• 6.2 非静态的隐通道消除算法
• 6.2.1 静态隐通道消除方法的一个缺陷
• 6.2.2 隐通道的活动层
• 6.2.3 LTHC算法
• 6.2.4 算法的正确性与消除效果
• 6.2.4.1 对存储隐通道的消除
• 6.2.4.2 对时间隐通道的消除
• 6.2.4.3 LTHC的效率
• 6.2.5 LTHC算法的改进形式
• 6.2.5.1 进程选择
• 6.2.5.2 改进算法的讨论
• 6.3 本章小结
• 第七章 隐通道可计算性研究中的一个不可判定问题
• 7.1 隐通道自动搜索程序的性质
• 7.2 与停机问题的关系
• 7.3 与二义性语法的关系
• 7.3.1 隐通道的策略
• 7.3.2 隐通道与二义性语法
• 7.4 本章小结
• 第八章 基于可计算性研究的隐通道仿真分析
• 8.1 隐通道的仿真
• 8.1.1 仿真环境与算法
• 8.1.2 隐通道的通信协议
• 8.2 仿真分析
• 8.2.1 简单通信协议
• 8.2.2 一般通信协议
• 8.2.3 有关带宽的讨论
• 8.2.4 抗干扰仿真
• 8.3 本章小结
• 第九章 结束语与下一步工作
• 9.1 全文总结
• 9.2 下一步工作
• 致谢
• 参考文献
• 附录
• 在学期间参加的科研项目与发表的论文