一种基于指针逻辑的代码安全属性分析方法.doc

一种基于指针逻辑的代码安全属性分析方法* 本课题得到国家“八六三”高技术研究发展计划项目基金(2007AA01Z465、2006AA01Z433和2007AA01Z414)(1971-),女,博士,主要领域为操作系统安全,Tel:(+86)**********, E-mail: ******@.;程亮(1982-),男,博士研究生,主要研究领域为操作系统安全.

张阳1, 程亮2
1(中国科学院软件研究所,北京 100190)
2(中国科学技术大学电子工程与信息科学系,合肥 230027)
摘要: 本文在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法。该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理。
关键词: 操作系统安全;形式化验证;代码分析;模型检测;指针逻辑
中图法分类号 TP309
引言
近几年来发生了多起大规模的安全事件,大部分是由于操作系统安全漏洞所造成的全球大量计算机被感染,造成了重大经济损失。由此,使用自动化的方法从操作系统的源代码出发分析漏洞的存在与否成为当今国际上的一个研究热点。代码(程序)分析的目的在于检验系统的实际代码是否确实满足了或违背了规范中所声明的安全准则。传统的代码分析方式以代码走查(walkthrough)为主,纯手工劳动,费时费力,而且效率低下。目前国际上许多大学和公司都开展自动化的软件错误检查方法的研究,其理论基础包括了模型检测技术(Model Checking)[1]、定理证明技术(Theory Proving)[2]以及约束求解技术(Constraint Solving)[3]。
处于效率的考虑,操作系统代码多半用C语言写成。目前,针对C语言的静态代码属性验证工具多半采用对源代码抽象进行模型检测以发现其中违反待验证安全属性的反例(路径)的办法来实现属性的验证。由于模型检测器生成的反例是基于源代码的抽象模型的,因此,程序抽象技术的好坏就直接影响到反例的正确性。然而,由于C语言中指针的应用非常灵活,多级指针、栈变量指针、运行时内存分配、强制类型转换、函数指针、外部变量指针、地址操作符、结构体和联合体等种种指针的应用使得在程序抽象时处理起来非常困难,因此,大部分的静态代码属性验证工具,如BOOP[4]、BLAST[5]等均没有能对指针作处理,SATABS[6] 则仅能发现对Null指针的脱引用。
而另一方面,基于程序分析理论和方法的代码查错工具,如ESC(Extended Static Checking)[7]和Spec#[8]等,试图通过应用类型系统或者逻辑系统部分实现了对指针的分析处理。然而这类代码差错工具或者只能应对C语言的子集,对待验证程序提出各种限制[9] [10];或者应用太过单一,仅仅能处理如空指针调用之类的内存安全错误[11],而且缺乏可靠性证明,更多地被当作程序差错工具而不是属性验证工具。比如,ured [12],虽然可以C语言中对部分指针实现静态分析,但是它需要插入动态检查代码,这在很多