Tool-Assisted Specification and Verification of Typed Low-Level Languages

摘要

Bytecode verification is one of the key security functions of several architectures for mobile and embedded code, including Java, Java Card, and .NET. Over the past few years, its formal correctness has been studied extensively by academia and industry, using general-purpose theorem provers. The objective of our work is to facilitate such endeavors by providing a dedicated environment for establishing the correctness of bytecode verification within a proof assistant. The environment, called Jakarta, exploits a methodology that casts the correctness of bytecode verification relatively to a defensive virtual machine that performs checks at run-time and to an offensive one that does not; it can be summarized as stating that the two machines coincide on programs that pass bytecode verification. Such a methodology has been used successfully to prove the correctness of the Java Card bytecode verifier and may potentially be applied to many similar problems. One definite advantage of the methodology is that it is amenable to automation. Indeed, Jakarta automates the construction of an offensive virtual machine and a bytecode verifier from a defensive machine, and the proofs of correctness of the bytecode verifier. We illustrate the principles of Jakarta on a simple low-level language extended with subroutines and discuss its usefulness to proving the correctness of the Java Card platform.