Machine-checked Verified _mJava Compiler Targeting Micro-Dalvik Virtual Machine

A compiler is key system software which translates source code written in high-level programming language into object code often having a binary form which is executable on the target platform. High-level languages are, however, complex and poorly specified often in natural languages. Their involved and ambiguous semantics makes it difficult to know exactly what language constructs mean to design their implementations correctly for compiler writers. Moreover, a compiler is itself necessarily a large complex piece of software. So even if it were possible to have the exact meaning of a high-level language, it is impossible to have any confidence that a compiler correctly implements this meaning. Therefore, even though substantial tests have been performed on a commercial-off-the-shelf compiler before it is delivered, it still has bugs. Compiler bugs could result in financial loss, and even severe injury or loss of life, especially for safety-critical applications. The compiler is not trustworthy, which makes almost all the efforts devoted into verifying the high-level language programs come to be in vain. Formal methods provide what is considered to be the strictest approach to constructing trusted software and thus it is necessary to formally prove the correctness of a compiler.Using the idea of the semantics equivalence (homomorphism) that the correctness of a compiler is specified by relating a source program to its target program with respect to their semantics, this paper presents a machine-checked verified compiler whose source language, mJava, includes the features of Java which are important for a practical imperative object-oriented (OO) language, and whose target platform is a virtual machine (VM) of register-based architecture, Micro-Dalvik, which is a subset of Android Dalvik VM. To realize this purpose this paper covers the following three issues.(1) Machine-checked formal semantics of both mJava source language and Micro-Dalvik VM target language.The Java subset this paper considering here includes core features of an OO language containing encapsulation, inheritance, method overloading, method overriding, and exception handling, besides those basic grammar constructs such as blocks, sequences, conditions, loops, etc. After introducing the abstract syntax this paper inductively specifies the semantics rules for each abstract grammar construct, thus presenting the big-step operational semantics of mJava language. The type rules and well-formedness of mJava are also defined.The instruction set of Micro-Dalvik is more abstract than comparable Dalvik VM to obtain clarity of its semantics, also supporting encapsulation, inheritance, method overloading, method overriding, and exception handling. After describing the runtime state this paper defines the state transition function and relation of single-step execution. The semantics of the program is the relation for any finite number of steps which is the reflexive transitive closure of the one-step state transition relation.(2) The compilation from mJava to Micro-Dalvik and its correctness proofThe compiler operates in two stages. First it replaces the names of local variables by their corresponding indices and hence translates mJava into an intermediate language program, Ji_prog. Then it generates the Micro-Dalvik VM instructions and the exception table. After defining the operational semantics of Ji prog the correctness of the two stages is formulated in terms of the preservation of the semantics and is proved respectively, and thus the correctness of compiling mJava to Micro-Dalivk is proved.(3) The Micro-Dalvik bytecode verifier and the type-preserving compilationThe bytecode verifier is a key constituent for Dalvik VM and its primary task is to do type checking. This paper presents a further study for the Micro-Dalvik VM from the point of view of type. Taking the approach of a data flow analysis the Micro-Dalvik VM's type system is designed and its soundness is proved, and then an executable bytecode verifier is realized and its correctness is also proved. Finally this paper proves that compiling well-typed mJava programs generates well-typed Micro-Dalvik VM programs by proving that the generated Micro-Dalvik VM programs pass bytecode verification. Thus the semantics-preserving compiler guarantees type soundness.In summary, this paper machine-verifies a mJava compiler targeting Micro-Dalvik VM with the support of the theorem proof assistant Isabelle/HOL, and this semantics-preserving verified compiler generates well-typed target programs for well-typed source programs. Meanwhile, it presents a relatively complete VM formal model of register-based architecture. This model includes formal semantics, the type system and a bytecode verifier. The soundness of the type system and the correctness and the bytecode verifier are both proved. Finally, this paper indicates that the feasibility of machine-verifying a complex program which is a practical OO language compiler using Isabelle/HOL. The definitions and proofs are of clarity, easy to extend and maintain, and thus it is potential to be applied in the software development for safety-critical industries.