优秀研究生学位论文题录展示

Java虚拟机安全性的形式化分析和验证

专 业: 计算机应用技术
关键词: 类型安全 字节码验证 动态类加载 类型系统 操作语义 定理证明
分类号: TP301
形 态: 共 189 页 约 123,795 个字 约 5.922 M内容
阅 读: 全文阅读说明

内容摘要


本文提出了一种描述Java虚拟机语义的形式化模型,该模型包含Java虚拟机安全体系结构中两个最重要的特性:

字节码验证和动态类加载。

具体地,本文定义了Java虚拟机语言JVML的一个子集,给出了该子集的类型系统和操作语义,并根据操作语义证明了该类型系统的可靠性。

因此,该类型系统可保证一个类型正确的字节码程序不会在运行时出现类型错误。

上述工作的形式化是在交互式定理证明器HOL系统中完成的。

本文认为,对于形式语义而言,采用一种机械化验证工具对于保证定义的一致性、保证形式化过程的正确性是十分重要的。

为此,本文还分析了HOL系统的实现,并对其进行了扩充。

在字节码验证的形式化过程中,本文分三个阶段研究了三个复杂的静态分析问题:

对象初始化、子例程和锁原语。

第一阶段,本文通过定义JVML的一个子集JVML0,来研究字节码的对象初始化特性。

本文证明了Java虚拟机规范对于别名分析算法的约束过强,这个结论表明,当前Sun的字节码验证程序包含了大量不必要的类型检查。

这里,JVML0的类型系统能够保证字节码程序不会使用未初始化的对象。

第二阶段,本文将JVML0扩充为JVML1,以包含子例程。

在类型规则中,本文引入了一个跟踪子例程调用过程的活动记录栈,用于记录程序当前所处的调用位置和子例程访问的局部变量集合。

本文为活动记录栈定义了一种偏序关系,它不允许字节码程序递归调用子例程这种约束与Java虚拟机规范是一致的。

实际上,递归调用不仅增加了Java虚拟机的复杂性,而且也没有为编译Java程序提供多少帮助。

与Java虚拟机规范相比,JVML1的类型系统具有更弱的类型约束。

例如,通过在对象的类型中引入表示子例程调用地址的信息,本文提出一种与Java虚拟机规范不同的别名分析方法。

该方法不仅更加简单有效,而且能够接受更多的类型正确的字节码程序。

Java虚拟机规范不允许aloadx指令使用未初始化的局部变量x,而JVML1的类型系统取消了这种约束;Java虚拟机规范要求每个子例程只能有一个ret指令,而JVML1的类型系统允许子例程有任意个ret指令。

尽管本文减弱了某些类型约束,但是并没有对字节码程序的类型安全造成任何影响。

JVML1的类型可靠性定理保证:1子例程能够以基于调用栈的方式返回到正确的调用地址;2子例程能够正确处理别名对象。

第三阶段,本文将JVML1扩充为JVML2,以包含锁原语。

JVML2的类型系统是对当前Sun的字节码验证的一种扩充,因为Sun的虚拟机实现并不对字节码程序进行静态检查,来判断其是否正确使用了锁原语。

JVML2类型系统通过引入锁记录集合和新的类型,在兼容JVML1类型系统的同时,能够静态检查字节码程序的结构化加锁特性,即:1无论方法调用正常或异常结束,方法调用过程中程序对某个对象的加锁次数必须等于对其的解锁次数;2方法调用过程中的任意一点,程序对某个对象的解锁次数不能超过对其的加锁次数。

JVML2的类型可靠性定理保证类型正确的字节码程序不会在运行时出现结构化加锁错误。

类加载器是动态类加载的核心机制,它在提供较高的程序设计灵活性的同时,还可用于动态隔离不同的应用程序。

但是,早期的Java版本JDK1.0和1.1中,动态类加载存在着一种称为Saraswat类型欺骗的设计错误。

为了修正这种错误,JDK1.2引入了一种类加载约束机制。

在动态类加载的形式化过程中,本文的模型不仅包含JDK1.2提出的这种机制,而且还指出了存在于JDK1.2和JDK1.3中的其它形式的类型欺骗,并为此提出一种称为子类型约束的解决方法。

该方法引入了一个称为类型合并集合的新的数据结构,并据此在类型规则中定义了相应的子类型约束条件。

为了证明该类型系统的可靠性,本文提出了一种为一个值指派类型的新方法。

另外,本文还对类文件结构进行了形式化,并定义了其上的相应操作,使得本文的模型更加符合Java虚拟机规范。

