C语言子集上的程序逻辑

《C语言子集上的程序逻辑》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中圈绅孽技求大誊硕士学位论文玛蚴＼JC语言子集上的程序逻辑作者姓名：学科专业：导师姓名：完成时间：王勇朝信息安全冯新宇教授二零一三年五月一夺一二，平丑月UniversityofScienceandTechnologyofChinaAdissertationformasterdegreeProgramLogicforaSubsetofCAuthor：YongzhaoWangSpeciality：InformationSecuritySupervisor：Prof．XinyuFengFinishedTime：May，2013中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是

2、本人在导师指导下进行研究工作所取得的成果。除己特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均己在论文中作了明确的说明。作者签名：签字日期：驯弓坪多目幻曰中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入《中国学位论文全文数据库》等有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论

3、文的内容相一致。保密的学位论文在解密后也遵守此规定。凇开口保密年作者签名：工勇朝签字日期：砌30导师签名：日签字日期：夕马绺———————————’r—一阳侈牟州弓／日摘要随着软件的广泛使用，软件的安全性在近些年来也逐渐受到开发人员的重视，虽然国家以及社会很多机构投入大量的人力物力来解决系统中的漏洞，但是构建高可信软件的挑战依然存在。提高软件安全性的方法有很多种，在众多方法中，程序验证技术则通过一种严格的数学方法，为程序的安全性提供了极大的保证。程序和逻辑有着本质的联系，程序逻辑则是描述和论证程序行为的逻辑。如果把程序看成一个执行过程，程序逻辑的基本方法是先给出程序和逻辑间联系的形

4、式化方法，然后建立程序逻辑系统，并在此系统中研究程序的各种性质。我们由之前的程序逻辑的相关工作发现，在为实际的编程语言设计程序逻辑后，针对程序逻辑的可靠性，如果采取严格的证明(如经过Coq证明)，证明工作是极其复杂和冗长的。一个高可信的软件系统的最底层则是操作系统，考虑到大部分操作系统核心代码都采用C语言实现，因此设计一种针对C语言的程序验证方法尤为重要。基于此，本文的主要工作设计了一套针对C语言的程序逻辑，这个方法采用了Hoare风格的逻辑推导规则，并吸收了分离逻辑在模块化验证中的优点。我们选取了一个C语言的子集C3(CCodeCertified)，首先描述了可以执行C3程序的机

5、器模型，在此机器模型上定义了程序执行时的行为以及用来程序推理的规则，并且证明推导规则的可靠性。本文工作的主要贡献如下：1．C3通过在代码执行时添加代码栈，给出了其小步操作语义。与用大步语义的方式描述程序的操作语义相比，小步语义的方式可以更容易的扩展以支持并发程序；2．在C3中，通过扩展Hoare三元组，我们设计了新的推导规则，其形式为ps，R，EC，I卜{P)s{Q}；3．我们在语义上定义ps，R，Ec，I}{P)s_[Q)时，采用了直接定义的方式(directstyle)，与Cminor的后继风格(continuationstyle)相比，直接定义的摘要方式更加直观；4．文4t中

6、的所有的推导规则的可靠性都经过Coq的检查，提供了break、continue、return这三条语句推导规则在Coq中的可靠性证明。关键词：C语言，小步语义，程序逻辑，可靠性，形式化验证IIABSTRACT_一__-__---_-_-__●-●_-●____-●___--___I-____●_____-_一Inrecentyears，softwareplaysasignificantroleinindustryorourdailylifeandtheincreasingimportanceofsoftwaresystemalsoattractsmanyattentionsofpr

7、ogrammers．Thoughthecountyhasinvestedalargeamountoff'mancialfundtoimprovethesoftwarereliability，thechallengesforbuildinghigh-confidencesoftwareremains．Ofallthemethodsofincreasingthereliabilityofsoftwaresystems，softwareverificationwhichco