Software Verification / Vérification de logiciel

Entries feed - Comments feed

Last entries

Wed 19 Jan 2011

  • David Mentré

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.

Fri 17 Dec 2010

  • David Mentré

Présentation introductive aux méthodes formelles

J'ai fait ce soir une introduction de 2h aux méthodes formelles aux étudiants de DIIC3, étudiants en 3e année de l'école d'ingénieur de la fac de Rennes 1. Le cours dans lequel j'intervenais s'appelle Test et Qualité du Logiciel. Le formel n'est jamais que du test un peu extrémiste. ;-)

Cette présentation se veut accessible au néophyte. Après une rapide introduction et quelques exemples de bugs pour éveiller l'attention, j'aborde les quatre approches qui me semblent intéressantes à suivre : l'interprétation abstraite, le Model Checking, la logique de Hoare et les démonstrateurs de théorèmes interactifs.

Voici donc les transparents, au format PDF ou les sources au format propriétaire PPTX (LibreOffice et OpenOffice 3.2 peuvent ouvrir le fichier). Ils sont libres, sous licence Art Libre 1.3, sauf pour quelques images, pompées sur le web et propriété de leurs auteurs.

Si vous avez des questions ou si vous voulez que je vous fasse la présentation, n'hésitez pas à me contacter : dmentre@linux-france.org.

Fri 19 Nov 2010

  • David Mentré

Track artifacts of a project: the Qualifying Machine

In a recent blog post about literate programming tools, I advocated for tools that would allow programmers to track changes in a set of documents, source code, figures, test suites, etc. that makes a software. More exactly, I was saying:

Moreover, to really exploit the full potential of literate programming, one needs to produce and track dependencies between several documents. For example, if I modify the specification, I need to modify some parts of the code. Inversely, if I change my code I need to know which part of the "specification" have to be updated. This tracking between pieces of code/documentation goes to test, user documentation, code documentation, test review, Q&A documents, GUI design, mathematical scripts describing an algorithm, formal models to check the software, etc. And more importantly, if I modify a piece of this code/documentation, I need a list of all document parts I need to review and possibly update, a kind of make on steroids.

I was also saying:

Overall, one needs an integrated documentation system that is able to encompass all the kind of artefacts that make a software and that can be used to maintain those artefacts along the whole life of the software, from design to maintenance. And this system should be flexible enough to not constrain you to a fixed development environment, letting you chose the tools that you prefer.

It appears that others have the same ideas as me (as usual ;-). Recently Matteo Bordin presented the Qualifying Machine that encompasses some of those ideas.

The Qualifying Machine main idea is to provide a development environment for avionic software where one could do continuous qualification. When you modify an artifact (source code, specification document, etc.), the tool tracks all the implied changes on other artifacts and let you know what kind of action you need to do to re-qualify your software (tests to execute, formal proofs to do, etc.).

I let you look at Matteo's presentation on Agile Qualification and the Qualifying Machine to understand its details. The Qualifying Machine is currently just a few ideas with a small prototype for GnatCheck but it sounds quite interesting.

Thu 09 Sep 2010

  • David Mentré
  • 2

New paper accepted on B Method and Model checking

I proposed a paper to ITST 2010 conference and it has been accepted!

The core proposal of this paper is to link low level B Method model (B0 code) to Model checking techniques. More exactly, I propose to automatically extract a SPIN model in Promela language from a B0 model. I applied this approach on a simple model of a railway level crossing.

For further details, just read "Checking temporal properties on state based formal specification: application to railway level crossing"! ;-)

Thu 18 Mar 2010

  • David Mentré
  • 3

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.

Mon 06 Apr 2009

  • David Mentré
  • 4

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.

page 2 / 2