Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine

摘要

Bytecodes and virtual machines (VM) are prevailing programming facilities in contemporary software industry due to their ease of portability across various platforms. Thus, it is critical to improve their trustworthiness. This paper addresses the interesting and challenging problem of certifying bytecode programs over certified VMs. Our solutions to this problem include: 1) A logical systems (CBP) for a bytecode machine is built to modularly certify bytecode programs with abstract control stacks and unstructured control flows, 2) and the corresponding stack-based virtual machine is implemented and certified, 3) a simulation relation between bytecode program and VM implementation is developed and proved to achieve the objective that once some safety property of a bytecode program is certified in CBP system, the property will be preserved on any certified VM. 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.