通过形式化建模和可靠性证明,本文还分析了字节码验证和动态类加载之间的关系。

综上所述,本文的主要贡献是:1为Java虚拟机提供了一种严格、可靠和全面的形式化定义;2为研究Java虚拟机的其它特性提供了一个统一的形式化理论框架;3为字节码验证提供了一种合理、可靠的重构方法;4通过形式化分析,进一步加深了对Java虚拟机的理解;5验证了采用HOL系统形式化实际程序设计语言的可行性..……

全文目录


文摘
英文文摘
第1章 前言
1.1Java虚拟机
1.2字节码验证和动态类加载
1.3研究目标
1.4研究方法
1.4.1类型系统
1.4.2定理证明器
1.5相关工作
1.6论文组织
第2章 对HOL系统的扩充
2.1 HOL系统的实现
2.1.1系统内核
2.1.2定理证明工具
2.2假设列表管理的扩充
2.3其它扩充
2.4 小结
第3章 JVML0-对象初始化
3.1引言
3.2 JVML0的语法及非形式化语义
3.3形式化模型
3.3.1操作语义
3.3.2静态语义
3.4别名对象分析
3.5可靠性
3.5.1基本谓词
3.5.2主要定理
3.6小结
第4章 JVML1-子例程
4.1引言
4.2 JVML1的语法及非形式化语义
4.3形式化模型
4.3.1操作语义
4.3.2静态语义
4.4可靠性
4.4.1基本引理
4.4.2主要定理
4.5小结
第5章 JVML2-锁原语
5.1引言
5.2 JVML2的语法及非形式化语义
5.3形式化模型
5.3.1操作语义
5.3.2静态语义
5.4可靠性
5.4.1基本谓词
5.4.2基本引理
5.4.3主要定理
5.5在HOL系统中的形式化实现
5.5.1类型和值
5.5.2集合及其操作
5.5.3通用谓词
5.5.4辅助函数
5.5.5操作语义
5.5.6静态语义
5.6小结
第6章 动态类加载
6.1引言
6.2 JDK 1.2和1.3中的类型欺骗及其解决方法
6.2.1类型欺骗
6.2.2解决方法
6.3形式化模型
6.3.1形式化定义
6.3.2操作语义
6.3.3静态语义
6.3.4可靠性
6.4在HOL系统中的形式化实现
6.4.1类文件
6.4.2堆
6.4.3 Class对象
6.4.4类、字段和方法解析
6.4.5操作语义
6.4.6静态语义
6.4.7语法支持
6.5小结
第7章 本文与相关工作的比较
第8章 结束语
8.1结论
8.2进一步研究方向
参考文献
附录A
附录B

相似论文

  1. 遗传算法研究及在航运船舶配载系统中的应用,63 页,TP301.6 TP319 U692.32
  2. 支持向量机集成学习算法研究, 11页,TP301.6 TP181
  3. 海量数据可视化方法的研究,58 页,TP301.6 TP393.08
  4. 改进型人工鱼群算法及其在数值方法中的应用,53 页,TP301.6 O241
  5. 求解QoS路由优化的蚁群算法研究,37 页,TP301.6 TN913.11
  6. 协作型协进化算法及其应用,46 页,TP301.6
  7. 微粒群优化算法的改进研究与应用,90 页,TP301.6
  8. 基于模糊聚类与多生境排挤的小生境遗传算法研究,61 页,TP301.6
  9. 基于群智能算法的聚类分析方法研究,63 页,TP301.6 O242.23
  10. 基于规则的委托授权研究,55页,TP309
  11. 视频数字双水印技术研究,68页,TP309.7 TP391.41
  12. SOAP消息传递安全性技术研究与SOAP加密的实现,64页,TP309.7 TP393.08
  13. CCIPS的分布实时容错一体化研究,72页,TP302.8 TP311.52 V57
  14. UML图的Petri网建模,70页,TP302 TP393.11
  15. 基于J2EE平台的益智类游戏开发中安全问题的研究,61页,TP309 TP393.08
  16. 航天分布式实时容错平台研究,74页,TP302.8 TP393
  17. 非负矩阵分解算法理论及其应用研究,53页,TP301.6
  18. 工作流的Petri网建模及模型分析,49页,TP302 TP391.78
  19. 访问控制模型RBAC中时间约束特性的研究,44页,TP309
  20. 公钥基础设施中证书路径构造方法研究,57页,TP309
中图分类: > TP301 > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法

© 2012 book.hzu.edu.cn