A technique for obtaining trustworthy compilation based on a compilation checker (similar to a proof checker) is proposed. The transformations used in a compiler will be formally specified and verified using interpreter equivalence methods. The compiler will be instrumented to produce a trace of the transformations applied in the compilation of a given program. The compilation checker will validate the trace using the verified transformations abstracted from the compiler. This approach separated the hard problem of finding the translation from the easier problem of ensuring that the translation has been correctly done. Formal specification and verification of the compilation checker using hand proof techniques is within the current state of the art. With appropriate formally based reverse engineering techniques, the approach should be extendable to cover existing commercial quality compilers for real languages such as C and Ada.Anticipated
Benefits:The proposed work has numerous potential applications both within the government and in the civilian sector. Government applications ranging from computer security and communications to avionics for military aircraft could benefit from trustworthy compilation as could civilian applications ranging from automobiles to commercial avionics to medical devices to household appliances where compilation errors have a potential for causing injury or death.
