Wiki Agenda Contact English version

Vérification déductive de programmes

Présentation

A foundation step of the team is the PhD thesis of Jean-Christophe Filliâtre [1] that proposes to establish soundness of a program with imperative features (assignments, while loops, but also exceptions and exception handlers) by means of a translation into an equivalent purely functional program with logical annotations. Such an annotated functional program is very well-suited to be expressed in Coq's type theory, hence this approach allowed for the first time to prove imperative programs with Coq [a].

Following this thesis, a new tool called Why was developed. It takes as input an imperative program and a specification that this program is expected to fulfil. It produces on one hand a set of verification conditions (VCs): logical formulas which have to be proved in the Coq system ; and on the other hand a Coq-term which contains a functional translation of the imperative program and a proof of correctness of this program based on the VCs. It was early remarked that this tool was independent of Coq, because the VCs can be validated in other interactive tools or with automatic provers. This multi-prover architecture is a powerful feature of Why: it spreads this technology well beyond the Coq community.

Why and Frama-C

The Why platform

Since 2002, we tackle programs written in mainstream programming languages. We first considered Java source code annotated with JML (Java Modeling Language). This method was implemented in a new tool called Krakatoa [2]. The approach is based on a translation from annotated Java programs into the specific language of Why, we then can reuse Why's VCG mechanism and choose between different provers for establishing these VCs. From 2003, we followed the same approach for programs written in ANSI C [3].

The combination of the Why VC generator and the front-ends dealing with C or Java form a tool box for program verification, called the Why platform. Its overall architecture is shown on the figure on the right. Nowadays, the front-end for C is in fact integrated in the Frama-C environment for static analysis of C programs, which was developed by the CEA-List in collaboration with us. Frama-C has an open architecture, structured as plugins around a shared kernel, and deductive verification of C code can be done using Why via the Jessie plugin. The annotation language for C source is also designed in collaboration with CEA, and called ACSL [4].

