Java虚拟机安全性的形式化分析和验证
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第1章 前言 | 第11-28页 |
| ·Java虚拟机 | 第11页 |
| ·字节码验证和动态类加载 | 第11-16页 |
| ·研究目标 | 第16-17页 |
| ·研究方法 | 第17-24页 |
| ·类型系统 | 第17页 |
| ·定理证明器 | 第17-24页 |
| ·相关工作 | 第24-26页 |
| ·论文组织 | 第26-28页 |
| 第2章 对 HOL系统的扩充 | 第28-46页 |
| ·HOL系统的实现 | 第28-37页 |
| ·系统内核 | 第28-32页 |
| ·定理证明工具 | 第32-37页 |
| ·假设列表管理的扩充 | 第37-43页 |
| ·其它扩充 | 第43-45页 |
| ·小结 | 第45-46页 |
| 第3章 JVML0-对象初始化 | 第46-58页 |
| ·引言 | 第46-48页 |
| ·JVMLO的语法及非形式化语义 | 第48-49页 |
| ·形式化模型 | 第49-53页 |
| ·操作语义 | 第49-51页 |
| ·静态语义 | 第51-53页 |
| ·别名对象分析 | 第53-54页 |
| ·可靠性 | 第54-56页 |
| ·基本谓词 | 第54-55页 |
| ·主要定理 | 第55-56页 |
| ·小结 | 第56-58页 |
| 第4章 JVML1-子例程 | 第58-81页 |
| ·引言 | 第58-61页 |
| ·JVML1的语法及非形式化语义 | 第61页 |
| ·形式化模型 | 第61-68页 |
| ·操作语义 | 第61-62页 |
| ·静态语义 | 第62-68页 |
| ·可靠性 | 第68-80页 |
| ·基本引理 | 第68-77页 |
| ·主要定理 | 第77-80页 |
| ·小结 | 第80-81页 |
| 第5章 JVML2-锁原语 | 第81-102页 |
| ·引言 | 第81-83页 |
| ·JVML2的语法及非形式化语义 | 第83页 |
| ·形式化模型 | 第83-91页 |
| ·操作语义 | 第83-86页 |
| ·静态语义 | 第86-91页 |
| ·可靠性 | 第91-95页 |
| ·基本谓词 | 第91页 |
| ·基本引理 | 第91-93页 |
| ·主要定理 | 第93-95页 |
| ·在 HOL系统中的形式化实现 | 第95-100页 |
| ·类型和值 | 第95-96页 |
| ·集合及其操作 | 第96-97页 |
| ·通用谓词 | 第97-98页 |
| ·辅助函数 | 第98-99页 |
| ·操作语义 | 第99页 |
| ·静态语义 | 第99-100页 |
| ·小结 | 第100-102页 |
| 第6章 动态类加载 | 第102-145页 |
| ·引言 | 第102-106页 |
| ·JDK1.2和1.3中的类型欺骗及其解决方法 | 第106-113页 |
| ·类型欺骗 | 第106-108页 |
| ·解决方法 | 第108-113页 |
| ·形式化模型 | 第113-127页 |
| ·形式化定义 | 第113-116页 |
| ·操作语义 | 第116-119页 |
| ·静态语义 | 第119-121页 |
| ·可靠性 | 第121-127页 |
| ·在 HOL系统中的形式化实现 | 第127-143页 |
| ·类文件 | 第127-131页 |
| ·堆 | 第131-133页 |
| ·Class对象 | 第133-134页 |
| ·类、字段和方法解析 | 第134-136页 |
| ·操作语义 | 第136-141页 |
| ·静态语义 | 第141-142页 |
| ·语法支持 | 第142-143页 |
| ·小结 | 第143-145页 |
| 第7章 本文与相关工作的比较 | 第145-152页 |
| 第8章 结束语 | 第152-156页 |
| ·结论 | 第152-153页 |
| ·进一步研究方向 | 第153-156页 |
| 致谢 | 第156-157页 |
| 参考文献 | 第157-170页 |
| 在研发表论文 | 第170-171页 |
| 附录A | 第171-174页 |
| 附录B | 第174-199页 |
