中文摘要：

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

英文摘要：

Bytecode, which is widely used in network software and mass devices, is a kind of interpretive execution instruction and a favorable intermediate presentation, Bytecode can highly improve the reliability of relevant software and strongly support the construction of proof-preserved compilers, so it holds theoretical and practical value. Although some efforts have been made on building a logic system for the bytecode program, modular certification of bytecode still remains challenging because of the complexity of the abstract control stack and the lack of control over flow structure information. Moreover, the expression ability of the recent logic system is very limited. This paper presents a logic framework that supports modular certification of bytecode programs and is more expressive. FPCC technology is originally introduced into this framework for bytecode. This paper provides the formal definition of CBP （certifying bytecode program） logic system for the running environment of Byteeode. Also, this paper has also finished the proof of the theorem and a group of instance programs. This piece of work is not only a good solution for certifying Bytecode, which is run on a stack-based virtual machine, but also a significant improvement for the construction of a proof-preserved compiler environment. In addition, this system is useful in finding a deeper understanding and analysis of network application based on a virtual machine.