(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf_第1页
(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf_第2页
(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf_第3页
(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf_第4页
(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf_第5页
已阅读5页,还剩47页未读 继续免费阅读

(计算机科学与技术专业论文)c程序格式串缺陷检测技术.pdf.pdf 免费下载

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

国防科学技术大学研究生院t 学硕七学位论文 摘要 c 语言是功能最强大、使用范围最广的高级程序语言之一。但是,c 语言存在 着很多安全性方面的问题,格式串缺陷就是一种典型的c 程序缺陷。虽然出现较 晚,但它的危害性却一点也不亚于诸如缓冲区溢出等广为人知的c 程序缺陷。例 如,有经验的攻击者能够通过发掘格式串缺陷来修改函数的返回地址,使之跳转 到恶意代码段,从而取得r o o t 权限,随心所欲地从事非法操作。 c q u a l 是一个轻量级的静态程序分析工具,和其他静态分析工具一样,在某些 情况下,c q u a l 会存在一些误报。本文通过一个实例,分析了c q u a l 关于结构体 方面的误报。为了消除这类误报,论文通过向一个类函数式语言中引入模拟c 语 言结构体的记录类型,对c 语言中结构成员之间的关系进行了建模,并在此基础 上扩充了e q u a l 的类型推断规则、类型检查规则和约束求解规则。理论上,它可 以提高c q u a l 在格式串缺陷分析、c o n s t 推断和死锁检测方面的分析精确性。 为了检验对c q u a l 的扩展工作,基于c q u a l ,我们构建了新的程序分析工具 e c q u a l ,并进行了实验。在实验中,我们使用e c q u a l 对一些网络程序进行了格 式串缺陷的检查。与c q u a l 的分析结果相比,它有效地消除了与结构成员相关的 一类误报。 基于已有的格式串缺陷检测思想,我们提出了一种新的格式串缺陷检查和处 理方法l i b f m t g r d 。该方法结合了动态拦截库函数和参数个数比较方法来检测格式 串缺陷攻击。在l i n u x 平台下,我们对它进行了实现。实验发现,与目前的绝大多 数工具相比,它可以发现的格式串缺陷种类更多,并且运行时开销也有所下降, 与f o r m a t g u a r d 和f o r m a t s h i e l d 相比,其运行时开销分别下降了0 1 7 和2 2 9 。 主题词:格式串缺陷,c q u a l ,消除误报,e c q u a l ,l i b f m t g r d 第i 页 国防科学技术大学研究生院下学硕士学位论文 a b s t r a c t t h ec p r o g r a m m i n gl a n g u a g ei so n eo ft h em o s tw i l d l yu s e dl a n g u a g e s h o w e v e r , t h e r ea r es o m es e c u r i t yp r o b l e m si ni t ,f o re x a m p l e ,f o r m a ts t r i n gv u l n e r a b i l i t i e s ,a t y p i c a lo n e t h o u g ha p p e a r i n gr e l a t i v e l yl a t e ,i th a sd o n ea sm u c hh a r ma so t h e r n o t o r i o u sd e f e c t s ,s u c ha sb u f f e ro v e r f l o w e x p e r i e n c e da t t a c k e r sc a ne x p l o i ti tt o m o d i f yt h er e t u ma d d r e s so faf u n c t i o nc a l l ,r e s u l t i n gi nt h ee x e c u t i o no fm a l i c i o u s c o d e s ,s oa st og e tt h er o o tp r i v i l e g et od ow h a t e v e rt h e yw a n t c q u a li sal i g h t w e i g h tp r o g r a ma n a l y s i st 0 0 1 l i k eo t h e rs t a t i ca n a l y s i st o o l s ,i t m a yl e a dt oaf e wf a l s ep o s i t i v e si ns o m es i t u a t i o n s i nt h i sp a p e r w ea n a l y z et h ef a l s e p o s i t i v eo ft h es t r u c t st h r o u g hap i e c eo fc o d e i no r d e rt or e d u c et h ef a l s ep o s i t i v ea n d i m p r o v et h ep r e c i s i o n ,w ea d dar e c o r dt y p et ol a m b d ac a l c u l u st oi m i t a t et h es t r u c t si n c ,a n db a s e do nt h a t ,w em o d e lt h er e l a t i o na m o n gf i e l d so fs t r u c t s a n de x p a n dm e r u l e so ft y p ei n f e r e n c e ,t y p ec h e c k i n ga n dc o n s t r a i n ts o l v i n g t h e o r e t i c a l l y ,i tw i l l r e d u c es o m ef a l s ep o s i t i v e si nf o r m a ts t r i n gb u g sd e t e c t i o n ,c o n s ti n f e r e n c ea n dd e a d l o c kd e t e c t i o n i no r d e rt oe v a l u a t et h ee x t e n s i o no fc q u a l ,w eb u i l dat o o ln a m e de c q u a lb a s e d o nc q u a l i nt h ee x p e r i m e n t ,w eu s e e c q u a lt oc h e c kt h ef o r m a ts t r i n gb u g si naf e w n e t w o r kp r o g r a m s c o m p a r e dw i t ht h er e s u l t so fc q u a l ,i tr e m o v e sak i n do ff a l s e p o s i t i v e s ,w h i c ha r er e l a t e dt of i e l d so fs t r u c t s b a s e do nf o r m e rt h o u g h t so ff o r m a ts t r i n gb u g sd e t e c t i o n ,w ep r o p o s ean o v e l m e t h o dn a m e dl i b f m t g r d ,w h i c hc o m b i n e sd l l i n j e c t i o na n dc o m p a r i s o no ft h e n u m b e ro fp a r a m e t e r st od e t e c tp o t e n t i a lf o r m a ts t r i n ga t t a c k s w ei m p l e m e n tt h et o o l o nt h el i n u xp l a t f o r ma n dd os o m ee x p e r i m e n t s t h er e s u l t sr e v e a lt h a ti tc a nf i n dm o s t k i n d so ff o r m a t s t r i n gb u g s a n dw h e nc o m p a r e d w i t hf o r m a t g u a r da n d f o r m a t s h i e l d ,t h er u n t i m eb u r d e nh a v i n gb e e nr e d u c e db yo 17 a n d2 2 9 r e s p e c t i v e l y k e yw o r d s :f o r m a ts t r i n gb u g ,c q u a l ,r e m o v i n gf a l s ep o s i t i v e ,l i b f m t g r d 第i i 页 国防科学技术大学研究生院工学硕士学位论文 表目录 表1 1 近5 年格式串缺陷出现情况统计。3 表1 2 当前分析工具在程序生命周期中的位置一5 表3 1 选择的网络程序列表2 6 表3 2 使用c q u a l 和e c q u a l 对网络程序进行分析2 6 表3 3 当前分析工具分析能力对比2 8 表4 1 安全性测试3 5 表4 2 运行m i c r o b e n c h m a r k 的结果3 6 表4 3 运行m a c r o b e n c h m a r k 的结果3 7 表4 4e c q u a l 与l i b f m g r d 功能对比3 8 第1 i i 页 国防科学技术大学研究生院工学硕士学位论文 图2 1 图2 2 图2 3 图2 4 图2 5 图2 6 图2 7 图2 8 图2 9 图2 1 0 图2 1 1 图2 1 2 图3 。l 图3 2 图3 3 图4 1 图4 2 图4 3 图4 4 图4 5 图4 6 图目录 限定子偏序及其合成9 c q u a l 分析流程1 0 一段c q u a l 产生误报的代码片段。1 1 c q u a l 分析图2 3 中代码产生的误报11 图2 3 中代码生成的约束1 2 添加了记录类型的类函数式语言。1 3 限定子类型之间的子类型关系。1 4 添加了限定子标注与检查后的类函数式语言。1 5 s t r i p 和e m b e d 函数的定义1 6 类函数式语言的类型推断系统1 8 类函数式语言的类型检查系统1 9 从子类型约束到限定子约束的变换规则2 0 e c q u a l 对结构体赋值的处理2 3 使用e c q u a l 分析图2 2 中代码2 4 新生成的约束。2 5 w u f t p d2 6 0 中存在的格式串缺陷3 0 容易招致读攻击的代码片段。3l l i b f m t g r d 分析流程3 2 对图4 1 中的程序插入终结符3 3 l i b f m t g r d 执行的核心代码3 4 性能测试程序3 6 第1 v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果。尽我所知,除了文中特别加以标注和致谢的地方外,论文中不包含其他人已 经发表和撰写过的研究成果,也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意 学位论文题目: 堡猩庄整盛塞遮陷拴趔技盔 学位做作者擀:童啦 帆拼,1 月哆日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档,允 许论文被查阅和借阅;可以将学位论文的全部或部分内容编入有关数据库进行检索, 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文 ( 保密学位论文在解密后适用本授权书。) 日期:加释,月乡日 日期:占年,2 月哆日 国防科学技术大学研究生院工学硕士学位论文 第一章引言弟一早jl 百 随着因特网的迅速发展与普及,计算机被越来越多的应用于人们的工作和日常 生活中。程序的互联带来了信息共享的深入,方便了人们工作和生活。但不幸的 是,信息共享与信息安全在某种程度上是矛盾的,极少信息系统能同时满足两者 的要求。 信息安全的概念是多方面的,其中一个国际性的难题就是软件的安全性。我们 已经见识过太多的由软件缺陷导致的安全问题,在一些关键的系统中,这甚至会 导致大的灾难。比如,1 9 9 6 年a r i a n a 5 型火箭发射失败,事后查明就是由于软件失 效。美国1 9 9 9 年发射的火星探测器m a r sc l i m a t eo r b i t e r 在登陆火星的时候坠毁【4 3 j , 后来追查原因,发现就是程序员没有处理好英制单位和公制单位的转换。 软件的安全性之所以难以解决,归根结底源自两个方面。首先,目前己知的安 全漏洞很难彻底根治。因此,每隔几年,就会有一些新的攻击手段出现,让人措 手不及。其次,总会有未知的安全性缺陷出现,这导致软件的安全性成为了一个 持久的话题。 由于c 语言在灵活性和性能方面的优势,它仍然被广泛的应用在系统软件的开 发中。但是,c 语言也是一门危险的语言,它恶名昭著的指针操作问题让很多程序 员头疼不已,很多成熟的软件系统都存在诸如空指针引用、内存泄漏之类的缺陷。 同时,数组越界、缓冲区溢出、格式串缺陷之类的漏洞也常常让安全人员措手不 及。 人们很早就已经意识到了软件安全可能导致的问题。事实上,对于规模越来越 庞大的程序,用人眼分析源代码查找缺陷是不现实的。自2 0 世纪6 0 年代起,计算 机科学家们就开始了对程序分析和验证技术的探索。程序分析主要是通过一定的 自动化技术对程序源代码进行分析,以检查其中的错误。时至今日,程序分析技 术已经取得了很大的进展,涌现出了一大批有效的程序分析理论和工具。另一支 常用的保证程序质量的技术就是程序测试,它通过运行程序来观察对于特定的输 入,是否能得到理想的输出。与之相比,程序分析能够发现很多测试无法觉察的 错误。 程序分析技术又分为静态分析和动态分析两种。前者能够较早的发现错误, 而且由于覆盖率高,能够发现的错误更多,不足之处是在某些情况下会存在误报; 后者在精确性上则具有天然的优势,但是需要运行程序,而且很多时候依据技术 的不同会导致不同的效果。两者不是相互替代的关系,而是互为补充。分析程序 的时候,如果将两者结合起来,往往具有较好的效果。 论文针对格式串缺陷问题,研究了如何使用程序静态分析、静态和动态分析 第1 页 国防科学技术大学研究生院t 学硕十学位论文 相结合的方法来检测c 程序存中的缺陷,提高检测的精度和完备性,降低误报。第 1 1 节简要介绍了c 程序中格式串缺陷及其造成的后果;第1 2 节介绍总结了当前格 式串缺陷检测工作的现状;第1 3 节给出了论文的主要工作和取得的成果;第1 4 节 对论文的结构进行了介绍。 1 1 格式串缺陷 格式串缺附l 】被发现于2 0 0 0 年左右,在一开始,人们认为它是无害的。但是 不久,它便向人们展示了它们的威力。入侵者可以修改函数的返回地址,让其跳 转到任意地址,带来的危害一种是使程序崩溃导致拒绝服务,还有一种就是执行 恶意代码,使得攻击者获取r o o t 权限,然后为所欲为,这都会给系统安全造成了 巨大的危害。 格式串缺陷的一个最简单的场景是,在c 源代码中应该书写成p r i n t f ( ”s ”, b u f f e r ) 的地方,程序员为了节约时间和提高效率简写成了p r i n t f ( b u f f e r ) 。事实上, p r i n t f 的第一个参数无论如何都是会输出的,似乎没有什么不妥。不幸的是,这时 编译器会把b u f f e r 理解成一个格式串。如果恶意人员可以修改这个b u f f e r ,在其中 添加“s ”等格式串标记,程序就会打印出堆栈中的内容,攻击者就可以偷看程序 的内存,给后面的攻击埋下了伏笔。一个更有效的攻击手段是进行了精确的计算 后在其中添加“n ”1 ,强迫修改函数的返回地址,使之指向一段恶意代码。这样, 攻击者便可以获取r o o t 权限,达到其不可告人的目的。 在实际应用中发现的格式串缺陷情况有很多种,也会比这个复杂,因此就不 像这个这么容易修正。如果在程序中用到了包装函数或者类v p r i n t f 的函数,用户 在使用的时候就比较容易犯错。 我们可以看到,导致格式串攻击的深层原因是在部分c 库函数中缺少对实参 的有效过滤,这是c 语言效率优先的原则所导致的。调查发现,格式串缺陷也不 仅仅出现在c 语言中,p e r l 程序中也有出现1 4 。 在实际应用中,格式串缺陷是比较常见的。c v e 上的搜索结果显示,截止2 0 0 7 年,人们已经发现了4 0 0 多个格式串缺陷【4 】。表1 1 中分别介绍了从2 0 0 1 年到2 0 0 6 年间,格式串缺陷在所有领域和操作系统领域的出现情况。“数目”栏介绍了当 年发现的格式串缺陷的数目,例如2 0 0 1 年在操作系统领域中共发现了2 3 个格式 串缺陷;“比例”栏描述了当年格式串缺陷在所有常见缺陷中的比例:“排名 栏列出了对所有3 7 中常见缺陷按数目进行排序时,格式串缺陷所处的位置。从表 中易见,在过去几年,格式串缺陷几乎一直排列在软件缺陷的前十位。 1 转换说明符能够将p r i n t f 函数已经输j l ;的字符数写入内存 第2 页 国防科学技术大学研究生院_ t 学硕+ 学位论文 表1 1 近5 年格式串缺陷出现情况统计 2 0 0 l2 0 0 2 2 0 0 32 0 0 42 0 0 5 2 0 0 6 总计 数目 4 63 93 26 27 66 23 1 7 所有领域比例 3 2 1 8 2 7 2 4 1 7 0 9 1 7 排名 71 0789l l9 数目2 31 01 22 l2 91 91 1 4 操作系统比例 5 2 1 5 2 3 2 8 2 4 1 5 2 3 排名 4 955596 1 2 格式串缺陷检测方法 第一个格式串缺陷出现之后,包括w i r e x 通信公司等在内的很多研究机构就 如何避免遭受格式串攻击开展了有效的研究。到目前为止,格式串缺陷检测相关 的工作主要分为以下几类: 1 2 - 1 程序静态分析 a l a nd e k o k 编写了一个程序p s c a n 7 。,来查找c 代码中潜在的格式串缺陷。 它的主要思想是扫描函数的最后一个参数,如果它是一个动态的格式串,则报错。 g e e 也提供了一个标记“w f o r m a t = 2 ”来静态的检查格式串缺陷。这两种方法使用 的都是词法分析的方法,虽然易于实现、分析速度快,但是分析能力却远远比不 上使用了流分析的静态分析。事实上,许多格式串缺陷都是简单的词法分析所不 能发现的,比如含有动态字符串的格式串。 u s h a n k a r 等人使用基于约束的类型推断方法来检查程序中是否存在格式串缺 陷【6 1 。他们使用c q u a l 分析了几个开源的网络程序,实验结果发现了一些前所未知 的格式串缺陷。这种方法可扩展性好,并且提供了直观的用户界面供程序分析人 员查错使用。o i n k 是对c q u a l 的改写,它也支持处理c + + 程序。k a r lc h e n 等人使 用o i n k 对d e b i a nl i n u x 中的c c + + 源码包进行了大规模的分析【l 列,发现了源码包 中大量的格式串缺陷。这两种都是静态的流分析方法,可以尽早地查找出程序中 存在的缺陷,具有良好的覆盖率,并且不增加运行时开销。但是,和其他静态的 分析方法一样,在某些情况下,存在一定的误报。 1 2 2 动态分析 动态分析格式串缺陷是指在运行时检测程序中的格式串缺陷,通常是通过加 第3 页 国防科学技术大学研究生院t 学硕十学位论文 入额外的库函数处理输入输出参数实现,其优点在于实现灵活方便,实现代价低, 缺点在于引入了运行时开销。 例如,l i b f o r m a t 库【l l j 的主要思想是通过动态链接器将自己插入到程序中,在 程序以后的运行中如果发现了包含“n ”的格式串出现在可写内存中,则终止程序。 l i b s a f e t l 5 】实现的思想与l i b f o r m a t 类似,但是它们检查函数参数的方法不同。它 们的优势是实现灵活方便,并且成本很低。但是,在多数情况下,出现在可写内 存中的包含n 的格式串是合法的,这就会造成误报。而且,这种方法不能抵御读 攻击和非控制数据攻击。因此,它既不是可靠的,也不是完备的。 1 2 3 综合静态和动态分析 为了更好的处理精确性和可扩展性之间的平衡,很多程序分析人员开始着手 结合静态分析和动态分析的手段来检测格式串缺陷。 c c o w a n 等人提出了一种f o r m a t g u a r d 的方法来弥补格式串缺附5 1 ,他们通过 计算参数的个数来保证安全性。实验表明,该方法有效的降低了格式串缺陷,而 且系统性能下降不到2 ,是一种有效的分析方法。但是,它不能处理用户自定义 的包装函数。m f r i n g e n b u r g 和d g r o s s m a n 综合应用了静态分析和动态分析的方 法,通过将静态分析的信息提供给运行时动态维护的链表( w h i t e 1 i s t ) ,有效减轻了 运行时的负担i l 引,但是它不能检测读攻击。p k o h l i 和b b r u h a d e s h w a r 提出的 f o r m a t s h i e l d 通过将那些可能有害的调用场景保存在二进制文件中,能够保证在下 一次遇到这样的场景时避免遭受格式串攻击【1 4 1 。这种方法的缺点是在对格式串攻 击免疫之前必须进行综合处理,以发现那些可能有害的调用场景。 1 2 4 总结 从程序生命周期的角度来看,所有的程序分析工具在这个过程中都有自己的 坐标。表1 2 分析了当前格式串缺陷检测工具在程序生命周期中所处的阶段。 在表1 2 中,按照程序编译、运行的过程,我们将当前工具进行了排列。从表 中可以看出,在程序编译的前几个阶段,从预处理到语义分析,都出现了相应的 程序分析工具。理论上,预处理只进行了基本的包含文件的插入和宏替换操作, 不具备独立的程序分析功能,因此一般只是作为程序分析工具的一部分,并不独 立出现( f o r m a t g u a r d 就综合使用了预处理和动态分析的方法) 。词法分析工具可 以作为一个独立的程序分析工具出现,但是它只处理词法匹配,因此分析能力最 弱。语法分析基于词法分析的基础之上,它还考虑了程序的语法结构,因此分析 能力稍强。要达到更好的分析效果,仅仅语法分析还是不够的,主流的程序分析 工具一般都会采用语义值流分析。 第4 页 国防科学技术大学研究生院工学硕士学位论文 表1 2 当前分析工具在程序生命周期中的位置 所处阶段分析工具备注 预处理提供的宏功能来对p r i n t f 函数 静 预处理f o r m a t g u a r d 中的参数个数进行计数 态 词法分析 p s c a n g c c 分 语法分析l i b f m t g r d 使用语法分析手段添加终止符 析 c q u a i o i n k e c q u a l 语义,值流分析 w h i t e 1 i s t 动拦截库函数的调用 l i b s a f e l i b f o r m a t l i b f m t g r d 态 f o r m a t g u a r d 动态检杏 分 程序执行 w h i t e 1 i s t 静态存储、动态布询 析 f o r m a t s h i e l d 二进制重写、动态查询 目前,程序的动态分析手段也呈现多样化。除了程序测试,仍有很多其他动 态分析的手段,本章1 2 2 和1 2 3 节中就介绍了格式串缺陷分析方面的一些动态 方法。 1 3 论文的研究内容和取得的主要成果 针对当前格式串缺陷分析方法存在的不足,论文在分析总结格式串缺陷、缺 陷分析技术的基础上,主要针对两个方面展开研究:一是扩展c q u a l 对结构体成 员的建模和分析,提高静态缺陷分析的精确度,减少误报;二是结合静态分析和 动态分析,通过静态参数插入、动态拦截库函数,提高缺陷分析能力,并减少运 行时开销。论文取得的主要成果如下: ( 1 ) 对c 语言结构成员关系进行建模,扩展c q u a l 的类型推断规则、类型检查规 则和约束生成规则,提高c q u a l 分析精确性,降低误报率 c q u a l 是一个轻量级的静态程序分析工具,可以用来检测c 程序中的格式串 缺陷、进行c o n s t 推断、死锁检测等等。和其他静态分析工具一样,在某些情况下, c q u a l 会存在一些误报。由于c q u a l 缺乏对结构体成员之间关系的建模,不支持 成员层次的多态,导致产生了误报。针对这个问题,论文通过向一个类函数式语 言引入模拟c 语言结构体的记录类型,对c 语言中结构成员之间的关系进行了建 模,并在此基础上扩展了类型推断规则、类型检查规则和约束生成规则,以减少 c q u a l 在进行程序分析时的误报。 ( 2 ) 基于c q u a l ,实现了针对结构的扩展e c q u a l ( e x t e n d e dc q u a l ) ,实验表明论 第5 页 国防科学技术大学研究生院丁学硕十学位论文 文提出的扩展有效地消除了与c 语言结构体相关的一类误报 基于( 1 ) 中提出的理论,我们在c q u a l 基础上实现了支持结构体成员处理的 e c q u m 。为了避免影响e c q u a l 的执行效率,我们使用h a s h 表等数据结构来存储 和处理程序中出现过的结构体成员,避免造成空间耗尽,同时减少查询时间。 为了评估e c q u a l 的实验效果,我们选择了一些常用的网络程序进行测试,包 括f t p 服务器程序b f i p d 等。文中分别使用c q u a l 和e c q u a l 对这些程序进行了格 式串缺陷检查。结果表明,e c q u a l 能够有效处理结构体成员,有效的消除了相关 误报。 ( 3 ) 结合静态参数插入和动态拦截库函数,提出并实现了l i b f m t g r d 方法,弥补 当前基于库方法的不足,能够有效地处理变参函数中的格式串缺陷 目前已经出现了一批处理格式串缺陷的方法,例如l i b f o r m a t 、f o r m a t g u a r d 等,但是都只能处理特定的格式串缺陷。基于这些方法,论文提出并实现了一种 新的格式串缺陷检查和处理方法l i b f m t g r d 。该方法首先识别程序中对所有变参函 数的调用,并进行静态插入;接着使用动态拦截库函数加载的方法来拦截对类p r i n t f 函数2 和类v p r i m f 函数3 的调用;然后通过对转换说明符和参数进行计数和比较,以 检测格式串缺陷攻击。如果发现潜在的攻击,则发出警告并杀死进程,否则继续 原来的执行逻辑。实验表明,与目前的绝大多数工具相比,它可以发现的格式串 缺陷种类更多;并且具有良好的运行时表现:与f o r m a t g u a r d 和f o r m a t s h i e l d 相比, 对m a n 2 h t m l 程序的运行时开销分别下降了0 1 7 和2 2 9 。 1 4 本文的结构 论文共分为五章。 第一章为引言。首先描述了论文研究的背景和意义,然后介绍了c 程序中的 格式串缺陷,分析总结了当前格式串缺陷的检测方法,最后给出了论文的主要工 作和取得的主要成果。 第二章首先介绍了c q u a l 的背景,然后基于一个简单的类函数式语言,重点 介绍了我们对c q u a l 的改进工作,包括扩展后的子类型构成规则、类型推断系统、 类型检查系统和约束生成系统等。 第三章中,我们对程序分析工具c q u a l 进行了扩展实现,使得它可以支持结 构体成员的多态。为了保证执行效率,我们添加了一些数据结构,从而构建了新 2 类p r i n t f 函数包括p r i n t f , s p r i n t f , s n p r i n t f , f p r i n t f , s y s l o g 等函数,它们接受可变参数 3 类v p r i n t f 函数主要包括v p d n t f , v s p r i n t v s n p r i n t v 巾r i n t c v s y s l o g 等函数,它们接受固定数目的参数,不过含 有一个v al i s t 类型的参数,该参数中封装了町变参数 第6 页 国防科学技术大学研究生院工学硕士学位论文 的程序分析工具e c q u a l 。而后,我们通过实验分析了改进工作的有效性,并把 e c q u a l 与当前的格式串缺陷分析工具进行了对比。 第四章中首先介绍了前人提出的两种格式串缺陷检查方法,基于它们,我们 提出了一种新的格式串缺陷检查和处理方法l i b f m t g r d ,并进行了实现和实验。在 实验中,我们测试了它的安全性,以及增加的运行时负担。接着,我们讨论了这 种方法在功能性方面的状况。最后,我们对当前的格式串检测手段进行了总结和 分析。 第五章中总结了本文所做的贡献,并对未来的工作进行了展望。 第7 页 国防科学技术大学研究生院工学硕士学位论文 第二章扩展c q u a l 支持结构体成员多态的研究 c q u a l 是一个基于类型的轻量级的程序分析工具,适合于值流分析。由于它具 有概念简单,可扩展性好等方面的优势,s h a n k a r 等人使用它对格式串缺陷进行了 分析【6 j ,发现了一些成熟程序中以前未知的的b u g 。 但是,与其他静态分析方法一样,c q u a l 也存在误报。而且,由于c q u a l 在 设计之初就以系统的可靠性为目标,这导致了它在某些时候具有较大的误报量, 加重了分析人员排错的负担。 为了使c q u a l 具有更好的可用性,我们检查了c q u a l 存在的误报。分析发现, 一个典型的误报是由c q u a l 不支持c 语言结构体成员的多态所造成的。于是,我 们对c q u a l 从理论上进行了改进:对结构成员之间关系进行了建模,扩充了类型 推断规则、类型检查规则和约束生成规则,以减少c q u a l 的误报。理论上,它可 以提高c q u a l 在格式串缺陷分析、c o n s t 推断等方面的精确性。 本章的结构如下:第2 1 节介绍了c q u a l 的相关背景,并分析了c q u a l 存在 的误报;第2 2 节中引入一个新增了记录结构的类函数式语言,并介绍了如何通过 限定子之间的偏序关系构造子类型关系;第2 3 节中模拟了程序分析人员添加类型 限定子和进行检查的工作;第2 4 节和2 5 节介绍了带限定子的类型推断系统和类 型检查系统;第2 6 节扩充了基于类函数式语言的约束生成规则;第2 7 节讨论了 c q u a l 所支持的多态。 2 1c q u a l 背景 c q u a l 2 】是一个基于类型的程序分析工具,它提供了一个轻量级的框架,使得 用户可以通过使用类型限定子,来分析传统类型系统所不能捕获的一些安全性质。 程序员通过格配置文件定义自己的类型限定子,并对程序进行少量的插入,c q u a l 能够自动推断剩余变量的类型限定子,并检查它们的一致性。 目f j ,程序分析人员已经把c q u a l 应用到了诸如格式串缺陷、c o n s t 推断、死 锁检测等方面【3 l ,取得了很好的效果。 2 1 。1 类型限定子 顾名思义,类型限定子就是类型的修饰符。阅读c 9 9 的参考文档就可以发现, c 语言已经支持了类型限定子,比如c o n s t ,r e g i s t e r 等。在c q u a l 的格配置文件中, 用户可以按一定的规则添加自定义的类型限定子( 为了便于分析,目前c q u a l 只 支持构成偏序和离散偏序的限定子集【3 1 ) ,这部分限定子就是限定子常量。在分析 第8 页 国防科学技术大学研究生院工学硕士学位论文 格式串缺陷的过程中,可以取$ t a i n t e d 和$ u n t a i n t e d 两个限定子常量,并且规定它 们构成偏序关系$ u n t a i n t e d 其中,q 表示类型限定子,彳表示带限定子的类型,v 表示剥去最外层限定子 后的类型。容易看到,f 和1 ,是递归定义的,记录类型本身可以有一个类型限定子, 而其成员也可以有各自的类型限定子。为了避免歧义,对于带标记的函数类型我 们记录为g f f ,) 。这样,我们已经得到了带限定子的类型和限定子之间的偏序 关系。c q u a l 的一个关键的思想是通过类型限定子之间的偏序关系可以引入带限定 子类型之间的子类型关系。基于图2 6 的类函数式语言,通过限定子之间的偏序关 系,我们构造了带限定子类型之间的子类型关系,如图2 7 。 c :一v le le 2 il e tx m e li ne 2 ir e f e i 事e e 1 e 2 e l := e 2 v :ox in g x :s e s := i n t r e f ( s ) i s i ;s 。 | s i ,s 2 值 应用 名字绑定 指针 解引用 取结构成员 ( ) 赋值 变量 整数 函数 整数类型 指向类型s 的指针 记录类型 ( ) 参数类型是s i ,返回 类型是s 2 的函数类型 图2 6 添加了记录类型的类函数式语言 如果f 是f 的子类型,表示f 可以使用的地方f 也可以使用。规则i n t 纛示如 果限定子q 和q 满足偏序关系q 姐,那么q 砌,是q i n t 的子类型( 这里重载 了操作符。这条规则同样可以应用于o 元的其他类型构造器,比如c h a r ,f l o a t , d o u b l e 。砌疗规则中,最外层限定子的关系与i n t 洲,但它同时要求,作为两个 第1 3 页 国防科学技术大学研究生院t 学硕士学位论文 函数类型,子类型的值域必须是父类型的值域的子类型,而它定义域则必须是父 类型的定义域的超类型【3 。只有这样,才能保证父类型可以使用的地方,子类型 都可以使用。r e c o r d 搠1 j 规定了如何构成两个具有子类型关系的记录。如果记录 刁;死;r n ) 的所有成员类型都是 订;f 2 ; 对应成员类型的子类型,并且q 和q 满足偏序关系q 知,那么, n ;r 2 ;葡) 就是 死;记;r n ) 的子类型。 矗餮熹( i n t d i n t qi n t q q q f - g f f qr e f ( r ) q r e f ( r 9 ( r 叽) 杀等努q 嚣岛c 帆,q ( r l 寸f 2 ) ( r l j 吒) 、 纠 恭q 篆装鑫q 赢器c 胁。以, f l ;屯;乙 q ;r 2 ;l ) 、 37 图2 7 限定子类型之间的子类型关系 由于指针操作的特殊性【4 0 1 ,r 呱规则规定在前提中必须满足f = r ,即指针必 须指向相同的类型。这是一种比较保守的方式,在一定的条件下可以适当放宽, 具体可以参见 2 】。 一般来说,对于类型构造器f ,如下规则 q q t = ti

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论