（计算机软件与理论专业论文）cc程序安全分析中契约的设计与实现.pdf

摘要 本文研究基于契约的安全分析方法。该方法通过对过程内的变量构造变量契 约、对跨过程的函数调用构造函数契约描述程序的状态，并按函数调用关系自下 而上获取相应的契约信息。在获取契约的基础上，使用相应的安全判定规则和更 新算法实现程序安全分析。 结合c ，c + + 语言的特点，本文设计和实现了针对c c + + 程序安全分析的契约 分析方法框架。根据c c + + 安全分析实际需求，给出了c c + + 指针变量前后置条 件的描述方法。同时结合契约分析原理，设计了指针变量契约的数据结构，并提 供一组算法，用于更新指针变量契约和对指针变量进行安全判定。 该框架具有一定的可扩展性，按需求继承相应的接口并实现对应的算法便可 以使契约分析方法支持对更多c c + + 类型变量的分析。 关键词：契约跨过程自下而上安全分析 a b s t r a c t ac o n t r a c t - b a s e dm e t h o df o rs a f e t y a n a l y s i si sp r e s e n t e di n t h i s p a p e r b y c o n s t r u c t i n g v a r i a b l ec o n t r a c t sf o rl o c a lv a r i a b l e sa n df u n c t i o n sc o n t r a c t sf o r i n t e r - p r o c e d u r ef u n c t i o nc a l l s ，t h i sm e t h o dk e e p sr e c o r d so ft h es t a t u so ft h ep r o g r a m t h r o u g ht h ea n a l y s i so ft h er e l a t i o n s h i pb e t w e e nf u n c t i o n s ，i to b t a i n sc o n t r a c t i n f o r m a t i o nb yb o t t o m - u po r d e r b a s e do nt h ec o n t r a c ti n f o r m a t i o n , t h i sm e t h o d i m p l e m e n t st h es a f e t yc h e c k i n gr u l e sa n dc o n t r a c t su p d a t i n ga l g o r i t h m s ，m a k i n gi t p o s s i b l et os u p p o r tt h ea n a l y s i so f p r a c f i c a lp r o g r a m s t a k i n gt h ec h a r a c t e r i s t i c so fc f c + + l a n g u a g ei n t oa c c o u n t t h i sp a p e rd e s i g n sa n d i m p l e m e n t st h e 吼m e w o r kf o rc ，c + + p r o g r a ms a f e t ya n a l y s i s b a s e do nt h e r e q u i r e m e n to fs a f e t ya n a l y s i s ，t h i sp a p e rd e s i g n e dt h ed e s c r i p t i o no fp r e - c o n d i t i o n sa n d p o s t - c o n d i t i o n sf o rp o i n t e rv a r i a b l e so fc ，c + + l a n g u a g ea n dt h ed a t as t r u c t m eo f p o i n t e rv a r i a b l ec o n t r a c t b yo f f e r i n ga s e to fa l g o r i t h m sf o ru p d a t i n ga n dc h e c k i n gt h e p o i n t e rv m i a b l ec o n t r a c t ，t h i si m p l e m e n t a t i o ns u p p o r t st h es a f e t ya n a l y s i sf o rp o i n t e r v a r i a b l e so f c c + + l a n g u a g e s b e c a u s eo ft h ee x p a n s i b i l i t yo ft h ef r a m e w o r k , s a f e t ya n a l y s i sf o ro t h e rt y p e so f c c + + v a r i a b l e si sp o s s i b l eb yi n h e r i t i n gt h ei n t e r f a c ea n di m p l e m e n t i n gi t sr e l a t e d a l g o r i t h m s k e y w o r d s ：c o n t r a c ti n t e r - p r o c e d u r eb o t t o m u pa n a l y s i s s a f e t ya n a l y s i s 创新性声明 本人声明所呈交的论文是我个人在导师的指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中 不包含其他人已经发表或撰写过的研究成果，也不包含为获得西安电子科技大学 或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究工 作所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 申请学位论文若有不实之处，本人承担一切相关责任。 本人签名：墨盘簦日期：丝! 生丛缒 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文：学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其他复制手段保存论文。( 保密的论文 在解密后遵守此规定) 本学位论文属于保密在 年解密后适用本授权书。 本人签名；墨生! 室日期：笙! 生幽! 旦 导师签名： 第一章绪论 第一章绪论 1 1 软件安全分析的现状 软件技术的不断发展，除了要求软件在效率和可用性上得到相应提高外，对 软件安全性也提出了更严格的要求。一些实时嵌入式软件，例如飞机的控制软件， 就必须符合一定的安全要求。一些涉及保密领域的软件，例如银行系统，也需要 对安全性有较高的要求。此外，在一些高尖科技和军事应用上，计算机软件的安 全性则是极其重要的一环。 作为被普遍使用的程序设计语言，c 口斗的安全性也不断受到人们的重视。由 于早期c 主要用于底层软件开发，其设计目标是更好的利用机器资源和提高效率， 而对安全性的考虑并不全面，缺少很多对软件安全性的支持。例如c 语言并没有 支持缓冲区越界的检查，也没有对指针的使用进行较好的限制。这些在软件安全 支持上的缺陷，导致使用c 语言进行程序设计时，可能存在安全问题。后来出现 的c + + 语言，由于继承了c 的大多数语法和语义，使得一些c 中的安全漏洞在c + + 仍然存在。虽然c - 卜 标准1 1 心引入新特性用于减少安全漏洞1 3 j 1 4 1 5 1 1 6 1 7 j ( 例如引入标 准模板类库，用模板类v e c t o r 和l i s t 等代替c 中的数组，解决数组越界问题；用模 板类a u t op t r ，帮助程序员自动管理动态分配的单个对象，解决内存动态分配相关 问题) ，但实际仍有很多c + + 程序没有使用这些新特性，而使相关的安全漏洞仍然 存在。 同时，由于c c + + 标准并不要求编译器【s 】对安全漏洞进行特定的检查，传统的 c c + + 编译器( 如开放源代码的g c c 和微软公司的v i s u a l c 什6 0 ) 只是完成语言 标准要求的工作，而将查找漏洞的任务交给程序员人工进行。人工进行安全检查， 在早期程序代码量较少、结构较为简单的时期，能够较好的找出程序中的安全漏 洞。但随着软件行业的发展，软件的功能越来越强大，伴之而来的是程序代码量 的剧增和程序结构的复杂化。这种情况下，人工查找程序中隐藏的安全漏洞显得 相当困难且代价很高。并且由于人工查找的成功率与程序员的经验和能力有关， 人工检查程序中的安全漏洞并不能很好的保证检查效果。针对人工检查c ，c h 程 序安全漏洞的缺陷，人们开始研究自动化检查工具，辅助程序安全分析 9 1 1 1o 】【1 ”。 l i n t 【1 2 1 系列的开放源代码检测工具，能检测出很大一类安全漏洞，而且也能够 有效地提出许多在空间利用、运行效率上的改进方法，但其检测方法相当有限， 且误报较多。该系列的最初版本l i n t ，检查条件比较宽，通常会检测程序的所有路 径而不考虑代码路径的可达性，然后报告可能存在安全问题。其采用的方法虽然 2c ，c + 十程序安全分析中契约的设计与实现 能有效检测过程内的安全漏洞，但在跨过程检查中存在严重的缺陷。l c l m t 1 3 】可 以看作是l i n t 的升级版，允许用户对源程序添加注解辅助安全分析，可以在l i n t 功能之外执行更进一步的检查。通过结合用户辅助定义信息，可以有效地缩小检 查范围，使检查结果更加准确。但由于需要用户修改源程序来添加辅助信息，该 检查方法降低了检测工具的自动化程度，增加程序员的工作量。并且为准确描述 用户需求，l c l i n t 定义了较为复杂的用户辅助信息描述方法，程序员需要学习如 何使用这种描述方法才能正确的使用该工具。而学习这些知识，往往需要相当长 的一段时间。 基于程序抽象表示的方法的工具c o v e r i t y “1 ，主要采用斯坦福大学d a w s o n e n g l e r 元编译m c ( m e t a - c o m p i l e ) 和模型检验【l5 】方法。模型检验是一种用来验证 有限状态并发系统的形式化验证技术。它通过全面搜索系统各种可能的行为来获 错误信息。由于通过算法自动进行，具有对用户要求不高、无需人为干与、可以 提供反例等优点而得到广泛应用，并己成功应用到硬件设计和协议验证上。目前 c o v e r i t y 用于检查开发源代码的l i n u x 内核和m o z i l l a 浏览器，并且越来越多的软 件正考虑采用c o v e r i t y 作为其安全检查工作。但由于模型检验方法具有模型构造 困难、属性规范难以表示对软件行为属性的要求、状态空间爆炸及模型验证的结 果难以阅读等缺点，该方法进一步应用将有待这些问题的解决。 添加类型信息的工具，如c c u r e d t l 6 1 1 m ，允许用户对特定类型添加限定信息【1 8 】， 使c 中的类型更精确，然后制定一系列的推导过程来验证程序的安全性。这种方 法同样需要程序员的交互，降低检测的自动化程度，并且制定完整的类型推导规 则相当困难。现在使用这种方法的工具处于实验阶段。 基于契约的跨过程安全分析方法【1 9 1 ，由西安电子科技大学软件工程所提出。 其核心思想为：将安全检测所需要的上下文信息用前后置条件保存，并通过制定 相应的规则来进行检测。其不需要用户在源程序中添加辅助信息，适合程序的自 动化分析，且支持过程内和跨过程检查。 1 2 研究背景 本文选题源于实际研究项目：c ，c + + 静态安全检查工具的设计与实现。该工具 设计用于分析和检查c c + + 源程序，从中查找源程序中的安全漏洞。该工具的设 计框架如下图： 第一章绪论3 图1 1c c + + 静态安全检查工具整体框架 工具分为前端和后端两部分。其中前端1 2 0 1 是后端分析和设计的基础，主要包 括源代码的语法分析、配置管理，控制流图的生成等。前端通过对项目源代码进 行分析，为后端收集分析需要的符号信息、抽象语法树和控制流信息。各部分功 能如下： 1 1语法分析：通过对源程序进行语法分析，收集程序的符号信息，包括类 型信息，变量信息和函数信息。同时生成以函数为单位的抽象语法树； 配置管理：对工具需要的参数进行配置，例如用户根据被分析项目的规 模配置符号表的参数，根据被分析项目源代码针对的环境，对基本类型的参 数进行配置； 3 )控制流图生成：通过遍历抽象语法树，生成携带抽象语法树的控制流图， 作为后端分析的基础。 工具后端主要是以数据流分析为主的安全检查的实现部分，主要包括以下几 个部分： 函数依赖分析【2 1 1 ：通过对工具前端生成的控制流图以及a s t 进行遍历， 辅以函数指针数据流分析，获取精确的函数调用依赖关系。根据该依赖关系 产生函数调用的拓扑序列，以此确定后续分析模块和安全检查的函数次序； 4 c ，c h 程序安全分析中契约的设计与实现 5 )指针别名分析口2 】【打1 ：基于程序分析器前端生成的抽象语法树a s t 和控 制流图c f g 以及函数依赖分析生成的函数调用拓扑序列，采用自顶向下的分 析方法，记录跨过程和过程内的指针别名信息记录的指针别名信息，供后续 的跨过程安全检查使用： 6 )契约配置管理和契约引擎的设计和实现：制定检查所需要用到的规则和 方法，设计和实现程序分析和安全检查模式所需的存储结构和算法，为后续 安全检查提供必要的信息； 7 )指针引用的有效性和资源泄漏检查 2 4 1 ：前者是以函数调用的拓扑排序为 输入，以契约机制为引擎的基于控制流图的数据流分析和安全检查实现的主 体；后者负责接受安全分析系统在分析过程中得到的错误信息，并整理成错 误报告以支持多种模式下的错误信息输出机制。 1 。3 论文的工作及组织 在项目的开发过程中，本文主要负责契约配置管理和契约引擎的设计和实现， 主要工作包括： ( 1 ) 研究契约安全分析方法。 ( 2 ) 管理契约配置信息和设计安全规则描述方法，设计和实现契约相关类型。 ( 3 ) 实现契约的安全判定规则和更新算法。 论文的主要内容安排如下： ( 1 ) 第一章论述安全分析工具和方法的发展情况和研究背景，并介绍论文所 基于的项目的总体框架； ( 2 ) 第二章论述契约分析方法的基本概念。主要论述契约的基本原理、契约 的更新和判定规则，最后描述使用契约进行的过程内和跨过程安全分析 方法及其在c c + + 安全分析中的应用； ( 3 ) 第三章主要论述契约分析方法的设计与实现，主要包括契约配置信息的 定义与获取，契约定义、更新算法和判定规则的实现；然后用两个实际的 例子验证其的正确性。 第二章契约安全分析方法概述5 第二章契约安全分析方法概述 2 1 契约的概述 对一个软件系统的源程序进行安全分析，需要对该系统建模，通过建立好的 模型指导程序分析。在契约分析方法中，主要是对过程内变量和跨过程函数调用 建模。 过程内的变量模型主要包括两个方面：一是变量状态的描述：二是基于变量 状态的检查方法。通过利用变量的状态和基于状态的检查方法，可以有效地判定 变量使用的正确性。跨过程的函数模型，主要考虑发生函数调用时，调用函数与 被调用函数之间的相互影响，核心思想是将被调用函数对调用函数的影响转化为 被调用函数对参数、全局变量和返回值的影响，从而将跨过程函数调用的安全判 定转化为过程内的变量使用安全判定。变量模型主要由变量契约具体描述，函数 模型用函数契约描述。 2 1 i 变量契约 变量契约由变量的前置条件和后置条件组成，它们分别用于记录安全使用变 量时变量所需要达到的状态和变量被使用后所达到的状态。通过建立变量契约， 可以把对于变量的安全检查转化为基于变量状态的检查。变量契约相关定义如下： 定义2 1 前置条件 设在语句s 中变量v 的契约为x ，为保证v 的安全使用，v 所要达到的状态， 称为v 在语句s 中的前置条件，记为p r o ( x ) 。 定义2 2 后置条件 设在语句s 中变量v 的契约为x ，语句s 执行后，v 达到的状态称为v 在语 句s 中的后置条件，记为p o s t ( x ) 。 定义2 3 变量契约 变量在语句s 中的契约由其在s 中的前置条件和后置条件组成。 下面举一个例子说明变量契约： 在语句f r e e ( v a t ) 中的指针变量v a t ，为了保证f r e e 能正确执行，v a t 的状态必须 为“指向空或指向c 的堆空间”；语句执行后，v a t 的状态变为“指向的空间已释 放”。根据本节的定义，变量v a t 在本语句中的前置条件为 b 就表明对a 的分析必须依赖于对b 的分析。在进行契约 的获取时，必须先获取到函数b 的契约，然后才能对函数a 进行正确的分析。 因此，函数契约的获取必须按照函数的调用关系自下而上进行。首先分析函 数的调用关系，按调用关系进行排序，然后根据函数调用关系自下而上进行分析。 基于自下而上的分析方法，只需要对所有的函数进行一次分析，便可以得到每个 函数的契约信息。 例如，一个c c + + 源程序经分析后得到其函数调用序列为a - b - c 。在进行 契约获取时，须先对函数c 进行分析，获取其契约信息；然后对b 进行分析，由 第二章契约安全分析方法概述7 于在分析b 之前c 的契约已经被获取，则b 的契约最终也能被获取；最后分析a 函数契约，从而完成整个源程序的契约获取。 2 2 2 契约的更新 要使契约能正确反映当前所分析程序的上下文，必须在进行安全分析的同时 对契约进行更新。比如语句a 对于变量p a r 的前置条件为x ，后置条件为y ，则 在完成语句a 的分析后，必需根据一定的规则对变量p a r 的契约进行更新。 在制定契约的更新规则时，需要考虑程序语句的所有可能结构，以达到对程 序进行全面的分析。下面分4 种情况对契约的更新规则进行描述： 【1 】顺序结构的契约更新 顺序结构的契约更新，主要考虑顺序相邻两个语句对契约的影响。在进行顺 序结构的契约更新前，先要确定变量契约的确定性，然后结合变量契约的确定性 制定顺序结构的契约更新规则。一个变量契约的确定性，分为以下两种： ( 1 ) 已确定。表示在分析中，变量契约已经确定。例如声明并初始化了一个指 针变量，那么这个变量契约既为己确定。 ( 2 ) 未确定。表示在分析中，变量契约未可确定。例如刚开始分析一个函数时， 由于采用自下而上的分析，其参数契约的状态为未确定。 下面用i s d e t e r m i n e d ( c ) 表示变量契约c 的确定性。 i s d e t e r m i n e d ( c ) = t r u e 代表契约已确定； i s d e t e r m i n e d ( c ) = f a l s e 代表契约未确定。 结合变量契约的确定性，制定契约的顺序更新规则如下： 规则2 1 顺序语句更新 对顺序语句s ： s 1 ；s 2 和变量v ，假设s 1 对v 产生的契约为c s l ，且p r e ( c s l ) = a ，p o s t ( c s l ) = b ；s 2 对v 产生的契约为c s 2 ，且p r e ( c s 2 ) = c ，p o s t ( c s 2 ) = d 。 则s 对v 产生的契约c s 为： p r e ( c s ) ：= i fi s d e t e r m i n e d ( c s l ) = t r u et h e na e l s ea & c p o s t ( c s ) ：= i fi s d e t e r m i n e d ( c s 2 、= t r u et h e nd e l s eb i i d 对于前置条件，如果i s d e t e r m i n e d ( c s l ) = f a l s e ，则表明语句s 1 并不能确定变 量的状态，下一条语句s 1 将对变量的使用进行更加严格的约束，所以p r e ( c s ) ：= a & c 。 对于后置条件，如果i s d e t e r m i n e d ( c s 萄= f a l s e ，则表示语句s 2 所产生的后置 条件只是一种可能情况，所以p o s t ( c s ) ：= b0d ； 【2 1 分支语句的契约更新 对于存在分支的语句，需要结合各个分支对契约的影响。具体的更新规则如 8c c + + 程序安全分析中契约的设计与实现 f ： 规则2 2 条件分支语句的更新 对于语句s ： i f ( ) t h e ns 1e l s es 2 和变量v ，假设s 1 对v 产生的契约为 c s l ，且p r e ( c s l l = a ，p o s t ( c s l ) = b ；s 2 对v 产生的契约为c s 2 ，且p r e ( c s 2 ) = c ，p o s t ( c s 2 ) = d 。则s 对v 产生的契约c s 为： p r e ( c s ) ：= a & c p o s t ( c s ) ：= b0 d 对于前置条件，在存在分支语句的情况下，为了保证变量能被每条分支安全 使用，在进入分支前所变量契约的后置条件必须符合每条分支的要求，所以分支 语句对变量的前置条件必须加强为每条分支语句前置条件相与的结果。基于这种 更新方法，只要在任何一个分支中存在安全漏洞，都有会被检测出。 当分支语句结束时，分析程序不能确定程序从哪一条分支流出，变量状态不 能确定。所以，需要把所有的可能结果相或起来。 对于超过两条分支的语句，需要对规则2 2 进行扩展如下： 假设语句s 有n 条分支，第n 条分支对变量产生的契约为c s n ，则最终s 对 变量产生的契约c s 为： p r e ( c s ) ：= p r e ( c s l ) & & p r e ( c s 2 ) & & & & p r e ( c s n ) p o s t ( c s ) ：= p o s t ( c s l ) p o s t ( c s 2 ) l l i i p o s t ( c s n 、 【3 】循环语句的契约更新 规则2 3 循环语句的更新， 设语句s ： w h i l e ( 1s 1 和变量v ，s 1 对v 的前置条件为a ，后置条件为b ， v 的契约为c v ，则： p r e ( c v ) ：= a p o s t ( c v ) ：= b 【4 i 琢i 数调用语句的契约更新 对于函数调用，需要考虑函数调用后对函数所使用到的外部变量的影响，所 以必须更新所有受影响的变量契约。 规则2 4 函数调用的更新 设在函数a 中存在对函数b 的调用，函数b 的契约为f c 。 对于调用时所使用到的实参、返回值和全局变量，从函数契约f c 中获取其对 应的参数契约，按照规则2 1 进行更新。 如下函数调用语句： v a t = f u n c ( p a r a m l ，p a r a m 2 ) ； 对契约进行更新时，首先取得f u n c 的函数契约，该函数契约包括第一个参数 的契约c p l 和第二个参数的契约c p 2 、所用到的全局变量契约g l o b a l s e t 和返回值 第二章契约安全分析方法概述9 契约c r e t 。 然后分别利用c p l 和c p 2 对实参p a r a m l 和p a r a m 2 的契约进行更新，利用c r e t 对v a t 的契约进行更新。最后查找相应的全局变量，对所使用到的全局变量契约进 行更新。 2 2 3 基于契约的安全判定 安全判定的基本思想是按照一定的规则对每个变量和函数契约的前后置条件 进行比较。当结果符合相应的规则时，则变量或函数的使用可以被认为是安全的。 否则，认为是不安全的。 由于契约分为变量契约和函数契约两种，契约的判定规则也分为变量的安全 判定和函数调用的安全判定两种。 规则2 5 变量的安全判定 设语句s 使用了变量v ，语句s 执行前变量v 的契约为x ，语句s 对v 的契 约为y ，着p o s t ( x ) 满足p r e ( y ) 的要求，则认为s 对变量v 的使用为安全的；否则 为不安全的。 规则2 6 函数调用的安全判定 设有函数调用) ，对函数f 使用的参数变量、全局变量和返回值变量按规 则2 5 进行判定，若所有变量的使用都安全，则认为函数调用是安全的；否则是不 安全的。 2 3 基于契约的安全分析方法 基于契约的安全分析方法，以契约的更新和判定为基础，通过对分析过程中 遇到的各种语句按照既定的契约规则进行更新和判定，最终达到程序安全分析的 要求。 一般的程序由函数所组成，因此基于契约的安全分析方法由过程内安全分析 方法和程序安全分析方法组成。 算法2 1 过程内安全分析 输入：函数f 输出：函数f 的契约信息 方法： 初始化f 的函数契约c f ； d o 从f 中取出语句s ； f f s 为顺序结构 1 0c c + + 程序安全分析中契约的设计与实现 按规则2 5 和规则2 1 对契约进行判定和更新； e l s i fs 为分支结构 按规则2 5 和规则2 2 对契约进行判定和更新； e l s i fs 为循环结构 按规则2 5 和规则2 3 对契约进行判定和更新； e l s i f s 为函数调用 按规则2 6 和规则2 4 对契约进行判定和更新； e n d i f w h i l e ( f 中还有未被分析的语句) r e t u r nc f ： 在过程内安全分析算法的基础上，按照函数依赖关系图，对程序包含的所有 函数进行分析，最终完成一个完整程序的分析。 算法2 2 程序安全分析 输入：源程序 输出：安全分析结果 过程： 按函数的依赖关系对函数进行拓扑排序。 根据拓扑排序的结果，按算法2 1 至下而上对各个函数进行分析。 2 4 契约在c ，c + + 安全分析中的应用 在研究契约安全分析原理的基础上，本文将契约分析方法应用于c c + + 安全 检查，设计与实现了针对c ，c + + 安全分析契约的方法。该设计主要支持指针变量 相关的安全检查，并提供了数组越界安全检查的接口。 针对c c + + 指针变量的契约检查方法的主要工作是设计指针变量的契约信息 和指针变量契约的安全规则和更新算法。对于指针变量契约的前后置条件，本文 采用基于指针指向状态的表示方法来实现。具体做法是将指针的前后置条件定义 为一系列可能指向状态集合，其中前置条件为安全使用指针变量时指针的所有允 许指向的状态；后置条件为语句结束后指针的所有可能指向的状态。然后针对指 针变量契约，设计与实现其安全判定方法，用于对指针变量的使用进行安全判定。 最后通过实现指针变量契约的更新算法，有效地指导具体程序的安全分析。 在支持指针引用的基础上，本文实现的契约安全分析方法还支持对指针相关 的资源泄露进行检查。在以往的工作中【2 5 】，资源泄露的检查独立成一个模块，采 用单独通过记录指针的资源使用情况对资源泄露进行检查，而没有采用契约分析 的方法。本文所实现的指针变量契约，可以支持对指针相关的资源泄露的检查，从 第二章契约安全分析方法概述 而将指针引用的安全检查和资源泄露检查统一起来。其核心思想是在具体程序分 析过程中对指针的契约进行更新，当指针变量失效时( 如指针变量出作用域) ，利 用指针失效前的后置条件。结合指针别名析和指针的指向状态中是否含有资源相 关的状态( 如指向c 的堆空间) 进行分析。 第三章契约安全分析模块的设计与实现1 3 第三章契约安全分析模块的设计与实现 3 1 模块需求 契约分析模块的目标是设计和实现基于契约的安全分析方法，并且使该方法 支持以下需求： ( 1 ) 支持对c e h 程序的安全分析。具体为支持指针引用相关的安全分析、 程序过程内和跨过程的安全分析等。 ( 2 ) 通过分析源程序，自动获取安全分析所需要信息，而不需要用户在源程 序中添加辅助信息。 如下一个例子： 0 1 c h a r h e l l o ( c h 丑r + p a r a m ) 0 2 0 3 s t r c p y ( p a r a m ，“h e l l ow o r l d ) ； 0 4r e t u r np a r a m ； 0 5 ) 0 6 i n t m a i n 0 0 7 0 8 c h a r + m y s t r i n g ； 严未初始化的指针+ 0 9 h e l l o ( m y s l r i n g ) ； 使用一个未初始化的指针 1 0 p r i n t f ( s ”m y s t r i n g ) ；宰打印一个未初始化的指针+ 1 1r e t u r no ： 1 2 ， 在第9 行、第l o 行中分别存在指针使用的安全问题。契约模块的实现必须支 持在无用户添加辅助信息的情况下，查找出以上的安全问题，并且最终能报告出 闯题所在的出处。 本模块主要是以契约分析方法作为指导思想，实现契约的定义、更新和安全 判定规则。 3 2 整体设计 契约模块的设计和实现主要包括以下四部分： ( 1 ) 配置管理：制定安全分析的配置信息，设计和实现用于保存配置信息的 配置文件；对配置文件进行解析获取所需的配置信息。通过契约配置管 1 4 c ，c + + 程序安全分析中契约的设计与实现 理，可以把预定义的判定规则和原始契约信息保存在配置文件中，然后 通过解析配置文件获取配置信息，供契约分析使用。 ( 2 ) 前后置条件信息保存：主要是讨论前后置条件的保存结构。通过所设计 好的前后置信息保存结构，保存契约的前后置条件， ( 3 ) 契约定义：主要是设计和实现契约相关的类和操作。其中主要包括前后 置条件类结构的设计与实现，变量契约类的设计与实现和函数契约类的 设计与实现。 ( 4 ) 契约更新判定：实现契约安全判定和更新算法。其中契约的安全判定算 法利用契约信息，判定程序的安全性；契约的更新算法用于在程序安全 分析过程中更新相应的契约信息，使契约信息能在安全判定中使用。 3 3 配置管理 对c c + + 源程序进行安全分析，首先必须制定基本的安全规则，在此基础上 进行程序的安全分析。 程序安全分析工具发展的早期，安全分析器的设计者通常将相关的规则集成 到安全分析器的当中【2 6 l 。这种把规则定义集成到安全分析器内部的方法，由于所 有规则都定义在安全分析器内部，用户不可能扩展自己定义的安全规则，其所能 定义的安全规则相当有限，扩展性差。在早期c c + + 使用范围比较小、外部库函 数相对不多的情况下，这种缺陷可以被接受。但随着c c + + 程序规模日益变大， c c + + 安全分析器所需要定义的安全规则也越来越多，将安全规则集成到c c + + 安全分析器中的做法已经明显不能满足需求。并且，越来越多的c + + 外部库函数 开始在程序设计中被使用，如果继续采用将安全规则集成到安全分析器中的做法， 将使这些外部库函数得不到检查，安全分析器的功能将受到很大的限制。 现在一般的安全分析器主要采用两种方法对以上的缺陷进行改进。其中一种 以s p l i n t e 2 ”为代表，其做法是允许用户在源程序中添加自定义规则，通过用户自 定义规则补充安全分析器的安全规则的不足。这种方法的缺陷是需要修改源程序， 破坏的源程序的原始结构。另一种以c o d e c h e c k t 2 s l 为代表，提供一种用于描述安 全规则的脚本语言。用户通过自定义脚本文件，实现对安全规则的扩充。这种使 用特定脚本语言定义安全规则的方法，具有强大的描述能力，可以较好的弥补分 析器安全规则定义的不足。但由于这些脚本语言一般比较复杂，程序员必须事先 学习相应的脚本语言才能使用这些安全分析工具。这弛做法大大的增加了使用安 全分析器的复杂度。 本文采用借鉴脚本描述的安全规则定义方法，通过外部定义的配置文件描述 安全规则和基本信息。与通过自定义脚本语言的方法不同，本文用x m l 的格式来 第三章契约安全分析模块的设计与实现1 5 描述安全规则和配置信息。由于x m l 是一种通用的描述语言，使用安全分析器的 用户只需要了解x m l 语言，而无需专门学习安全分析器提供的特定脚本语言便可 以方法的对安全规则进行扩展，从而使安全分析器的易用性和有效性得到提高。 并且利用已有的x l v i l 解析器 2 9 1 ，便可实现对配置文件的分析，有效地低了安全分 析器实现的复杂度。 本节以下内容将介绍契约配置信息的定义和获取。其中配置信息定义相关小 节主要论述契约分析所需要的配置信息和如何利用x m l 语言来定义配置信息：配 置信息的获取相关小节主要介绍如何通过定义相应的数据结构，解析配置文件获 取相应的配置信息。 3 3 1 契约配置信息的定义 契约配置信息主要包括指针变量前后置条件的原子状态集合、c c 什标准的库 函数配置、外部定义配置信息。下面分别描述契约配置信息及其在x m l 中的表现 形式。 1 、指针变量原子状态信息 指针变量原子状态是指针变量契约前后置条件的基本组成元素。通过原子状 态之间的运算，构成前后置条件。原子状态为一个有限结合，预定义如下： p o i n tt ou n i n i t i a l i z e d ，指针未初始化 p o i n tt on u l l + 指针指向空地址叩 p o i n tt oe x c e e d _ s c o p e 产指针指向的变量超出作用域范围 p o i n tt of r e e d严指针指向的空间已被释放+ ， p o i n tt og l o b a l ，l 指针指向全局数据区的变量 p o i n tt os t a c k，l 指针指向栈变量， p o i n tt o s t a t i c 产指针指向静态变量， p o i n tt och e a p严指针指向c 堆空间+ p o i n t t o l c p p h e a p p 指针指向c + + 堆+ p o i n tt 0a r r a y，指针指向数组吖 p o i n t t o s i n g l e 产指针指向单一地址吖 p o i n tt of u n c t i o n 指针指向函数+ ， p o i n t t o c o n s t 产指针指向常量+ p o i n tt oh l eo p e n+ 指针指向打开的文件 p o i n tt of i l ec l o s e d ，幸指针指向关闭的文件， p o i n tt ou n k n o ws t a t u s ，指针指向未知吖 p o i n tt ov a r i a b l e产指针指向变量+ ， 1 6c ，c + + 程序安全分析中契约的设计与实现 以上原子信息在配置文件中的描述方式如下： p o i n t t o u n i n i t i a l i z e d p o i n t t o n u l l p o i n t t o v a r i a b l e 2 、c c + + 标准库函数信息 c c + + 标准库函数的契约信息主要包括库函