Abstract: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 Bytecode. 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.