论文摘要
随着国家、社会对计算机和网络技术的依赖程度日益增长,信息安全问题越来越重要。访问控制、加密技术等标准的安全机制是保护信息机密性、完整性的重要手段,但是它们并不能确保端到端的安全,而这必须要控制程序信息流才能做到。近年来研究人员广泛借助于进程代数和类型系统等程序设计语言的理论工具分析系统的信息流,排除系统中潜在的隐蔽信道。基于语言的信息流控制中应用最为广泛的模型是无干扰模型:机密输入数据的变化不会影响公共可见的输出数据的变化。但是它的性质太强,阻止了很多系统上的正常应用。实用软件中有时需要对机密信息做降密处理,指定信息从高安全级流向低安全级。针对这种需求,本文研究使用基于程序设计语言的技术来控制信息安全降密,主要包括以下四方面的工作:首先,针对动态安全降密控制问题,提出动态鲁棒降密模型。建立包含机密性级别和完整性级别的安全格,然后从“哪儿”和“何时”的角度描述数据的完整性级别升级策略。该策略指定数据可从哪个完整性级别开始升级,又至哪个级别升级结束,以及每一步升级时要满足的安全语义条件。虽然安全降密只能发生在高完整性级别的程序上下文中,但是不可信的低完整性数据就能以这种严格受限的方式升级到高完整性级别以影响机密数据释放。本文还设计了灵活的类型系统,允许开发者根据应用需求和程序特点选择合适的静态条件分析技术(如数据流分析方法、抽象解释等)引入类型检查,用于推断数据完整性级别升级时安全条件是否满足。其次,面向多线程程序中的信息流控制问题,本文基于强互模拟等价的方式定义了多线程环境下能同时处理信息降密和抹除的安全模型。它在任意线程调度方式下都是鲁棒的,能精确地控制哪些信息才被允许释放,使得降密机制不会被攻击者破坏而获得多余的机密信息,并且能确保低安全级别信息被抹除后不会被攻击者滥用。为了检查程序是否满足安全需求,本文构造了实施同一安全策略的非转换类型系统和转换类型系统。前者简单地判断一个给定的程序是否为良类型,而后者使用交叉拷贝技术消除由于线程之间互相竞争执行引起的内部时间隐蔽通道。如果程序被非转换类型系统判定为非良类型,可使用转换类型系统尝试将其转换成一个具有相同语义的安全程序。如果还是没有相应的转换类型规则能应用到程序上,那么程序就会被判定为不安全的。接着,针对概率系统中的安全降密控制,本文将非传递无干扰信息流安全模型由确定系统推广到概率系统。为了模拟实际系统中的可信部分,将可信域的概念引入概率安全进程代数,然后在弱概率互拟等价的基础上提出了非传递概率互拟强无干扰(I_BSPNI)和非传递概率互拟复合不可演绎(I_PBNDC)安全属性。为了揭露出I_PBNDC在动态环境中不能暴露的安全隐患,提出了要求系统所有可达状态都满足I_PBNDC的持久I_PBNDC属性。接着使用基于单步状态的展开条件定义了易于验证的强I_PBNDC属性。本文还分析了一个实际概率路由系统上的非传递信息流安全属性。最后,面向概率时间系统中的安全降密控制问题,本文以概率时间自动机为形式化工具将非传递无干扰模型扩展到概率时间系统,使其能够应用于诸如实时系统之类的时间系统上的信息流分析。本文根据高安全域、低安全域和可信域划分概率时间自动机中的动作集合,然后提出了非传递概率时间无干扰(I_PTNI)和非传递概率时间复合不可演绎(I_PTNDC)。这些安全属性不仅能够分析概率时间系统中的非传递信息流,而且能够探测系统中的概率隐蔽通道和时间隐蔽通道。总而言之,本文所提出的理论使得基于程序设计语言的安全降密模型走向实用,能更有效地应用于实际系统的开发以及安全验证。