一种用于字节码程序模块化验证的逻辑系统

摘要

字节码既是运行于虚拟机的解释指令,也是定义良好的中间表示,是当今网络软件和计算设备中广泛使用的重要技术.字节码验证可以提高相关软件的可信程度,同时为构造证明保持编译器提供中间表示支持,具有重要的实用价值和理论价值.虽然近年提出了一些用于字节码程序的逻辑系统,但由于字节码本身的特点,造成了抽象控制栈复杂、控制流结构信息不足,因而字节码程序的"模块化验证"依然是一个巨大的挑战,并没有得到有效解决.将FPCC(foundational proof-carrying code)方法引入中间表示字节码,借鉴汇编程序的验证方法,设计出一种逻辑系统,给出字节码程序运行环境BCM(ByteCode machine)的逻辑系统CBP (certifying bytecode program)定义,完成系统的合理性证明和一组代表性实例程序的模块化证明,并实现机器自动检查.该工作为字节码验证提供一种良好的解决方案,同时也向着构造证明保持编译器环境迈出了坚实的一步,还可以为广泛使用的基于虚拟机复杂网络应用程序的深刻理解和深入分析提供理论帮助.