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

摘要：

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

关键词：软件安全、指针逻辑、Hoare逻辑、携带证明的汇编程序

所属期刊栏目：30

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2009-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1025-1030