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

随着软件规模和复杂度的日益提升,软件安全的问题变得越来越严峻,同时有越来越多的研究工作集中在高可信软件的开发上 .由于类型系统表达能力的不足,现有的研究不触及底层软件的验证 .由于Hoare逻辑更好的表达能力,采用Hoare逻辑风格的推理,在汇编语言级别,使用Coq形式化与定理证明工具可以实现一个经过安全验证的动态存储管理函数库,这是程序验证技术一次有意义的实践 .实践表明,程序验证技术可以应用到高可信软件的开发上 .

Safety Verification of Dynamic Storage Management in 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.