本文提出了一种描述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)无论方法调用正常或异常结束,方法调用过程中程