Long term plans

One promising solution to the problem of verification of code coming from untrusted sources is the approach known as Proof Carrying Code (PCC). According to the PCC approach, mobile code is supplied with a formal proof that it satisfies a specification defined by the host system, which will then simply check the proof, to ensure that the code complies with its policy. One step forward is the idea of extending compilers with proof-generation capabilities (certifying compiler). In most current (experimental) implementations of the PCC idea, properties expressed in specifications are essentially type properties and certification boils down to type inference and verification.

Several techniques are available to improve the specification and certification capabilities of a PCC system. These include proof systems, model checking and dataflow analysis. We believe that abstract interpretation is now scientifically mature, although not yet fully explored in the context of automatic program certification. Abstract interpretation provides both a general enough setting where different type systems, proof methods, and dataflow analysis techniques can be reconstructed and combined, and a strong enough theory to assist in the correct specification and implementation of program certification systems. On one side, abstract interpretation can be viewed as a common interface for validating code by standard program analysis, proof methods, and type-based validation methods. On the other side, it is particularly adequate to cope with highly dynamic systems. Properties which need to be proved are in fact subject to change, because of the evolution of the environment. Several systematic design techniques are available (systematic design of the abstract semantics, systematic design of domains from the property of interest) to make it easier the adaptation to new requirements. Moreover, a program certifier which is systematically derived from the concrete language semantics is more reliable and flexible. Finally, abstract interpretation based certification methods are intrinsically modular (if the collecting semantics is compositional). This is of course relevant to the issue of scalability of the techniques.

Some of our current activities are relevant to the applicability of abstract interpretation techniques to certification in a PCC approach. In particular:

• Our attempt to better understand and to make some experiments with assertions as abstract domains, specification languages and verification based on the corresponding abstract semantics, if successful, will make it possible to reconstruct assertion based verification methods as instances of a more general method. In particular we will be able to understand the limits of the approach, typically in terms of constraints on the specification language.
• The combination of partial evaluation and analysis, which is essentially partial evaluation of an interpreter obtained by combining (by a sort of reduced product operation) the standard interpreter and an abstract interpreter, can be viewed as a method to generate at the same time the compiled code and the abstract property. One can build on this idea to define a certifying compiler, which generates a proof that the inferred property satisfies the specification.