This paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that formal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness of the problems that PCC addresses has already brought students to show interest in this project. Traditional PCC architectures center their certificate generation mechanisms on the output of the compilation. Along the lines of recent projects, we believe that there are strong benefits in moving the certificate generation to the source code level. Because there exist good tools for source code verification and for formal verification in general, it is a feature of the Lissom platform that existing tools are used as much as possible at key points of its infrastructure. Our vision of PCC is based on the following two underlying principles: • Source level PCC is the way. It is our belief that the realistic formal verification of mobile code should be performed at source level. Programmers may be unaware of the target architecture details, and in general algorithmic constructions are expressed at source level. • Reuse as much as possible. There exist plenty of powerful tools for the formal verification of source code. Such tools already have experienced user communities, and have reached an appreciable level of maturity and flexibility that make them natural choices in the context of a source level PCC architecture. Our main goal with Lissom is to get experienced with PCC and to put it into practice. We now describe the proposed architecture for the Lissom platform (see figure below) . The Source Language and the Compiler. LISS (Language for Integers Sets and Sequences) is a non-trivial toy language that also features a realistic type system (with e.g. sets, vectors a la Java, etc.) and high-level constructs. LISS is intended here as a suitable test-bed before aiming at an industrial-level language. This language must be extended in order to provide an annotation system for the source code. In a source level PCC architecture, the compiler has to compile source code but also proofs into their machine level counterpart. A very interesting challenge is to transform a source level structural proof (proofs heavily rely on the structure of the analyzed program) into a proof that is still structurally close to the machine level code. We follow here the contributions of [1]).
Lissom is a source level PCC platform REF that outputs VCs into the Why toolset [CM09] and the Coq proof assistant [INR06] .
Lissom, a Source Level Proof Carrying Code Platform
ArXiv
ArXiv
Computer Science