论文题目: Java虚拟机安全性的形式化分析和验证
论文类型: 博士论文
论文专业: 计算机应用技术
作者: 左天军
导师: 陈平
关键词: 类型安全,字节码验证,动态类加载,类型系统,操作语义,定理证明,系统
文献来源: 西安电子科技大学
发表年度: 2005
论文摘要: 本文提出了一种描述Java虚拟机语义的形式化模型,该模型包含Java虚拟机安全体系结构中两个最重要的特性:字节码验证和动态类加载。具体地,本文定义了Java虚拟机语言(JVML)的一个子集,给出了该子集的类型系统和操作语义,并根据操作语义证明了该类型系统的可靠性。因此,该类型系统可保证一个类型正确的字节码程序不会在运行时出现类型错误。上述工作的形式化是在交互式定理证明器HOL系统中完成的。本文认为,对于形式语义而言,采用一种机械化验证工具对于保证定义的一致性、保证形式化过程的正确性是十分重要的。为此,本文还分析了HOL系统的实现,并对其进行了扩充。 在字节码验证的形式化过程中,本文分三个阶段研究了三个复杂的静态分析问题:对象初始化、子例程和锁原语。 第一阶段,本文通过定义JVML的一个子集JVML0,来研究字节码的对象初始化特性。本文证明了Java虚拟机规范对于别名分析算法的约束过强,这个结论表明,当前Sun的字节码验证程序包含了大量不必要的类型检查。这里,JVML0的类型系统能够保证字节码程序不会使用未初始化的对象。 第二阶段,本文将JVML0扩充为JVML1,以包含子例程。在类型规则中,本文引入了一个跟踪子例程调用过程的活动记录栈,用于记录程序当前所处的调用位置和子例程访问的局部变量集合。本文为活动记录栈定义了一种偏序关系,它不允许字节码程序递归调用子例程(这种约束与Java虚拟机规范是一致的)。实际上,递归调用不仅增加了Java虚拟机的复杂性,而且也没有为编译Java程序提供多少帮助。与Java虚拟机规范相比,JVML1的类型系统具有更弱的类型约束。例如,通过在对象的类型中引入表示子例程调用地址的信息,本文提出一种与Java虚拟机规范不同的别名分析方法。该方法不仅更加简单有效,而且能够接受更多的类型正确的字节码程序。Java虚拟机规范不允许aload x指令使用未初始化的局部变量x,而JVML1的类型系统取消了这种约束;Java虚拟机规范要求每个子例程只能有一个ret指令,而JVML1的类型系统允许子例程有任意个ret指令。尽管本文减弱了某些类型约束,但是并没有对字节码程序的类型安全造成任何影响。JVML1的类型可靠性定理保证:(1)子例程能够以基于调用栈的方式返回到正确的调用地址;(2)子例程能够正确处理别名对象。 第三阶段,本文将JVML1扩充为JVML2,以包含锁原语。JVML2的类型系统是对当前Sun的字节码验证的一种扩充,因为Sun的虚拟机实现并不对字节码程序进行静态检查,来判断其是否正确使用了锁原语。JVML2类型系统通过引入锁记录集合和新的类型,在兼容JVML1类型系统的同时,能够静态检查字节码程序的结构化加锁特性,即:(1)无论方法调用正常或异常结束,方法调用过程中程
论文目录:
摘要
Abstract
第1章 前言
1.1 Java虚拟机
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 JVMLO的语法及非形式化语义
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 JDK1.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
发布时间: 2007-01-10
参考文献
- [1].云环境下能量高效的任务调度方法研究与应用[D]. 丁有伟.南京航空航天大学2016
- [2].面向云计算的虚拟机系统安全研究[D]. 刘谦.上海交通大学2012
- [3].虚拟机安全保障及其性能优化关键技术研究[D]. 唐宏伟.中国科学院大学(中国科学院深圳先进技术研究院)2017
- [4].多核虚拟环境的性能及可伸缩性研究[D]. 宋翔.复旦大学2014
- [5].云计算环境下的任务调度与虚拟机整合研究[D]. 许贺洋.电子科技大学2017
- [6].基于虚拟机架构的可信计算环境构建机制研究[D]. 程戈.华中科技大学2010
- [7].公共云计算环境下用户数据的隐私性与安全性保护[D]. 张逢喆.复旦大学2010
- [8].智慧城市信息系统关键技术研究[D]. 袁远明.武汉大学2012
- [9].大规模高效能计算的系统软件关键技术研究[D]. 刘勇鹏.国防科学技术大学2012
- [10].云计算环境下可信虚拟数据中心构建及其关键技术研究[D]. 万鑫.华中科技大学2017
相关论文
- [1].Java程序优化与数据竞争检测的研究[D]. 杨克峤.复旦大学2010
- [2].分布式多层次数据库应用模型研究[D]. 李文立.大连理工大学2002
- [3].JE-Java芯片系统关键技术的研究与设计[D]. 陈虎.中国人民解放军国防科学技术大学2000
- [4].Java USIM卡安全计算研究[D]. 王明华.北京邮电大学2006
- [5].基于逻辑的程序验证方法在高可信软件开发上的应用[D]. 项森.中国科学技术大学2006
- [6].可信软件开发框架下的出具证明编译研究[D]. 葛琳.中国科学技术大学2007
- [7].面向C程序验证的切片执行方法[D]. 易晓东.国防科学技术大学2006