The central issue for the design of our platform is the modeling of memory heap for Java and C programs, handling possible aliasing (two different pointer or object expressions representing the same memory location): the Why VC generator does not handle aliasing by itself, indeed it does not support any form of complex data structures like objects, structures, pointers. On the other hand, it supports declaration of a kind of algebraic specifications: abstract data types specified by first-order functions, predicates and axioms. As a consequence, there is a general approach for using Why as a target language for programming the semantics of higher-level programming languages [b]. The Krakatoa and the Jessie memory models are inspired by the `component-as-array' representation due to Bornat, following an old idea from Burstall, and commonly used to verify pointers programs [c] . Each field declaration f in a Java class or a C structure introduces a Why variable Mf in the model, which is a map (or an array) indexed by addresses. We extended this idea to handle Java arrays and JML annotations [10] and pointer arithmetic in C [3].

An important difficulty with programs handling pointers is to specify side-effects of a function or a method. The annotation languages offer the assigns clauses in specifications in order to delimitate the part of memory which is modified by a function or a method. We proposed an original modeling for such clauses [d] [3].

This kind of memory model does not scale up well for large programs. We designed an improved modeling of memory heap incorporating ideas from static analysis of memory separation, and from Reynolds' separation logic. Experiments on a C code proposed by Dassault Aviation were succesful [e], [f].

The use of Why as intermediate language opens interesting new approaches for reasoning on programs. We studied the specification of global properties, by reuse of the validation term of Why in order to define a model of each function, and then express and prove properties of functions composition. Such an approach was investigated by J. Andronick in the framework of proofs of security properties on smart cards [g], [h]. We also proposed a way to handle the Java Card transaction mechanism (a specificity of Java Card memory with both persistent and volatile parts), by indeed generating a Why model on-the-fly for each Java Card applet [i], thanks again to the flexibility of the approach using Why as an intermediate language.

Applications and case studies

The techniques we are developing can be naturally applied in domains which require to develop critical software for which there is a high need of certification.

The Krakatoa tool was successfully used for the formal verification of a commercial smart card applet [j] proposed by Gemalto. This case study have been conducted in collaboration with LOOP and Jive groups. Banking applications are concerned with security problems that can be the confidentiality and protection of datas, authentication, etc. The translation of such specifications into assertions in the source code of the program is an essential problem. We have been working on a Java Card applet for an electronic purse Demoney [k] developed by the company Trusted Logic for experimental purpose. Other Java Card case studies have been conducted in collaboration with Gemalto by J. Andronick and N. Rousset, in particular on global properties and Java Card transactions [g] , [i].

To illustrate the effectiveness of the approach on C programs, T. Hubert and C. Marché performed a full verification of a C implementation of the Schorr-Waite algorithm [l], using Coq for the proofs. This is an allocation-free graph-marking algorithm used in garbage collectors, which is considered as a benchmark for verification tools. Other industrial case studies have been investigated by T. Hubert (with Dassault Aviation) [f] and by Y. Moy (with France Telecom) [m],[n].

Personnes

Martin Clochard, Jean-Christophe Filliâtre, Léon Gondelman, Claude Marché, Guillaume Melquiond, Andrei Paskevich

Anciens contributeurs

Romain Bardou, François Bobot, Paolo Herms Johannes Kanig, Kalyan Krishnamani, Asma Tafat,

Développements de logiciels

Collections de programmes prouvés

Contrats

Publications de référence

[1]
J.-C. Filliâtre. Verification of Non-Functional Programs using Interpretations in Type Theory, in: journal of Functional Programming, July 2003, vol. 13, no 4, p. 709-745. http://www.lri.fr/~filliatr/ftp/publis/jphd.pdf
[2]
C. Marché, C. Paulin-Mohring, X. Urbain.The Krakatoa Tool for Certification of Java/JavaCard Programs annotated in JML , in: Journal of Logic and Algebraic Programming, 2004, vol. 58, no 1-2, p. 89-106.http://krakatoa.lri.fr
[3]
J.-C. Filliâtre, C. Marché.Multi-Prover Verification of C Programs, in: 6th International Conference on Formal Engineering Methods, Seattle, WA, USA, J. Davies, W. Schulte, M. Barnett (editors), Lecture Notes in Computer Science, Springer, November 2004, vol. 3308, p. 15-29.http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz
[4]
P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto.ACSL: ANSI/ISO C Specification Language, 2008.http://frama-c.cea.fr/acsl.html

Autres publications liées à la thématique

[a]
J.-C. Filliâtre. Formal Proof of a Program: Find, in: Science of Computer Programming, 2006, vol. 64, p. 332-240. http://www.lri.fr/~filliatr/ftp/publis/find.pdf
[b]
C. Marché.Preuves mécanisées de Propriétés de Programmes, Université Paris 11, December 2005, Thèse d'habilitation.
[c]
R. Bornat.Proving Pointer Programs in Hoare Logic, in: Mathematics of Program Construction, 2000, p. 102-126.
[d]
C. Marché, C. Paulin-Mohring.Reasoning about Java Programs with Aliasing and Frame Conditions, in: 18th International Conference on Theorem Proving in Higher Order Logics, J. Hurd, T. Melham (editors), Lecture Notes in Computer Science, Springer, August 2005, vol. 3603, p. 179-194.http://www.lri.fr/~marche/marche05tphols.ps
[e]
T. Hubert, C. Marché.Separation Analysis for Deductive Verification, in: Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007, p. 81-93.http://www.lri.fr/~marche/hubert07hav.pdf
[f]
T. Hubert.Analyse Statique et preuve de Programmes Industriels Critiques, Université Paris-Sud, June 2008, Thèse de Doctorat.http://www.lri.fr/~marche/hubert08these.pdf
[g]
J. Andronick, B. Chetali, C. Paulin-Mohring.Formal Verification of Security Properties of Smart Card Embedded Source Code, in: International Symposium of Formal Methods Europe (FM'05), Newcastle,UK, J. Fitzgerald, I. J. Hayes, A. Tarlecki (editors), Lecture Notes in Computer Science, Springer, July 2005, vol. 3582.
[h]
J. Andronick.Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation, Université Paris-Sud, March 2006, Thèse de Doctorat.
[i]
C. Marché, N. Rousset.Verification of Java Card Applets Behavior with respect to Transactions and Card Tears, in: 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, D. V. Hung, P. Pandya (editors), IEEE Comp. Soc. Press, September 2006.
[j]
B. Jacobs, C. Marché, N. Rauch.Formal Verification of a Commercial Smart Card Applet with Multiple Tools, in: Algebraic Methodology and Software Technology, Stirlinqg, UK, Lecture Notes in Computer Science, Springer, July 2004, vol. 3116.
[k]
V. Chaudhary.The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A Case Study, IIT internship report, July 2004, Technical report.
[l]
T. Hubert, C. Marché.A case study of C source code verification: the Schorr-Waite algorithm, in: 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, B. K. Aichernig, B. Beckert (editors), IEEE Comp. Soc. Press, September 2005.http://www.lri.fr/~marche/hubert05sefm.ps
[m]
Y. Moy.Automatic Modular Static Safety Checking for C Programs, Université Paris-Sud, January 2009, Ph. D. Thesis.http://www.lri.fr/~marche/moy09phd.pdf
[n]
Y. Moy, C. Marché.Modular Inference of Subprogram Contracts for Safety Checking, in: Journal of Symbolic Computation, 2010, vol. 45, p. 1184-1211.http://hal.inria.fr/inria-00534331/en/