论文部分内容阅读
随着Internet的不断发展,人们越来越多地从网上下载并使用程序,程序信息流安全问题越来越重要。程序信息流安全问题是指程序能否保护重要数据的机密性和完整性。数据机密性的保护是指程序不让窃密者通过其所能得到的输出数据等信息来获取或推断程序中的机密数据(如用户密码),数据完整性的保护是指程序不让窃密者通过调整给程序的输入数据等方式来篡改程序中的机密数据。本文研究使用基于语言的技术来保护程序信息流安全。鉴于保护数据机密性的方法也可用于保护数据完整性,所以本文的程序信息流安全研究以数据机密性的保护为研究对象。为了保护重要数据的机密性,机密性的安全策略通常要求程序具有如下的安全性质:高安全级别的输入数据的变化不会影响低安全级别输出数据的变化。文献中将这种安全性质称作无干扰性。
本文综合叙述了已有的基于编程语言的软件安全研究:带证明的代码(PCC)和类型化汇编语言(TAL)两种方法针对的安全策略都是最基本的安全策略如内存安全、控制流安全和栈安全;信息流安全编程语言则实施信息流安全策略,它扩大了所描述的类型安全,使其包含无干扰性。
本文首先考虑一个简单的移动计算模型,以此为基础,着重考虑了代码移动对程序信息流安全的影响,确定相应的安全策略。在Cornell大学Zdancewic的工作(函数式语言λsec的单进程程序信息流安全)的基础上,根据移动计算系统的结构特征,通过对函数式语言λsec进行扩充,加入通讯原语,将其扩展成移动计算语言MobileML,设计了相应的信息流类型系统,用以类型检查保证MobileML语言程序信息流安全。
鉴于实际使用的分布式移动计算系统中的主机数目通常多于两个,进程会根据需要自动创建。我们研究了多进程分布式计算系统中进程之间的通讯对系统信息流安全的影响。通过对MobileML语言进行扩充,加入进程产生表达式,将其扩展成分布式移动计算语言ConcurML,并设计了两级信息流类型系统(基于源语言的类型检查和基于进程演算的类型检查),保证进程之间的通讯不会导致信息泄密。
基于类型的分析虽然是检查程序信息流安全的一种有效方法,但过于保守。本文也尝试将传统的数据流分析方法用于单进程程序信息流安全的检查,即利用数据流分析来跟踪程序数据间的安全依赖关系,达到检查程序信息流安全的目的。和基于类型的方法相比,数据流分析方法能更加精确地分析程序,具有更大的宽容性。