文档介绍：西安电子科技大学
硕士学位论文
C/C++程序安全分析中契约的设计与实现
姓名:马志宇
申请学位级别:硕士
专业:计算机软件与理论
指导教师:刘坚
20070101
摘要本文研究基于契约的安全分析方法。该方法通过对过程内的变量构造变量契约、对跨过程的函数调用构造函数契约描述程序的状态,并按函数调用关系自下新算法实现程序安全分析。结合珻语言的特点,本文设计和实现了针对疌程序安全分析的契约件的描述方法。同时结合契约分析原理,设计了指针变量契约的数据结构,并提供一组算法,用于更新指针变量契约和对指针变量进行安全判定。该框架具有一定的可扩展性,按需求继承相应的接口并实现对应的算法便可关键词:契约跨过程自下而上安全分析而上获取相应的契约信息。在获取契约的基础上,使用相应的安全判定规则和更分析方法框架。根据疌安全分析实际需求,给出了痗指针变量前后置条以使契约分析方法支持对更多疌类型变量的分析。
珻,瓸,..:·瓸瑃琲畉.
本人签名:墨盘簦本人签名;墨生创新性声明关于论文使用授权的说明日期:笙旦日期:丝早本人声明所呈交的论文是我个人在导师的指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢中所罗列的内容以外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含为获得西安电子科技大学或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究工作所做的任何贡献均已在论文中作了明确的说明并表示了谢意。申请学位论文若有不实之处,本人承担一切相关责任。本人完全了解西安电子科技大学有关保留和使用学位论文的规定,即:研究生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕业离校后,发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。学校有权保留送交论文的复印件,允许查阅和借阅论文:学校可以公布论文的全部或部分内容,可以允许采用影印、缩印或其他复制手段保存论文。C艿穆畚在解密后遵守此规定本学位论文属于保密在年解密后适用本授权书。导师签名:
,除了要求软件在效率和可用性上得到相应提高外,对就必须符合一定的安全要求。一些涉及保密领域的软件,例如银行系统,也需要作为被普遍使用的程序设计语言,豢诙返陌踩砸膊欢鲜艿饺嗣堑闹厥印S支持缓冲区越界的检查,也没有对指针的使用进行较好的限制。这些在软件安全的镅裕捎诩坛辛薱的大多数语法和语义,使得一些械陌踩┒丛赾仍然存在。虽然卜曜囊胄绿匦杂糜诩跎侔踩┒缫氡镏绦蛟弊远芾矶峙涞牡ジ龆韵螅饩瞿诖娑峙湎喙问题导嗜杂泻芏郼程序没有使用这些新特性,而使相关的安全漏洞仍然的剧增和程序结构的复杂化。这种情况下,人工查找程序中隐藏的安全漏洞显得相当困难且代价很高。并且由于人工查找的成功率与程序员的经验和能力有关,人工检查程序中的安全漏洞并不能很好的保证检查效果。针对人工检查瓹.【盗械目7旁创爰觳夤ぞ撸芗觳獬龊艽笠焕喟踩┒矗乙材芄软件安全性也提出了更严格的要求。一些实时嵌入式软件,例如飞机的控制软件,对安全性有较高的要求。此外,在一些高尖科技和军事应用上,计算机软件的安全性则是极其重要的一环。于早期饕S糜诘撞闳砑7ⅲ渖杓颇勘晔歉玫睦没髯试春吞岣咝剩而对安全性的考虑并不全面,缺少很多对软件安全性的支持。例如镅圆⒚挥支持上的缺陷,导致使用镅越谐绦蛏杓剖保赡艽嬖诎踩侍狻:罄闯鱿准模板类库,用模板类和等代替械氖椋饩鍪樵浇缥侍猓挥媚板类存在。同时,由于疌标准并不要求编译器【慷园踩┒唇刑囟ǖ募觳椋车标准要求的工作,而将查找漏洞的任务交给程序员人工进行。人工进行安全检查,在早期程序代码量较少、结构较为简单的时期,能够较好的找出程序中的安全漏洞。但随着软件行业的发展,软件的功能越来越强大,伴之而来的是程序代码量序安全漏洞的缺陷,人们开始研究自动化检查工具,辅助程序安全分析有效地提出许多在空间利用、运行效率上的改进方法,但其检测方法相当有限,且误报较多。该系列的最初版本,检查条件比较宽,通常会检测程序的所有路径而不考虑代码路径的可达性,然后报告可能存在安全问题。其采用的方法虽然俊”。
研究背景能有效检测过程内的安全漏洞,但在跨过程检查中存在严重的缺陷。】可以看作是的升级版,允许用户对源程序添加注解辅助安全分析,可以在功能之外执行更进一步的检查。通过结合用户辅助定义信息,可以有效地缩小检查范围,使检查结果更加准确。但由于需要用户修改源程序来添加辅助信息,该检查方法降低了检测工具的自动化程度,增加程序员的工作量。并且为准确描述用户需求,定义了较为复杂的用户辅助信息描述方法,程序员需要学习如何使用这种描述方法才能正确的使用该工具。而学习这些知识,往往需要相当长基于程序抽象表