（计算机软件与理论专业论文）一种基于契约的安全分析方法的研究与实现.pdf

摘要 本文针对c c + + 程序安全漏洞，提出并实现了一种基于契约的安全分析方法。 该方法采用自下而上分析遍历程序中的函数体，将跨过程分析转变为过程内分析： 提供安全规则描述方法，使得用户可以扩展安全规则；通过为变量和函数附加契 约以记录其前置和后置条件，并在程序分析的过程中按照规则更新契约，使得在 程序分析时自动进行安全检查。该方法具有代价小，灵活性强的特点，可以用来 检查程序中指针非法引用、函数调用时实参或全局变量的状态不合法、内存泄漏 及其他资源泄漏等安全漏洞。 关键词：基于契约安全分析前置条件后置条件安全规则 a b s t r a c t ac o n l t a c t - b a s e ds a f e t ya n a l y s i sm e t h o df o rd e t e c t i n gca n dc + + s a f e t yh o l e si s p r o p o s e d a n di m p l e m e n t e di nt h i s p a p e r w i mb o t t o m 叩a n a l y s i s ，t h ep r o c e s so f i n t e r p r o c e d u m la n a l y s i si st r a n s f o r m e di n t ot h ei n t r a p r o c e d u r a la n a l y s i s af o r m a tf o r d e s c r i p t i n gs a f e t yr u l e si sd e s i g n e ds ot h a ts a f e t yr u l e sc a nb ee x p a n d e db yu s e r s b y a s s o c i a t i n gv a r i a b l e sa n df u n c t i o n sw i t hc o n t r a c t st or e c o r dp r ea n dp o s tc o n d i t i o n s ，a n d u p d a t i n gt h ec o n t r a c t sa c c o r d i n gt ot h er u l e sc o n s t r u c t e d ，s a f e t yc h e c k i n gc a nb ed o n e a u t o m a t i c a l l yd u r i n gt h ep r o g r a ma n a l y s i s t l l em e t h o dc a nb eu s e dt od e t e c ts a f e t y h o l e s ，s u c ha si l l e g a lp o i n t e rr e f e r e n c e s ，t h eu s eo fi l l e g a ls t a t u s e so ff i m c t i o na r g u m e n t s o rg l o b a lv a r i a b l e sd u r i n gaf u n c t i o nc a l l ，m e m o r yl e a k s ，a n do t h e rr e s o u r c el e a k s ，a ta l o wc o s ta n dw i t hh i g hf l e x i b i l i t y k e y w o r d s ：c o n t r a c t - b a s e ds a f e t ya n a l y s i s p r ec o n d i t i o n p o s tc o n d i t i o n s a f e t yr u l e s 创新性声明 本人声明所呈交的论文是我个人在导师的指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中 不包含其他人已经发表或撰写过的研究成果，也不包含为获得西安电子科技大学 或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究工 作所做的任何贡献均己在论文中作了明确的说明并表示了谢意。 申请学位论文若有不实之处，本人承担一切相关责任。 本人签名日期 关于论文使用授权的说明 本人完全了解话安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其他复制手段保存论文。( 保密的论文 在解密后遵守此规定) 本学位论文属于保密在年解密后适用本授权书。 本人签名 导师签名 日期 日期：挪；? 第一章绪论 第一章绪论 1 1 研究背景 c c + + 程序设计语言由于灵活高效、功能强大的特点，在软件开发领域中得到 了广泛的应用，但在提供灵活控制能力的同时也带来了一些潜在的安全性问题， c c + + 程序中易出现如内存泄漏、缓冲区溢出、指针非法引用等安全漏洞，这些安 全漏洞的存在极大地威胁着系统的稳定和安全。 本文工作源于“十五”预研课题“软件安全性故障模式分析”。该课题主要研究被 广泛应用的c c + + 程序设计语言的程序分析技术和面向不同领域的软件安全模式 构建技术，提供一组与安全分析相关的方法，并研制出一个基于静念分析的软件 系统安全检查工具。该工具可以检查出c c + + 程序中那些符合语法要求、但可能 导致程序错误的代码，从而在软件运行之前发现程序中潜在的错误，提高程序的 可靠性，避免不必要的损失。 针对c c + + 程序中可能存在的安全漏洞，国内外在对c c + + 程序的静态安全检 查领域进行了大量的探索，并已经实现了多种工具，其中相当一部分已经商业化。 现有的静态安全分析方法主要有模型检验 ，引、携带证据代码】、程序分析1 6 1 等。 模型检验是一种用来验证有限状态并发系统的形式化验证技术i lj 。它通过全面 搜索系统各种可能的行为来获取错误信息。由于通过算法自动进行，该方法具有 对用户要求不高、无需人为干与、可以提供反例等优点，得到了广泛应用，并己 成功应用到硬件设计和协议验证上。但该方法具有模型构造困难、属性规范难以 表示对软件行为属性的要求、状态空间爆炸及模型验证的结果难以阅读等缺点， 阻碍了将该方法成功应用于软件系统。 携带证据代码( p r o o f c a r r y i n gc o d e ，p c c ) 1 5 l 是一个证明可移动代码程序安全 特性的通用框架，它通过静态代码检测的方法保证代码不违背所规定的安全策略。 其基本思想是为程序代码事先定义一组安全策略，编写程序时遵守这些安全策略， 并在程序代码中加入形式证据以证明程序遵守了这些安全策略。由于该方法关注 的是代码被更改造成的安全问题，其使用范围受到限制，不能广泛应用于对软件 系统的安全检查中。 程序分析是目前主流的验证软件安全性的方法之一，包括基于词法分析【7 8 ，9 】、 语法和简单语义分析1o ，”】、以及信息流验证和检测1 1 2 , 1 3 】等安全检查方法。利用上述 检查方法的安全检查工具很多，如通过静态扫描c ，c + + 程序中对危险函数的使用 2 一种基于契约的安全分析方法的研究与实现 来检测安全漏洞的i t s 4 1 7 1 和r a t s l 9 1 ，通过向程序中加入注释信息的方式静态检查 标准c 语言安全性漏洞的s p l i n t i l 4 】等。随着软件的规模和复杂度越来越大，这种 方法已成为该领域研究的热点。 1 2 课题解决方案 本课题依据c c + + 安全漏洞的产生原因对c ，c + + 程序中易出现的安全漏洞进 行了分类“5 1 ，该分类较完整地覆盖了n a s a 安全报告 t 6 a 7 1 中的漏洞类别： ( 1 ) 存储越界和缓冲区溢出； ( 2 ) 资源泄漏； ( 3 ) 指针非法使用； ( 4 ) 使用危险函数； ( 5 ) 控制流及类型转换相关的安全漏洞； ( 6 ) 函数调用时实参或全局变量状态不合法； ( 7 ) c + + 类定义相关的安全漏洞； ( 8 ) c + + 异常处理相关的安全漏洞。 针对这些安全漏洞，本课题采用了程序分析技术结合语法制导翻译、自下而上 分析、基于契约的安全分析、构建全局类型系统、构建c c + + 编译器前端等方法， 实现了在词法、语法、静态语义级别上对c f c - h 程序的安全分析，研制了一个基 于静态程序分析的软件系统安全检测工具原型x d c h e c k 。该原型采用开放的 平台与技术，提供实用的、可扩充且可定制的安全规则，其安全检查部分由七大 模块组成：缓冲区边界检查模块、资源泄漏检查模块、指针合法性检查模块、异 常安全检查模块、与类型转换和控制流相关的安全模块、c + + 类定义合法性检查模 块、危险函数检查模块等，能够检测出c c + + 源程序中典型的、出现频度高的、 且危害性大的安全性问题。 第一章绪论3 x d c h e c k 的整体程序框架如图1 1 所示： l 源代码列表 契约关 系定义 x d c h e c k 前端 源代码项目分析模块 g c c 编译器卜 m a k e 程序l危险函数检查 编译后得到的a s g 圆 l 契约关 l 系表 函数依赖关系 分析器 - r 孺 i 酗j a s g 程序安全分析器 缓冲区边界检查摸块 指针合法性检查模块 资源泄漏检查模块 控制流安全性检查模块 类定义合法性检查模块 异常安全性检查模块 错误报告管理模块 最终的错误报告 图i ix d c h e c k 程序框架 如图1 1 所示，x d c h e c k 由前端和后端两部分组成。 前端程序负责调用g c c ( g u nc o m p i l e rc o l l e c t i o n s ) 编译器和m a k e 工具对输入 的源代码进行处理并获取中间表示。在获得中间表示之后，调用后端执行实际安 全分析。 后端程序负责实际的安全检查操作，主要分为如下五个模块： ( 1 ) 安全规则与契约分析模块：负责分析安全检查程序内建和程序员通过外部 输入的契约信息，并根据该信息构造安全模式的内部表示。该安全规则在后续的 安全分析中被使用： ( 2 1 符号表信息收集提取模块：负责遍历所有的程序中间表示，从中抽取程序 中的符号表信息，以供后续的安全分析使用； 4 一种基于契约的安全分析方法的研究与实现 ( 3 ) 函数调用关系分析模块：负责分析并处理整个项目中所有函数的调用依赖 关系，并根据该依赖关系确定后续安全检查过程中各个函数的分析顺序； ( 4 ) 程序安全分析器模块：负责遍历每一个中间语法树，根据符号表信息和安 全规则在遍历过程中执行安全检查。该模块是x d c h e c k 安全检查功能的主体部 分，其内部包含六个子模块，分别对各类程序安全漏洞执行安全检查； ( 5 ) 错误报告管理模块：负责接收安全检查器分析过程中得到的错误信息，并 根据程序员制定的格式将错误信息整理为错误报告并输出。 1 3 本文主要工作 针对上节c c + + 程序中易出现的安全漏洞分类中的资源泄漏、指针非法使用， 及函数调用时实参或全局变量状态不合法等安全漏洞，提出并实现了一种基于契 约的安全分析方法，使得在程序分析过程中可以使用此方法方便地进行安全分析， 检查出c c 十+ 程序中潜在的上述安全漏洞。 主要设计思想是； ( 1 ) 提供安全规则描述方法，使得x d c h e c k 支持可扩展安全规则定义，实现 课题解决方案中的安全规则与契约分析模块； ( 2 ) 使用自下而上分析方法，将跨过程安全分析转变为过程内安全分析； ( 3 ) 通过为变量和函数附加契约以记录其前置和后置条件，并在程序分析过程 中根据规则更新契约并进行安全判定，使得在程序分析过程中自动进行安 全分析。 主要工作包括： ( 1 ) 提出了自下而上分析方法中契约的相关概念，由函数调用对上下文环境产 生的影响引出了变量契约和函数契约的定义，为了支持可扩展可定制的安 全规则而提出了契约信息的定义。本部分在第二章阐述。 ( 2 ) 提出了基于契约的安全分析的核心思想，制定了安全判定规则、契约更新 规则，并在此基础上设计了基于契约的安全分析的核心算法。本部分在第 三章阐述。 ( 3 ) 在( 2 ) 的基础上，设计了基于契约的安全分析方法的程序框架。并实现了该 框架中的主要模块，包括配置文件格式的设计、契约信息的提取、前后置 条件的状态保存方法，契约结构的设计、契约安全规则和更新规则的实现 等。本部分在第四章阐述。 ( 4 ) 通过分析含有安全漏洞的程序实例，验证了此方法的正确性。本部分在第 五章阐述。 第二章自下而上分析方法中的契约5 第二章自下而上分析方法中的契约 x d c h e c k 使用自下而上分析方法，将对程序的跨过程分析转变为过程内分 析，在此基础上，本章定义了变量契约、函数契约和契约信息等概念，为后续章 节论述契约规则及基于契约的安全分析方法作好准备。 2 1 自下而上分析 定义2 1 函数依赖 设a 、b 均为函数，若在a 的函数体中调用了b ，则称爿依赖于b ，记为b 嗍。 定义2 2 函数依赖关系图 若将任意函数依赖b - ) a 中的一、b 表示为结点，“9 ”表示为从b 到a 的有向 边，则对任意程序p ，其所有函数的函数调用依赖关系可以表示为一个有向图，称 为p 的函数依赖关系图。 任何程序p 的函数依赖关系图为一个有向图，若图中存在环，则首先解环，所 得结果必为一有向无环图。对该图进行拓扑排序，沿所确定的次序分析各函数可 以保证：对任意函数依赖b - ) a ，b 必定先于4 被分析。 使用自下而上分析方法，对程序p 的函数依赖关系图中任意函数依赖b - ) a ， 若在分析b 后，分析结果能够确定4 调用口后对a 的上下文环境造成的影响，则 分析a 时就不需要展开b 进行分析，从而将对a 调用b 的跨过程分析转变为对a 、 口函数体单独的过程内分析，使得对p 的跨过程分析转变为过程内分析，与传统 方法【1 8 ，1 9 】相比较，该方法具有速度快、代价小的特点。 自下而上分析方法可分析完整或部分的程序代码，也可以分析没有单独程序入 口的程序( 如各种库函数等) ，使程序分析具备了一定的灵活性。 2 2 变量契约与函数契约 在安全检查中，被调函数曰对主调函数4 上下文环境的影响包括两个部分： ( 1 ) a 在调用b 之前，为保证b 能够安全执行所应满足的上下文环境。该条件 决定了函数调用是否安全。 ( 2 ) a 在调用b 之后，曰对a 的上下文环境的影响。该条件使得a 调用b 后的 6 种基于契约的安全分析方法的研究与实现 结果能够用于指导随后的分析。 为了明确表述被调函数对主调函数上下文环境的影响，本文用“契约”来描述 函数的上下文环境信息。契约包含两类：变量契约与函数契约。 定义2 3 变量契约 从函数f 的入口开始分柝，为使到语句s 前所有对变量v 的操作均安全，v 必 须满足的状态集合称为v 在s 处的前置条件；分析完语句s 后v 的状态集合称为 v 在s 处的后置条件。 变量v 在语句s 处的前置和后置条件( 以下简称前后置条件) 称为y 在s 处 的变量契约。 一 对于变量y 的变量契约zv 的前置条件记为p r e ( x ) ，后置条件记为p o s t ( x ) 。 定义2 ，4 函数契约 对所有调用函数f 的函数，为使调用f 安全，调用前所使用的全局变量、参 数必须满足的状态集合称为f 的前置条件，调用后主调函数中的全局变量、参数 及f 的返回值的状态集合称为f 的后置条件。 f 的前后置条件称为f 的函数契约。 一 函数，的前置条件是对主调函数在调用f 前的上下文环境的要求，后置条件 是调用完f 后f 对主调函数的上下文环境的影响。 若用变量契约来描述函数的前后置条件，则函数契约可表述为：与函数过程内 分析相关的全局变量、参数和返回值的变量契约的集合。函数的返回值契约只有 后置条件，对任意函数f 的函数契约c ，其返回值后置条件记为p o s t ( c ) 。 变量契约有两个作用，一是在程序分析的过程中记录并不断更新变量的前后置 条件，二是根据变量的当前状态和下一操作对此变量产生的前置条件进行安全检 查。 函数契约也有两个作用，一是利用过程内分析获得函数契约，保存分析结果， 二是在过程内分析中遇到函数调用时查找调用函数的契约来进行安全检查和契约 更新。 2 3 契约信息 为了支持可扩展安全规则，将所有与安全类型相关的信息提取出来，形成了契 约信息的概念。 定义2 5 契约信息 契约信息是与安全相关类型的状态信息和相关的库函数契约集合，它包含四部 第二章自下而上分析方法中的契约7 分：原子状态集合、互斥状态集合、资源状态集合和相关库函数契约集合。 契约信息决定每个变量契约中的前后置条件的取值范围。对于任何一个类型n 设所对应的契约信息为q ，则： q 中的原子状态集合规定r 类型变量所有可能状态。任意r 类型变量的前后置 条件为原子状态或原子状态的与( ) 、或( ij ) 、非( ，) 操作的结果。 q 中的互斥状态集合规定r 类型变量不能够同时拥有的原子状态对。任意丁类 型变量的前后置条件中的与操作( ) 的操作对象不能为互斥状态对。 q 中的资源状态集合规定r 类型变量在不存在别名的情况下，被重新赋值或变 量出作用域范围( 以下称为变量失效) 前不应具备的状态，若存在此状态，则表 示发生了资源泄漏。 q 中的相关库函数契约集合规定与f 类型相关的库函数的函数契约集合。 系统默认的契约信息包括普通指针和文件指针类型的契约信息，将这些契约信 息以一定的格式保存至配置文件，使得用户可以根据安全检查的需要以指定的格 式添加任何类型的契约信息，从而实现安全规则的定制与扩充。 第三章基于契约的安全分析方法的设计 9 第三章基于契约的安全分析方法的设计 在契约信息的基础上，安全分析实质上转换为根据程序语义设计相应的契约安 全规则和契约更新规则。契约安全规则用于对源程序进行安全检查，以找出潜在 的安全漏洞；契约更新规则用于对契约进行实时更新，以记录安全信息。 3 1 安全判定规则 在程序分析中，要使当前分析的下一语句执行安全，则应使下一语句中所使用 到的变量的当前契约的后置条件满足下一语句对该变量的要求，郎满足它对此变 量所产生的契约的前置祭件，若能满足这一条件，则认为是安全的，否则存在安 全隐患。 规则3 1 变量契约的安全规则 设变量v 的当前契约为咒下一语句s 对v 产生契约n 若对任意元素s p o s t ( y ) ，均有sc p r e 矽，即若在v 的当前状态集合中，每一个元素均在下一操作 允许的状态集合内，则s 是安全的，否则是不安全的。 规则3 1 用于在程序分析过程中进行单个变量的安全检查。若一个操作同时对 多个变量产生变量契约，则需要重复运用规则3 1 对每个变量契约进行安全检查。 在变量失效前，需要判定其是否可能导致资源泄漏。 规则3 2 变量失效前的安全规则 设变量v 的当前契约为咒且下一语句将导致变量v 失效，则： ( 1 ) 若v 存在别名，则v 失效后不产生安全漏洞； ( 2 ) 否则，对任意状态s 矿( 其中为v 所对应的契约信息q 的资源状态集 合) ，若有s p o s t ( x ) ，则v 失效时存在安全漏洞。 函数调用时，需要判定被调用函数的执行是否安全。由于采用包下雨上分析， 可以保证在函数调用时，被调用函数或者已经先被分析，或者为库函数，因此它 们已经获取了函数契约，从而将安全判定转换为判定在被调用函数中所使用的变 量( 包括全局变量和参数) 是否符合该函数契约的前置条件，及若被调用函数的 返回值契约的后置条件中包含了资源状态，主调函数是否保存了该资源。根据这 两点，制定安全规则3 3 ： l o 一种基于契约的安全分析方法的研究与实现 规则3 3 函数调用时的安全规则 设a 、b 为函数，且有函数依赖b 蝴，a 在语句s 处调用b ，a 在语句s 处的 全局变量契约集合为g ，实参契约集合为p ，判定a 调用b 是否安全的规则如下： 对任意变量契约x g 或x p ，设在曰中对应的变量契约为y ，若兄y 满足 规则3 。l ，则丑对此变量的使用是安全的，否则是不安全的。 若b 的函数契约含有返回值契约，且该返回值契约不存在别名且后置条件中包 含资源状态，则a 必须接收_ 8 的返回值契约并加入到a 的变量契约集合中，否则 是不安全的。 3 2 契约更新规则 使用安全规则进行安全检查后，必须更新契约以记录分析完下一条语句后变量 的前后置条件。契约更新的基本原则有二： ( 1 ) 覆盖程序中的所有结构( 顺序、分支、循环) ，根据各程序结构语义的不同 制定对应的更新规则； ( 2 ) 记录程序中各变量所有可能的状态，使得在安全判定时能够检测出所有潜 在的安全漏洞。 对于顺序结构，由于自下而上分析无法确定函数参数和全局变量的初始状态， 故使用i sd e 丁e r 膨f d e 0 来表示变量契约c 所包含状态的确定性，若能确定则置 为t r u e ，若不能确定( 如全局变量或函数参数) 则置为f a s l e 。契约更新依据当 前契约和下一语句所产生契约的确定性而定。 规则3 4 顺序结构变量契约的更新规则 对顺序语句s ： s l ；s 2 j 并u 其中的变量”若分析田后矿的契约为z 韶对v 产 生变量契约y 则s 对v 产生的变量契约z 的前后置条件为： p r e ( z ) j = i f i s _ _ d e t e r m i n e d ( x ) = t r u et h e np r e ( x ) e l s ep r e ( x ) & & p r e ( y ) p o s t ( z ) j = i f i s _ d e t e r m i n e d ( y ) = 豫晒t h e np o s t ( y ) e l s ep o s t ( x ) i l p o s t ( ” 在规则3 4 中，若岱d e t e r m i n e d ( x ) 为f a l s e ，则说明不能确定x 的前置条 件，下一语句对v 所产生的前置条件将进一步限制在执行s 前v 的当前状态所允 许的范围，从而其结果为j 与】，的前置条件的交集，即p r e ( x ) & & p r e ( y ) ；而若 i sd e t e r m i n e d ( y ) 为f a l s e ，则说明】，的后置条件只是可能的，是不确定的，从 而其结果为x 与】，的后置条件的并集，即p o s t ( x ) | | p o s t 御。 对于分支结构，要保证程序的安全，则变量在分支结构执行前的状态应该满足 所有分支对该变量的状态要求，即前置条件为所有分支对该变量产生的前置条条 第三章基于契约的安全分析方法的设计 件的与集，由于每一个分支结构均有可能被执行，且不可能同时被执行，故其后 置条件为所有分支对该变量产生的后置条件的并集。 规则3 5 分支结构变量契约的更新规则 对分支语句矿- 一j 肼e l s e 盟和其中的变量v ，若剐对v 产生契约x ，髓对 y 产生契约y 则s 对y 产生的契约z 的前后置条件为： p r e ( z ) ：= p 心c 玛p r e ( 1 9 p o s t ( z ) j 2p o s t ( x ) p o s t ( y ) 对于循环结构，变量的前后置条件与在循环体中对该变量产生的前后置条件一 致。 规则3 6 循环结构变量契约的更新规则 对循环语匈& w h i l e ( 一，s t 和其中的变量儿若鲥对矿产生契约墨则s 对v 产生的契约y 的前后置条件为： p r e ( j f ) ：= p r e ( x ) p o s t ( y ) j = p o s t ( x ) 一 由于函数契约由变量契约组成，故在函数调用时的契约更新即对相关的变量契 约的更新，具体实现参见规则3 7 ： 规则3 7 函数调用时契约的更新规则 设a 、b 均为函数，且存在函数依赖b - k a ，若a 中调用b 的语句为s ，则分析 s 后契约应做如下更新： ( 1 ) 对任意属于b 的全局变量契约集合中的元素y ，若在a 的函数契约中有对 应的全局变量契约咒则按照规则3 4 更新j 的契约；否则将】，加入到 的全局变量契约集合中。 ( 2 ) 对任意属于b 的参数变量契约集合中的元素，在a 中必定有对应的实参 变量契约肘，按照规则3 4 更新m 的契约。 在分析返回语句时，需要更新其所在函数的函数契约，与分支结构中契约更新 类似，由于返回语句的互斥性( 返回语句的执行总是使德函数返回，从而在一次 调用中不可能执行两个返回语句) ，故将函数契约的返回值契约更新为其与返回语 句产生的变量契约这二者的后置条件的并集。 规则3 8 函数返回时契约的更新规则 设函数f 的函数契约为c ，返回语句为返回值的变量契约为j 厂，则分析s 后f 的返回值契约的后置条件为： p o s t ( c ) j = p o s t ( c ) | ip o s t ( x ) 1 2 一种基于契约的安全分析方法的研究与实现 在规则3 8 中，若在分析语句s 前c 中不存在返回值契约，即p d s f 幻为空集 合，此时为p o s t ( c ) ? = 毋l | p o s t ( x ) ，可简化为p o s t ( c ) j = p o s t ( x ) 。 3 3 基于契约的安全分析算法 基于契约的程序安全分析由两个关键算法组成：过程内安全分析算法与程序安 全分析算法。两个算法均依赖于契约信息库。 过程内安全分析算法对一个确定的函数，首先为f 及f 中的全局变量和参数 附加初始契约，然后依次分析函数体中的每一条语句，根据语句类型选择适应的 规则进行安全检查和契约更新，完成该函数体的安全分析并获得函数契约。 算法3 1 过程内安全分析 输入：函数f 的函数体 输出：f 的函数契约c 方法： 初始化函数契约c ； f o rf 中的每一条语句s ，根据语句类型进行下述处理之一： 变量声明语句：初始化变量的契约； 返回语句：使用规则3 8 更新契约c ； 函数调用语句：使用规则3 3 和规则3 7 检查和更新契约c ； 赋值语句：使用规则3 2 和规则3 4 检查和更新契约c ； 退出作用域语句：使用规则3 2 检查契约c ： 其他任何情况：使用规则3 1 、3 4 、3 5 、3 6 检查和更新契约； 若所有语句均分析完毕则退出f o r 循环，否则继续； e n d f o r 一 程序安全分析以函数调用依赖图为基础，针对完整的程序p 中所有函数进行过 程内分析，最终得到分析结果。 算法3 2 程序安全分析 输入：程序户 输出：程序p 的安全分析结果 方法： 读取配置文件并构建契约信息库； 构建函数调用依赖关系图； i f 函数调用依赖关系图中存在环 第三章基于契约的安全分析方法的设计 1 3 对函数调用依赖关系图进行解环； e n d i f 对函数依赖关系图进行拓扑排序； f o r 排序后的每一个函数凡 使用算法3 1 对f 的函数体进行过程内安全分析； e n d f o r 对函数调用依赖图进行解环操作后，可保证按照拓扑排序结果进行的过程内安 全分析不会在函数体内再对其他函数进行展开分析，从而将跨过程分析转化为过 程内分析。在此操作后，依次使用算法3 1 对排序后的每一个函数的函数其进行过 程内分析，即完成对整个程序的安全分析并给出其安全分析结果。 本章在契约及契约信息的基础上，设计了安全判定规则及契约更新规则，然后 根据这些规则设计了基于契约的安全分析算法。这些规则和算法是实现基于契约 的安全分析方法的基础。 第四章基于契约的安全分析方法的实现 1 5 第四章基于契约的安全分析方法的实现 针对a c + + 程序中易出现的资源泄漏、指针非法使用，及函数调用时实参或全 局变量状态不合法等安全漏洞，本文提出了一种统一的检测方法，即基于契约的 安全分析方法。在本章论述了该方法的具体实现，首先设计了一个合理的程序框 架，然后详细阐述了在程序框架中每一模块的作用及具体实现，从而达到检测安 全漏洞的功能。 4 1 程序框架 基于契约的安全分析方法由以下几个核心模块组成：配置文件格式定义模块、 契约信息模块、前后置条件状态保存模块、契约结构定义模块、契约规则模块、 以及安全分析模块。程序框架如图4 1 所示： 安全分析模块 l 基于契约的安全分析 i l卜 契约规则模块 l 契约更新规则 ll 契约安全规则 l 。 契约结构定义模块 = 令变量契约卜_ + | 函数契约i t ， 状态二重集合 t 提取 前后置条件的l j l 状态条件析取范式语法树l 状态保存模块r t 转换 状态条件表达式语法树 t 解析 状态条件表达式 t 蓦：盘、非 ll 卜 l契约信息模块b ；原子状态l 互斥状态i资源状态ll 安全规则l i 卜。f 解卜f 配耄定义模块r _ 一 配置文件 l 图4 1 基于契约的安全分析方法的程序框架 1 6 一种基于契约的安全分析方法的研究与实现 各模块的功能如下： ( 1 ) 配置文件格式定义模块：定义了配置文件的格式，为添加系统默认和用户 自定义的契约信息提供途径： ( 2 ) 契约信息模块：通过解析配置文件，获取在配置文件中定义的原子状态、 互斥状态、资源状态、安全规则的详细信息，此模块是前后黄条件状态保 存模块、及安全判定和契约更新的基础； ( 3 ) 前后置条件的状态保存模块：使用为状态引入与或非逻辑的状态条件表达 式作为基本的状态保存方法，通过解析表达式建立起状态条件语法树，然 后转换为析取范式状态条件语法树，最终提取出状态二重集合并进行优 化，为安全分析提供支持： ( 4 ) 契约结构定义模块：定义了变量契约和函数契约的数据结构，这是契约规 则模块的基础； ( 5 ) 契约规则模块：使用当前分析程序中的函数契约和变量契约，结合契约信 息中的资源状态集合及安全规则，按照设计的思想实现了具体的契约更新 规则和契约安全判定规则； ( 6 ) 安全分析模块：给出使用契约规则模块中的算法及其它算法进行安全分析 的核心算法。 在本章以下各节中详细阐述每一个模块的具体实现方法。 4 2 配置文件格式定义模块 早期的程序安全检查工具往往选择将程序的安全规则全部内建于安全检查器 内部。这种检查方法在检查简单的程序代码时可以得到较好的效果，但是在检查 实际项目的程序代码时效果较差。这主要是由于安全分析器内建的安全规则通常 较为有限，往往只能够对c c + + 语言本身和标准库中各种可能出现的安全漏洞进 行建模。但是在实际项目开发过程中的c ，c + + 代码往往需要大量依赖于各种外部 函数库，安全检查器不可能对市场上所有的c c 什外部函数库中所有可能出现的 危险函数进行安全规则建模。这就使得传统静态安全检查器无法适应各种具体项 目开发的要求。 为了解决这一问题，现代静态安全检查器往往提供某种扩展机制，允许程序员 根据实际项目需要自行扩充安全规则。此类安全分析器的典型代表是商业产品 c o d e c h e c k l 2 0 和开放源代码工具u n o f ”】等。上述两种工具均支持一种语法类似 于c 语言的脚本语言，并且通过该语言编写的脚本来定义任意的安全检查规则。 理论上，只要程序员能够编写出正确的安全规则描述脚本，就可以利用此类工具 实现任意复杂的程序安全检查逻辑。但是过分复杂的脚本规则定义会加大安全检 第四章基于契约的安全分析方法的实现1 7 查工具的学习难度。例如s c o t t m a y e r s 在其对9 个c c + + 静态安全检查工具的评测 报告田】中营经指出，c o d e c h e c k 工具的安全规则定义语言需要程序员学习3 到 6 个月才能熟练掌握。另外，解析复杂的安全规则定义语言也加大了安全分析器的 开发难度。 本方法将安全规则写入配置文件，可以实现安全规则的任意定制和扩充，同时， 为了方便程序员能够快速掌握添加安全规则的方法并应用于实践，采用x m l l 2 3 1 语言来描述安全规则。 4 2 1 配置文件格式定义 在本方法中，安全规则是指在发生函数调用时，上下文环境必须满足的条件， 以及此函数调用对上下文环境造成的影响，即被调用函数的函数契约。 通过在配置文件中规定程序中使用的库函数的函数契约，从而能够在调用库函 数时根据上下文环境判定函数调用是否安全，并更新当前所分析函数的函数契约 及相关的变量契约。 x d c h e c k 采用x m ld t d 2 4 1 来描述配置文件的格式，相对于传统单独设计语 言去描述安全规则的方法，有以下优点： ( 1 ) 格式明确，通用，安全规则易被用户理解； ( 2 ) 结合d t d 定义，用户可以快速学习掌握并应用于对程序的安全检查之中， 此方法不需要用户再去学习专门的程序设计语言，只需了解x m l 的基本 知识即可； ( 3 ) 解析方便，有技术成熟的解析器开发库可供使用，不需要开发专门的编译 器，降低了开发难度。 综合考虑为实现定制安全规则所需要的信息，包括必须的原子状态集合、互斥 状态集合、用于在变量失效前判定是否存在资源泄漏而设定的资源状态集合、以 及函数原型、函数契约等信息，设计配置文件的格式如表4 1 所示( 篇幅所限略去 所有注释，详细内容参见附录。 1 8 一种基于契约的安全分析方法的研究与实现 4 2 2 系统默认契约信息 x d c h e c k 默认提供普通指针和文件指针的契约信息，用户可以根据所检查项 目的需要添加任意类型的契约信息。 对于普通指针，采用一个抽象的类型名称“”来表示，当某一变量类型为指 第四章基于契约的安全分析方法的实现1 9 针，且不存在对应该指针的契约信息时，则使用普通指针的契约信息。 使用表4 1 所设计的配置文件格式来描述普通指针的安全规则的配置文件片断 如表4 2 所示( 系统默认契约信息的详细内容请参见附录b ) ： 2 0 一种基于契约的安全分析方法的研究与实现 4 3 契约信息模块 本模块完成契约信息结构的定义及从配置文件中提取出系统默认及用户自定 义契约信息的工作，后续的前后置条件的状态保存模块、契约规则模块均以此模 块所提取出的契约信息库为基础。 4 3 1 契约信息的定义 契约信息用来保存在配嚣文件中系统默认及用户自定义的安全规则等信息，它 是后续模块的基础。其定义主要包含四部分：原子状态集合、互斥状态集合、资 源状态集合、安全规则( 即函数契约) 集合。 定义契约信息的结构如下： s t r u c tc o n t r a c t l n f o g e n e r i e t y p e i n f o + t i n f o ； + 该契约信息所对应的类型+ g s l i s t * s t a t u sl i s t ； 严原子状态链表+ ， g s l i s t + e x c l u s i v e _ s t a t u sp a i r _ l i s t ； 严互斥状态对链表+ g s l i s t * r e s o u r c es t a t u s ，西f ： 严资源状态链表+ g s l i s t * f u n c t i o n产安全规则链表，_ c o n t a c tl i s t ； 元素类型为f t m c t i o n c o n t r a c t * + ) ； 其中g e n e r i c t y p e l n f o 为x d c h e c k 中记录c c + + 程序中类型的信息的结构体 类型，g s l i s t 为g l i b 2 5 l 中定义的单链表结构体类型，f t m c i o n t c o n t r a c t 为函数契约 结构体类型，其具体定义参见4 5 2 节。 该契约信息结构体的定义完整地描述了配置文件中各项的信息，并保留了与变 量类型的对应关系。 4 3 2 契约信息的提取 本小节首先介绍x m l 解析器开发库e x p a t 2 6 1 ，然后给出使用e x p a t 编写解析 器对配置文件进行解析，从而提取出契约信息的具体实现。 4 3 2 1e x p a t 介绍 e x p a t 是一个由j a m e sc l a r k 使用c 语言开发的面向流的非验证性的x m l 解析 第四章基于契约的安全分析方法的实现2 1 器开发库。它已被许多开源项目所使用，包括m o z i l l a 、p e r l 、p y t h o n 和p h p 等。 要使用e x p a t ，应用程序需要首先使用e x p a t 所提供的接口声明处理函数，然 后启动e x p a t 解析器解析x m l 文件。在解析过程中，e x p a t 依据x m l 文件中节点 的类型来调用相应的处理函数。 e x p a t 提供了各种可由用户设置的句柄和选项，最重要的几个函数【2 q 如下： x m lp a r s e r c r e a t e ：创建一个新的x m l 解析器实例； x m ls e t e l e m e n t h a n d l e r ：为元素的起始和结束标记设置回调函数； x m ls e t c h a r a c t e r d a t a h a n d l e r ：为文本内容设置回调函数； x m lp a r s e ：使用创建的解析器进行x m l 文件的解析。 使用e x p a t 解析x m l 文件的过程【27 l 可以概述为： ( 1 ) 应用程序创建一个e x p a t 解析器： ( 2 ) 应用程序向所创建的解析器注册由e x p a t 规定了接口的各种回调函数( 句 柄) ，应用程序对x m l 文件中各节点的处理均由这些回调函数来完成； ( 3 ) 解析器读入x m l 文件，在读入过程中，每遇到x m l 文件中的一个节点， 解析器就去查找是否存在相应的回调函数，若存在，则调用之。 4 3 2 2 使用e x p a t 编写x m l 解析器提取契约信息 根据配置文件格式定义，使用e x p a t 编写x m l 解析器提取出所有在配置文件 中的契约信息，以供后继的安全分析使用。 在具体解析前，需进行一定的准备工作，其步骤如下： ( 1 ) 根据配置文件格式定义，设计保存x m l 文件各节点内容的中间数据结构； ( 设计处理x m l 文件中元素节点的起始和结束标记的回调函数； ( 3 ) 设计处理x m l 文件中文本节点的回调函数； 算法4 1 实现了使用e x p a t 编写x m l 解析器提取契约信息操作： 算法4 1 提取契约信息 输入：配置文件c o n t r a c t ：o n f i g x m l 输出：契约信息库 步骤： ( 1 ) 打开c o n t r a c t _ c o n f i g x m l 文件，若失败，则转1 2 ； ( 2 ) 使用x m l _ p a r s e r c r e a t e 创建e x p a t 解析器p a r s e r ； ( 3 ) 使用x m ls e t e l e m e n t h a n d l e r 向p a r s e r 注册处理元素节点的起始和结束标记的 回调函数； ( 4 ) 使用x m ls e t u s e r d a t a 向p a r s e r 注册中间数据结构； ( 5 ) 使用x m ls e t c h a r a c t e r d a t a h a n d l e r 向p a r s e r 注册处理文本节点的回调函数； 2 2 一种基于契约的安全分析方法的研究与实现 ( 6 ) 使用x m l p a r s e 解析c o n t r a c t c o n f i g x m 以获取中间数据结构内容，若失败， 则转1 2 ： ( 7 ) 将中间数据结构内容转换为契约信息保存： ( 8 ) 将契约信息添加到契约信息库中； ( 9 ) 使用x m lp a r s e r f r e e 释放p a r s e r ； ( 1 0 ) 释放中间数据结构内容所占用的内存空间； ( 1 1 ) 返回契约信息库，算法结束； ( 1 2 ) 解析失败，给出错误信息，算法结束。 一 4 4 前后置条件的状态保存模块 本文提出的基于契约的安全分析方法设计了一种统一的检测方法来检测 c c + 十程序中的资源泄漏、指针非法使用，及函数调用时实参或全局变量状态不合 法等安全漏洞。这种方法建立在对变量的前后置条件的状态的统一表示上。如何 有效的表示状态，是本节的内容。 由于程序逻辑的复杂性( 顺序、分支、循环及各种组合结构的出现) 及程序中 变量类型的多样性( 系统定义、用户自定义) ，简单的状态表示方法已不能适用于 实际软件代码的检查。为了能够如实地记录任意类型的变量在任意程序逻辑中的 状态，本文通过为状态引入与、或、非运算逻辑的状态条件表达式来记录状态的 方法，达到了这一目的。 本节阐述了使用状态条件表达式来记录状态的方法，其最终目的是为了提供等 价于状态条件表达式的状态二重集合( 具体定义见4 4 5 节) 。 状态二重集合具有以下特点： ( 1 ) 在一重集合的基础上增加了表示与、或逻辑的能力，使得可以表示任何程 序逻辑中任何类型的变量的状态。 ( 2 ) 状态二重集合之间的运算符合集合运算规则，有成熟的数学模型。 状态二重集合为保存变量契约的前后置条件的状态提供了便利，也使得安全分 析由针对前后置条件转化为针对状态二重集合来进行，从而可以使用统一