安全c语言的设计与实现

《安全c语言的设计与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、伞固钟＾满来大赛‘ＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙｏｆＣｈｉｎａ＾硕±学位论文戀论文题目姿全Ｃ语言的役计与卖现作者姓名车为胜学科专业计算机应巧化术导师姓名陈意著教梭冯新李教投二Ｑ—Ｊ完成时＾年Ｉ月间中通种緣投术丈緣硕±学位论文幽巧安全Ｃ语言的设计与实现作者姓名：李为胜学科专业：计算机应用技术’导师姓名：陈意云教授冯新宇教授句於《—一完成时间：二〇六年四月二十日ＵｎｉｎａｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｏｆ

2、ＣｈｇｙＡ’ｄｉｓｓｅｒｔａｔｉｏｎｆｏｒｍａｓｔｅｒｓｄｅｒｅｅｇ？ＴｈｅＤｅｓｉｎａｎｄｇＩｍｌｅｍｅｎｔａｔｉｏｎｏｆＳａｆｅＣｐＬａｎｕａｅｇｇ’Ａｕ也ｏｒｓＮａｍｅ：ＬｉＷｅｉｓｈｅｎｇＳｅｃｉａｌｉｔＴｅｃｈｎｏｌｏｏｆＣｏｍｕｔｅｒＡｌｉｃａｔｉｏｎｐｙ：ｇｙｐｐｐＳｕｐｅｒｖｉｓｏｒ：Ｐｒｏｆ．ＹｉｙｕｎＣｈｅｎ，Ｐｒｏｆ．ＸｉｎｙｕＦｅｎｇＦｉｎｉ化ｅｄｔｉｍｅ：Ａｐｒｉｌ２ＰＳ２０１６中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取

3、得的成果，。除己特别加Ｗ标注和致谢的地方外论文中不包含任何他人己经发表或撰写过的研究成果一。与我同工作的同志对本研究所做的贡献均己在论文中作了明确的说明。．Ｖ作者签名；／使签字日期ｙｏｌｌｊ中国科学技术大学学位论文授权使用声明一作为申请学位的条件么，学位论文著作权拥有者授权中国科学技术大学拥目有学位论文的部分使用权，Ｐ；学校有权按有关规定向国家有关部口或机构送交论文的复印件和电子版，允许论文被查阅和借阅，＞可１＾１将学位论文编入《中国学位论文全文数据库》等有关数据库进行检索，可Ｗ采用影印、缩印或扫描等复制手段保存一、汇编学位论文。本人提交

4、的电子文档的内容和纸质论文的内容相致。保密的学位论文在解密后也遵守此规定。＾开材！□保密（年）作者签名：导师签名：。八．签字日期、、：八去，抑签字日期）．令：（Ｓ＾摘要摘要在社会高度信息化的今天，社会生产生活高度依赖软件系统，因此软件系统的安全性与可靠性也就显得愈加重要，通过形式化验证的方式保证程序的安全是一种重要的手段。一形式化验证有两种方法，种是模型检测，模型检测能够通过遍历系统所有的状态空间一，自动验证有穷状态的系统并构造不满足性质定理的反例。另种是演绛推理，它使用形式化的方式对程序进行数学推理，尽管Ｗ这种方式实现的

5、自动验证工具早己有实验室开发出来，但是至今都无法在工业界使用。巧其原因在于自动定理证明方面的困难，因为不管是断言语言描述能力的提升、循环不变式的推断、别名判断和验证条件的证明等，最终还是受到自动定理证明器能力的影响。鉴于送些原因，在研究自动定理证明的同时，应当适当考虑降低对自动定理证明期待，可Ｗ通过设计安全的语言去提高合法程序的口槛，同时设计规范语言来描述程序代码的行为性质Ｗ降低定理证明器的负担。本文主要贡献：一一，，Ｃ语言ｏａｒｅ第设计了种面向验证的Ｃ语言子集称为安全。在基于Ｈ＝逻辑推理规则对程序进行形式验证过程中，每当使用赋值公理怕比／ｘｘＥ（Ｑ

6、］｝怕｝是赋值语句的后断言，Ｑ［Ｅ／ｘ］表示对Ｑ中所有Ｘ代换为Ｅ）时，必须保证后断言＝Ｑ与赋值语句ｘＥ中没有潜在别名，否则Ｑ［Ｅ／ｘ］是最弱前断言的结论不可靠，而Ｃ语言广泛存在的别名，给基于Ｈｏａｒｅ逻辑的推理带来难题。本文在基于Ｃ９９标准之上，从别名的角度讨论了Ｃ语言的安全性Ｗ及其会给程序验证带来的问题，并Ｗ此为启示设计了安全Ｃ语言，在安全Ｃ语言中要求对Ｃ语言中各种类型增加编程限制来使得对送些被限制类型的变量操作表现得较为规范，同时还要求使用标注对程序加Ｗ说明Ｗ减轻定理证明器负担。二一第，设计了种规范语言，规范语言定义了安全Ｃ语言要求的标注的语法

7、语义及使用方式，Ｃ，规范语言Ｗ形式化的方式描述Ｃ程序的行为性质该些对程序行为性质的描述最终都会传递给自动定理证明器，从而更大程度上帮助自动定理证明器认知程序的行为，并最终验证程序行为是否符合规范中的描述。在规范语言中还专口引入形状描述来表示指针相关性质，Ｗ解决指针引起的别名导致程序难Ｗ验证这一问题。第Ｈ，基于ｃｌａｎｇ实现了安全Ｃ语言要求的编程约束检查Ｗ及规范语言的分析。Ｈｏａｒ关键词；ｅ逻辑形式化验证安全性语言规范