动态存储管理安全验证的Coq实现  

Safety Verification of Dynamic Storage Management in Coq

作　　者：项森[1] 陈意云[1] 林春晓[1] 李隆[1] 

机构地区：[1]中国科学技术大学计算机科学技术系,合肥230027

出　　处：《计算机研究与发展》2007年第2期361-367,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60473068;60673126);Intel中国研究中心资助项目

摘　　要：随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上.由于类型系统表达能力的不足,现有的研究不触及底层软件的验证.由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践.实践表明,程序验证技术可以应用到高可信软件的开发上.The increasing scale and complexity of software makes the software safety and security critical. Thus more and more research focuses on the development of high-assurance software. Since type system is not expressive enough, the existing research does not touch the verification of infrastructure codes. In this paper, a certified dynamic storage management library is built using Hoare-logic style reasoning at the assembly level with the assistance of a theorem formalization and proof tool called Coq, since Hoare logic is more expressive. This work is a significant application of program verification technique. The experiment shows that program verification can be applied in high-assurance software development.

关 键 词：形式化方法 高可信软件 程序验证 携带证明的代码 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]