English Version

Certify Once, Trust Anywhere -- Modular Certification of Bytecode Programs for Certified Virtual Machine
Yuan Dong, Kai Ren, Shengyuan Wang, and Suqin Zhang

Abstract: Bytecode (such as JAVA bytecode and .NET CIL) and virtual machine are the key technologies for hardware- and operating system-independence. Although some efforts have been made to build logic system for bytecode programs, modular certification of bytecode still remains challenging. Moreover, certified programs will still get stuck due to the virtual machine faults. To overcome these challenges, this paper presents a logic system to verify bytecode programs with their running environment.We define a Hoare-style logic system which fully supports abstract control stacks and unstructured control flows for modular certification of bytecode programs. We also implemented a certified stack-based virtual machine with simulation relation proof. This logic system guarantees that a certified bytecode program will run on the certified virtual machine without getting stuck unless hardware faults occur. We prove the soundness and demonstrate its power by certifying some example programs with the Coq proof assistant. This work not only provides a solid theoretical foundation for reasoning about bytecode programs, but also gains insight into building proof-preserving compilers.

Key words: Modular Certification; Bytecode; Hoare-like Logic; Certified VM; Simulation Relation

相关链接

Tech. Report: PDF Format

---