一种汇编语言指针逻辑的设计与实现

Assembly Pointer Logic:Design and Implementation

软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表。

Safety of the software is getting more and more important. One of the hot researches is the verification method for software to satisfy its safety policy. And the safety verification of the pointer programs is especially difficult to deal with. On the basis of our framework for the design and verification of safe program, and the PointerC pointer logic, this paper mainly in- troduces our research on an assembly pointer logic system for the assembly pointer programs. And the soundness of the assembly pointer logic has been proved using the proof assistant Coq. Moreover, using an implemented prototype, many non-trivial assembly pointer programs with shared mutable data structures such as list and tree have been verified.