Tag - frama-c

Entries feed - Comments feed

Last entries

Introduction aux méthodes formelles actualisée

Comme en 2010 et 2011, j'ai faire une intervention de 2h pour présenter les méthodes formelles à l'ESIR, école d'ingénieur de Rennes 1. J'ai un peu actualisé la présentation, je pense qu'elle est plus illustrée et j'ai introduit quelques démonstrations d'utilisation des outils. La présentation est disponible en PDF ou en source au format PowerPoint (licence Art Libre, sauf pour les illustrations, que j'ai pioché à droite et à gauche sur le web).

Note pour les libristes : la plupart des logiciels mentionnées sont libres.

Introductory slides on Frama-C

I recently made at work slides to present Frama-C: what it is, the various plug-ins and how to use the two main ones, Value analysis and WP. The examples used in the slides are also available.

The attached version is updated after fixing minor issues found by frama-c-discuss mailing list readers.

Enjoy! (and let me know if you find them useful)

Which approach for Hoare logic formal verification?

Currently, if one wants to do some program verification using Hoare logic framework, three approaches are possible:

  1. Down to code approach, when one annotates code functions with pre and post-conditions. This is the approach proposed by Frama-C on C code, SPARK on Ada code or GNATprove on Ada code. This approach has the advantage to be directly palatable to programmers because they are keeping they preferred language. Moreover, one can use such approaches on existing code, even if to fully verify it one will probably need to make some change. The downside of the approach is that the formal verification is tightly linked to the code, making the formalisation of program wide properties more complex;
  2. Abstract specification refined in implementable code, like the B Method (and its variant Event B for system specification). This approach using using pre and post-conditions but also invariants on which all the correctness of the code is built. Due to its abstract specification, it can express complex properties that help reasoning on the built program or system. However, it uses very mathematical concepts like set theory or relations which are making engineers not at ease. And the proof can be somewhat complex, involving some manual steps. Moreover, one needs to fit its development process in B approach, without reuse of existing code;
  3. A new approach proposed by Bertrand Meyer (of Eiffel fame which popularized the Design by Contract approach) which relies on pre and post-conditions on code but where such specification can use more abstract operators made available from libraries called Domain theories. The main idea is that such domain theories provide to the programmer abstract view on some domains (like maximum of an array) so formal specifications are easier to read (and thus probably more correct) and hopefully to prove.

The third approach of Meyer seems to take most advantages of the two first ones: use of current programming language so the programmer is at ease and use of abstract formalisation so the specification is easier to read and more abstract. Moreover, it relies heavily on invariants (already available in Eiffel language) so a B Method-like approach is possible. However, Meyer's approach lacks refinement capabilities of B Method. But as far as I know, refinements are rarely used in B Method, except for making difficult proofs easier by using several steps to make concrete algorithms or data structures[1].

It remains to see how it will be implemented in a tool. Formal methods effective capabilities are determined by the supporting tools. Time will tell if Meyer's approach is really useful! :-)

Note

[1] But that might make the difference between a nice approach and a usable one. ;-)

Frama-C pour l'analyse de valeur et la preuve

J'ai fait hier soir une présentation Gulliver sur Frama-C, un framework qui permet notamment de faire de l'analyse et de la preuve sur du code C. Les transparents et exemples sont disponibles (réutilisez les, c'est du Libre !).

Suite à l'annonce de ces transparents sur la liste frama-c-discuss, une très intéressante discussion a démarré sur l'utilisation concrète de Frama-C sur des codes industriels et les avantages respectifs de l'analyse de valeur et la preuve. Je recommande de lire notamment les points de vue de quelqu'un d'Atos Origin (avec des remarques encore plus précises sur la manière de faire ces analyses) et de quelqu'un de chez Dassault Aviation.

Apparemment, Frama-C est utilisé sur du code industriel et il donne des résultats. Intéressant !

Présentation de l'analyse de valeur avec Frama-C

Lundi 18 au matin, je suis intervenu dans un cours de compilation de l'ESIR (anciennement DIIC) pour présenter le framework d'analyse statique Libre Frama-C et en particulier l'analyse de valeur. Les transparents en PDF, les sources au format propriétaire et les exemples sont disponibles dans ce répertoire.

Vous pouvez facilement tester les exemples, il n'y a qu'à installer le paquet frama-c dans une Debian ou une Ubuntu. Si vous comptez venir à ma présentation de lundi 31, ne regardez pas trop en détail, sinon ça manquera de surprises. ;-)

