使用显式控制流语言验证汇编程序的方法
| 摘要 | 第1-7页 |
| Abstract | 第7-13页 |
| 第1章 绪论 | 第13-25页 |
| ·形式程序验证 | 第14-17页 |
| ·经典霍尔逻辑 | 第14-16页 |
| ·携带证明的代码 | 第16-17页 |
| ·汇编级程序验证的概述 | 第17-20页 |
| ·类型化汇编语言 | 第17-18页 |
| ·CAP系列 | 第18页 |
| ·存在的不足和挑战 | 第18-20页 |
| ·本文工作概述 | 第20-25页 |
| ·一个汇编程序部分正确性的验证系统 | 第20-22页 |
| ·一套基于步指标的验证系统语义模型 | 第22-24页 |
| ·章节安排 | 第24-25页 |
| 第二章 背景知识和基本设置 | 第25-35页 |
| ·程序的安全性和正确性 | 第25-26页 |
| ·元逻辑 | 第26-27页 |
| ·机器模型 | 第27-35页 |
| ·基本机器模型定义及其操作语义 | 第27-32页 |
| ·指标化机器模型及其操作语义 | 第32-35页 |
| 第三章 形式程序验证系统TCAP | 第35-61页 |
| ·显式控制流语言 | 第35-44页 |
| ·语言定义 | 第36-43页 |
| ·程序的局部性 | 第43-44页 |
| ·断言语言及覆盖 | 第44-51页 |
| ·验证系统及其语义模型 | 第51-61页 |
| ·本章小结 | 第60-61页 |
| 第四章 使用TCAP推理几个例子 | 第61-83页 |
| ·验证汇编级的函数 | 第61-67页 |
| ·验证汇编语言级的异常处理 | 第67-72页 |
| ·嵌入代码指针的支持 | 第72-81页 |
| ·本章小结 | 第81-83页 |
| 第五章 TCAP系统的扩展 | 第83-97页 |
| ·验证自修改代码 | 第83-89页 |
| ·支持自修改代码的机器模型 | 第84页 |
| ·验证框架 | 第84-85页 |
| ·验证自修改程序实例 | 第85-89页 |
| ·支持自修改代码的扩展小结 | 第89页 |
| ·高阶框架规则的支持 | 第89-95页 |
| ·扩展后的的新断言类型及新断言操作符 | 第90-93页 |
| ·高阶框架规则及新语义模型 | 第93-95页 |
| ·本章小结 | 第95-97页 |
| 第六章 相关工作及文章总结 | 第97-101页 |
| ·相关工作 | 第97-99页 |
| ·文章总结 | 第99-100页 |
| ·后续工作展望 | 第100-101页 |
| 参考文献 | 第101-107页 |
| 致谢 | 第107-108页 |
| 在读期间发表的学术论文与取得的研究成果 | 第108-109页 |
