| 一种汇编语言指针逻辑的设计与实现 |
| |
| 引用本文： | 李兆鹏,陈意云,华保健,王伟,田波.一种汇编语言指针逻辑的设计与实现[J].小型微型计算机系统,2009,30(6). |
| |
| 作者姓名： | 李兆鹏 陈意云 华保健 王伟 田波 |
| |
| 作者单位： | 1. 中国科学技术大学,苏州研究院软件安全实验室,江苏,苏州,215123
2. 中国科学技术大学,计算机科学技术系,安徽,合肥,230026 |
| |
| 基金项目： | 国家自然科学基金，Intel中国研究中心 |
| |
| 摘 要： | 软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题面临的困难,保证通过验证的汇编指针程序不存在空指针引用和内存泄露等安全问题.此逻辑的可靠性证明已在证明辅助工具Coq中完成.此外,本文还实现一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证.
|
| 关 键 词： | 软件安全 指针逻辑 Hoare逻辑 携带证明的汇编程序 |
Assembly Pointer Logic: Design and Implementation |
| |
| LI Zhao-peng,CHEN Yi-yun,HUA Bao-jian,WANG Wei,TIAN Bo.Assembly Pointer Logic: Design and Implementation[J].Mini-micro Systems,2009,30(6). |
| |
| Authors: | LI Zhao-peng CHEN Yi-yun HUA Bao-jian WANG Wei TIAN Bo |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
