Toward a Verified Software Toolchain for Java
David Pichardie · HAL (Le Centre pour la Communication Scientifique Directe) · 2012
Software are increasingly complex and are unavoidably subject toprogramming errors (a.k.a. bugs). The problem is well known andmany techniques have been developed in order to reduce the numberof bugs in a program. Among them, this document specially studiesautomatic verification techniques that operate at compile timeand that aim at catching all errors of a certain kind: staticanalyses and type systems. For example, we can rely on aninformation flow type system to verify, before running ordistributing a program, that it does not leak confidentialinformation to the external environment.One concern we can have is about the reliability of such averification. Indeed, verification tools are themselves complexsoftwares. Moreover they make assumptions about the executionmodel of programs but this model is itself an abstraction of thereal compiled code that is run at the end. Therefore the wholesoftware toolchain of a programming language requiresreliability. Our ultimate objective is to build such a toolchain for the Javaprogramming language. Our challenge here is to build a verifiedplatform: each components (transformation, verification tools)should be formally specified in an expressive logic andcorrectness of the implementation of these components should berigorously proved. Proof assistants are of special interest forthese tasks: they provide a very rich specificationlanguage (based for example on high- order logic) with anautomatic mechanism to check validity of proofs. The proof we areinterested in are specially long and too error-prone to be fullyverify at hand. Proof assistants allow for writing programs (herecompilers and verification tools), their specification, and thecorresponding correctness proof in a unified, logicalframework. Several of them provide an extraction mechanism thatautomatically generates executable code that fulfills theformalized specification.We mainly focus on Java because it is a modern language withseveral challenging features: security mechanisms, type andmemory safety, modularity. Still many facets of our work are notfully specific to this programming language. The object-orientedprogramming paradigm is for example quite orthogonal in thiswork. This document will summarise seven years of my researchwork around this objective. As we will see in conclusion the roadis still long to achieve our goal but we already have learnt someinteresting lessons that we will share here.