N'hésitez pas à me poser des questions si besoin.

Looking for a C software for Formal Verification

As you probably know, I'm a huge fan of Formal Methods: use appropriate Mathematics and tools to ensure a program is correct in all possible situations. In other words, bug free software... well, sort of. :-)

The interesting side of this is that tools to apply Formal Methods have improved a lot and most of them are now Free Software. I'm maintaining a list of Free Software tools for Formal Methods (it is a wiki, you can update it!).

I would like to make an experiment with Frama-C and its plugins, especially Jessie. Frama-C is a framework for static analysis of C programs developed at CEA. Combined with the Why and Alt-Ergo tools, you can prove some properties on real C code (absence of integer underflow or overflow, absence of out-of-bound accesses, absence of NULL pointer de-referencing, program's specific properties, etc.). All those tools are Free Software and are developed in OCaml. And they now are available in Debian and Ubuntu!

I made a simple experiment last year but I would like to make a more elaborated one.

Therefore, I'm looking for a piece of C code with following criteria:

  • Free Software: I'm interested in improving software for the whole humankind; ;-)
  • Pure C code, no C++. If there is some assembly, I could work around for example by re-writting corresponding C function;
  • Code of moderate size, a few thousands line at most. It could be a sub-module or subset of a bigger code;
  • Code using mostly integers and pointers, few strings (aka char *)[1];
  • Verifying some properties on this code would be "interesting". Several possible reasons: for security or safety reasons, because the code is used in an embedded platform on which modifications are difficult once in production or simply because this code is used a lot.

If you know some software that fills those criteria, let me know through a comment or at dmentre@linux-france.org!

Notes

[1] Frama-C is a bit slow to handle strings and it can become cumbersome.

Les outils de vérification logiciel deviennent de plus en plus accessibles

Les méthodes de développement se sont un peu améliorées, mais en 2009 on développe encore du logiciel comme on le faisait dans les années 70 : on spécifie (plus ou moins), on code et on teste (ce que l'on peut). Suivant le temps, les ressources et la volonté dont on dispose, le résultat est plus ou moins réussi, voire largement utilisable (une distribution Linux fonctionne plutôt bien après tout ;-).

Mais cette approche ne permet pas de s'assurer que dans tous les cas le logiciel fonctionnera comme on l'attend. Et vu la place que prend le logiciel dans notre vie (dans les machines à laver, dans les voitures, dans les téléphones, dans nos ordinateurs de bureau, dans les trains et avions, ...), cette approche n'est pas satisfaisante. On devrait quand même être capable de faire du logiciel qui marche correctement, comme on fait des ponts et des immeubles qui ne s'effondrent pas !

C'est pour cette raison que je m'intéresse depuis pas mal de temps aux méthodes formelles. Elles consistent à utiliser les outils mathématiques pour vérifier un certain nombre de propriétés dans un programme et ainsi garantir, par construction, l'absence d'une certaine classe d'erreurs. Ces méthodes formelles sont plus ou moins compliquées à utiliser. Les plus simples sont peut-être l'utilisation des types dans des programmes en C++ ou OCaml, qui garantissent qu'on ne va pas mélanger les e-torchons et les e-serviettes. Les plus compliquées, comme la méthode B, partent d'une spécification formelle dans un formalisme mathématique précis et arrivent par raffinements successifs à un programme conforme par construction à cette spécification.

Évidemment, les méthodes formelles ne sont pas magiques ! Si vous posez mal votre problème, c.-à.d. si vos spécifications sont incorrectes, vous obtiendrez un programme qui garantit des propriétés bidons, pas très utile dans la vraie vie[1]. Mais l'utilisation de méthodes formelles oblige à réfléchir plus sérieusement à son programme et, en général, les programmes sont de meilleure qualité.

La bonne nouvelle, c'est que ces méthodes formelles deviennent de plus en plus accessibles :

  • les outils sont facilement accessibles, et de nombreux outils sont disponibles sous forme de logiciels libres (et même deviennent libres). Ainsi, je maintiens une telle liste d'outils formels ou semi-formes libres ;
  • les méthodes elle-mêmes deviennent plus accessibles, avec des approches plus « presse bouton » et des formalismes ne nécessitant pas un gros bagage mathématique.

Dans la suite de ce billet, j'insiste sur deux exemples : Frama-C et l'Atelier B.

Frama-C

Frama-C est un outil libre (sous licence GNU LGPL) développé principalement au CEA (Commissariat à l'Énergie Atomique) en partenariat avec des universités et centres de recherche (INRIA). Frama-C permet :

  • l'analyse de code C : propagation de constantes, valeurs des variables, arbre d'appel des fonctions, analyse d'impact, slicing, etc. ;
  • la preuve de propriétés sur du code C, en utilisant des programmes libres complémentaires (Why et Alt Ergo notamment).

En fait, Frama-C est un framework qui, grâce a un système d'extensions, permet de faire différentes analyses ou vérifications. Par exemple, l'analyse d'impact permet de savoir quelles variables ou structures de données sont influencés par la modification d'une variable : très utile pour l'analyse de sécurité ! Et comme Frama-C utilise une approche formelle (notamment l'interprétation abstraite), les analyses produites sont valables dans tous les cas (avec éventuellement des sur-approximations).

Avec Frama-C (et un peu d'huile de coude), on peut également prouver des propriétés sur un programme C, par exemple que telle variable entière ne débordera pas ou que telle fonction renvoie bien le résultat escompté. J'ai ainsi utilisé Frama-C pour prouver quelques propriétés sur un programme de vote électronique jouet. Ça peut-être utile d'être sûr que le gagnant calculé par le programme de vote a bien le nombre de voix le plus élevé[2]. ;-)

L'Atelier B

L'Atelier B est un environnement logiciel pour faire des spécifications et des programmes en utilisant la méthode B. Attention, l'Atelier B n'est pas un programme libre (honte à moi !) mais simplement gratuit. Seulement, lorsqu'on sait qu'il y a quelques mois à peine il était vendu 45.000 € et qu'il est utilisé pour développer des systèmes critiques comme le cœur de calcul du métro Météor, sa disponibilité devient intéressante. Enfin et surtout ClearSy, l'entreprise qui développer l'Atelier B, a une réelle ouverture vers le Libre (voir notamment la politique de distribution de l'Atelier B) avec mise à disposition de certains de ses outils en logiciels libres (licence GNU GPLv3) ou de certaines documentations en documentation libre (licence CC-BY).

L'Atelier B 4.0 est disponible en version Linux (mais aussi Windows et MacOS X). Il s'installe relativement facilement même si le script d'installation n'est pas standard. Il est fournit avec toutes les documentations (en anglais et français) nécessaires : Référence du langage B, Manuel de l'utilisateur d'Atelier B, etc.

En guise de conclusion

J'espère que ce petit billet a au moins éveillé une curiosité pour les méthodes formelles. Si vous avez des questions, n'hésitez pas à me les poser.

Notes

[1] L'article A Few Remarks About Formal Development of Secure Systems donne quelques exemples intéressant d'erreurs possibles dans des spécifications.

[2] Au passage, quelle que que soit la position qu'on peut avoir vis à vis du vote électronique, tous les systèmes de vote devraient être développés avec des méthodes formelles, condition nécessaire (mais pas suffisante) pour avoir confiance en ces programmes.