OSIS 2017 - Journée Frama-C et SPARK - Analyse formelle et preuve pour les programmes C et Ada

Les 11 conférences de cette journée de l’OSIS le 30 mai 2017 ont été très riches en enseignements. D’une durée de 30 minutes et en anglais, elles ont été l’occasion d’aborder les réussites et les difficultés de l’application des méthodes formelles en entreprise avec SPARK et Frama-C.

Deductive Verification in Frama-C and SPARK 2014: Past, Present and Future - Claude Marché (Inria)

La vérification déductive consiste à élaborer des spécifications formelles des comportements fonctionnels d’un programme. Il s’agit alors de procéder à une démonstration (au sens mathématique) de la correction (absence d’erreurs) et de la complétude (toutes les fonctionnalités spécifiées sont bien implémentées) pour vérifier le programme. Les langages Ada et C ont tous les deux des outils de vérification formelle depuis les années 90. Contrairement à SPARK qui a toujours été la référence en ce domaine pour Ada, C a connu plusieurs outils avant d’arriver à Frama-C. Dans les années 2000 un outil non lié à un langage en particulier est né : Why. Il a connu une mise à jour importante dans les années 2010, nommée Why3. Il permet d’interfacer les deux outils SPARK et Frama-C avec des solvers SMT, des assistants de preuves, etc.

Il y a deux grandes catégories de vérification : statique et dynamique. L’analyse statique est en générale plus efficace et permet de trouver plus de bogue, mais il est parfois nécessaire de procéder à une analyse dynamique.

Depuis l’ajout de structures natives permettant la programmation par contrat dans la version 2012 d’Ada, et de par ses spécifications plus rigoureuses que celles du C, il y a moins de difficultés à utiliser des méthodes formelles avec SPARK qu’avec Frama-C.

From Learning Examples to High-Integrity Middleware, Comparing ACSL and SPARK - Christophe Garion, Jérôme Hugues (ISAE)

PolyORB-HI est un intergiciel de haute intégrité sous licence GLPv3+ ayant pour but de prouver formellement l’absence d’erreurs et la correction des contrats, établis dans le code source, d’un logiciel en exécution. Il doit être utilisé avec Ocarina, un « compilateur » de modèles ADDL, ce dernier étant un langage de description d’architecture système destiné au monde de l’embarqué.

Il dispose de deux implémentations : une en C et une en Ada, mais il n’est utilisable efficacement que sur des sous-ensembles de ces langages, pour le moment. Par exemple, le code Ada ne doit pas utiliser de pointeurs ou d’allocation dynamique, cela facite en effet l’établissement de la preuve. La situation est bien plus compliquée en C, car les programmeurs expérimentés de ce langage ont l’habitudes d’utiliser de nombreuses astuces de codage dans un but de performance. De plus, certaines constructions habituelles du C, tels que le pointeur non typé (void *) nécessitent de réécrire le code si on veut pouvoir prover le processus d’exécution correspondant.

L’autre point de cette conférence est le commencement de la rédaction de SPARK by example sur le modèle de ACSL by example, qui est un ouvrage de référence destiné aux débutants. Une première étape de transposition naïve du code C en code SPARK a été faite sur quelques examples. Il est nécessaire ensuite de réécrire le code SPARK en utilisant les idiomes propres au langage. Deux exemples ont été présentés durant le cours : une fonction d’égalité entre deux tableaux, et la fonction d’inégalité entre deux tableaux.

Implementing Formal Code Verification: Feedbacks from Thales Early Adopters - Jean-Marc Mota (Thales Research & Technologies)

Chez la société Thales, 3 projets ont implémenté des méthodes de vérification formelle de code. Le premier consistait en un développement de bibliothèques de sécurité, et le client a demandé à ce que les méthodes formelles soient utilisées. L’équipe de développement a décidé d’utilisé Frama-C/ACSL pour répondre au besoin du client. Le deuxième projet a été porté par la section Thales Air System pour le développement logiciel de défense. L’équipe a utilisé dans ce cadre SPARK 2014, car le client a exprimé comme besoin le respect des standards de sûreté, ceux-ci recommandant fortement l’utilisation de méthodes formelles. Enfin, le dernier projet est le développement d’un logiciel de radar, toujours en SPARK 2014. La motivation a été d’ajouter de la robustesse au programme.

D’après l’expérience des équipes de Thales, l’usage des langages formels a été bien accueilli par les développeurs. Cela ne remplace pas les méthodes de génie logiciel (que faut-il formaliser ?). Débuter avec la vérification des propriétés fonctionnelles n’est pas une bonne idée ; ajouter des annotations pour aider les assistants de preuve ou les démonstrateurs automatiques n’est pas facile.

Thales préconise plutôt une approche incrémentale d’insertion de code formellement analysée, dans un sous-ensemble bien délimité du code existant. Il est également utile de définir des niveaux de formalisation afin de ne pas consacrer trop de ressources à cette tâche pour un gain pas nécessairement utile selon le contexte. Enfin, la tentative de vérifier formellement une grande base de code existante n’a pas été concluante.

From 80% to 99% : An Industrial Collaboration for Automating Frama-C/WP - Loïc Correnson (CEA List)

L’institut List du CEA a travaillé avec la société Airbus afin de mettre à jour leur chaîne d’outils de vérifications formelles. Airbus utilisait CAVEAT, un outil destiné au langage C, qui présentait comme défaut l’exigeance de règles particulièrement strictes en plus du fait qu’il pose comme hypothèses que les programmes n’ont pas d’erreurs à l’exécution. Cet outil est donc lourd et obsolète, mais atteint tout de même un taux d’automatisation de 96 %. Alors l’institut proposa d’utiliser le module WP de Frama-C. Afin d’en tester l’efficacité, 16 bancs d’essai particulièrement difficiles d’après l’expérience d’Airbus ont été conçu. L’objectif est d’atteindre un taux d’automatisation supérieur à 96 %. Les résultats après un premier essai ont été particulièrement décourageant : le taux d’automation était inférieur à 50 % sur les 4 bancs d’essai les plus simples.

Après plusieurs années de développement a essayé de corriger ce problème, les équipes du List ont, pour résoudre ce problème, conçu une bibliothèque permettant de définir une représentation logique intermédiaire dans Frama-C/WP : QED. Disponible sous licence LGPLv2 sur GitHub, elle procède a d’importantes simplification aggressives combiné à une approche systématique. Grâce à cette bibliothèque et au suivi des tickets sur un dépôt Git, l’équipe travaillant sur ce problème a réussi à atteindre un taux d’automatisation de plus 99 % sur les 16 bancs d’essai, le dernier pourcent restant étant laissé au soin d’un assistant de preuve interactif.

Replicated Synchronization for Imperative BSP Programs - Arvid Jakobsson (Huawei Technologies France)

L’utilisation de méthodes formelles dans les logiciels embarqués exploitant une architecture parallèle permet d’assurer leur sûreté et leur efficience. Un des modèles de développement utilisé pour concevoir des algorithmes parallèles est le Bulk Synchronous Parallel (BSP), avec une structure simple de synchronisation. L’une des bibliothèques les plus utilisées pour implémenter ce modèle en C est BSPlib. L’objectif que s’est fixé l’équipe d’Huawei est de vérifier les programmes utilisant cette bibliothèque, notamment si la synchronisation se déroule correctement.

L’exemple donné pour illustrer le sujet est l’usage d’une boucle boguée exécutée par plusieurs processus parallèles, suivant un modèle Simple Program Multiple Data (SPMD). L’affichage réalisé dans la boucle était en effet désynchronisé. La première idée naïve qui peut venir à l’esprit pour résoudre cela est d’introduire un délai pour réaliser des affichages synchronisés. Le problème est que le temps lui-même a besoin d’être synchronisé entre les différents processus, et ce n’est pas toujours le cas.

En réalité, on peut définir la source du problème de synchronisation dans ce cas comme étant l’utilisation de valeurs locales au processus pour effectuer une synchronisation globale. Ainsi, en formulant ainsi le problème, on peut vérifier avec les méthodes formelles si les programmes utilisant BSPlib présentent ce bogue ou non. En en analysant plusieurs, l’équipe d’Huawei a remarqué que ce problème de synchronisation survenait assez rarement, car les développeurs expérimentés ont tendance à utiliser, parfois inconsciemment, un modèle de synchronisation intitulé synchronisation répliquée (Replicated Synchronisation). Elle consiste à ce que toutes les conditions et les boucles soient PID-independant, c’est-à-dire qu’elles n’utilisent pas données locales au processus considéré. Elle résulte donc de bonnes pratiques de génie logiciel.

Specifying and Proving Correctness of Linux Kernel Components with ACSL - Alexey Khoroshilov, Mikhail Mandrykin (Linux Verification Center, ISPRAS)

Cette conférence expose le retour d’expérience sur la tentivate de vérifier formellent le module de sécurité de Linux (Linux Security Module (LSM)). Pour mener à bien ce essai, l’équipe du Linux Verification center a dû personnaliser le modèle de la politique de sécurité ainsi que le modèle de sécurité lui-même de Linux. L’objectif est de prouver l’absence d’erreurs à l’exécution ainsi que la conformité du module au modèle fonctionnel. L’outil utilisé pour cette tâche est Frama-C avec le module Jessie (WP n’était pas assez mature à l’époque du projet).

Plusieurs difficultés sont évidemment apparues. Elles sont principalement dûes aux techniques et astuces complexes et compliquées utilisées dans la programmation bas-niveau. Des exemples sont donnés avec les fonctions memcpy et memset. La première passe les tests et les vérifications, mais pas la deuxième alors qu’elle est correcte. En effet, l’outil signal un problème de dépassement de tampon (overflow), mais celui-ci a été réalisé intentionnellement dans un but de performance.

Afin de surmonter ces obstacles, l’équipe a développé un ensemble d’outils nommé Astraver. Il utilise un modèle d’entier composite, qui consiste à définir de nouvelles annotations au code combiné avec des fonctions fantômes (des fonctions qui ne peuvent être compilées mais qui sont utilisées dans les assertions).

CubedOS: A Verified CubeSat Operating System - Carl Brandon, Peter Chapin (Vermont Technical College)

CubedOS est un système d’exploitation généraliste destiné au système de vol de CubeSat, un nano-satellite. Écrit avec SPARK, il a été soumis aux méthodes de vérification formelles : plus de 98 % des lignes de code le constituant ont été prouvées comme ne contenant pas d’erreurs à l’exécution ; seulement 102 lignes ne le sont pas. Reposant sur une architecture modulaire, il permet d’ajouter facilement des fonctionnalités sans nécessité particulière.

Les modules communiquent par passages de messages dans des boîtes aux lettres (numériques !) et s’exécutent de façon concurrente. Les messages sont constitués de tableaux d’octets non structurés, ce qui améliorent la flexibilité au détriment de la surêté, car l’on perd alors les garanties données par le système de typage. Cependant, les développeurs de CubedOS ont estimé que c’était un compromis acceptable.

La mission Lunar IceCube est la première qui a vu un CubeSat lancé dans l’espace avec le système CubedOS. Cette mission a été un succès, elle a permis de récupérer des photographies prises avec la caméra de 20 dollars embarquée sur le nano-satellite. Un système d’exploitation concurrent existe et est édité par la NASA : cFE/CFS. Il est écrit en C et, contrairement au CubedOS, n’a pas été vérifié formellement.

Remove Before Flight: Defect-Free Software and Agile Development in SPARK 2014 - Martin Becker (TU München)

L’équipe du TU München s’est lancé un défi particulièrement intéressant : utiliser les méthodes formelles avec SPARK 2014 dans un projet de seulement 3 mois avec 2 développeurs. Il s’agit de lancer un ballon-sonde équipé d’un drone. En effet, il a été constaté que les ballons-sondes, et surtout leurs capteurs, ne sont pas retrouvés pour une grande majorité. L’utilisation d’un drone permettrait de pallier ce problème.

Dû au peu de moyen alloué à ce projet, il faut trouver un moyen de vérifier autant que possible la conformité du système embarqué, sans avoir à faire de tests en condition réelle… puisqu’il n’y a qu’un seul essai. D’où l’usage des méthodes formelles avec SPARK 2014, mais d’une manière un peu particulière. En effet, le but était de retirer les bogues du programme, en espérant que plusieurs d’entre eux seraient détectés à la phase d’analyse statique du code, un peu durant les tests d’intégration (qui ont pour but de s’assurer que le ballon-sonde ne volera pas à plus de 100 m par exemple, car cela nécessite alors des autorisations administratives) et bien sûr qu’il ne reste plus aucun bogue lorsque le ballon décolle. À noter qu’aucun tests unitaires n’a été développé, l’accent a été mis sur les tests fonctionnels.

Les retours d’expérience de l’équipe sont que SPARK a aidé à capturer et formuler plusieurs prérequis manquants, mais que pour certains composants matériels, par exemple le GPS, il n’a pas été capable de le faire. Il a été noté que le traitement des nombres flottants est particulièrement difficile. Un bogue considérablement difficile a eu lieu à ce propos. Il arrivait à la boucle d’exécution du processeur de redémarrer durant les vérifications d’avant-vol ; ce bogue a été très difficile à reproduire, et pour cause, il s’agit en fait d’une erreur de configuration du programme d’exécution. En effet, le programme traite à un certain moment un nombre flottant dénormalisé, et le programme d’exécution considérait que le processeur ne pouvait le gérer, alors qu’en réalité il prend très bien en charge ce type de nombres.

Vient le moment fatidique du lancement du ballon-sonde : après un bon début, le drone s’est subitement mis à faire plein de cercle et s’est ensuite perdu dans l’eau sans jamais être retrouvé. Deux causes probables sont actuellement discutées sur l’origine de ce comportement erratique. Soit c’est un problème de la boussole qui a pu généré une sortie imprévue, soit c’est un problème de distortion magnétique. Malgré cet échec, l’équipe cherche à obtenir des subventions afin de retenter cette mission avec plus de ressources.

Development of Security-Critical Software with SPARK/Ada at secunet - Stefan Berghofer (secunet)

Cette présentation explique comment la société de sécurité secunet utilise SPARK pour développer des systèmes de haute sécurité. Le cas présenté est un système d’information interne basé sur des composants et découpé en deux parties principales reliées par une passerelle. Le but est d’assurer l’absence de levées d’exceptions lors de l’exécution des composants de confiance et également de garantir la conformité de certaines fonctionnalités.

L’architecture de ce système est modélisé par deux systèmes Linux : un RedLinux comportant les données sensibles et un BlackLinux connecté à Internet. Ces deux systèmes sont reliés par un composant cryptographique de confiance. Les méthodes formelles qui ont été utilisées dans ce cadre sont celles fournies par les démonstrateurs automatiques, l’utilisation des annotations dans le code ainsi que les assistants de preuve interactifs. Bien que ces derniers nécessite une intervention manuelle, secunet a déterminé qu’environ 4 à 10 % du code source ne pouvait être prouvés par les résolveurs SMT, et les annotations et fonctions fantômes sont difficiles à utiliser pour les preuves complexes.

Un exemple avec la réduction de Montgomery (multiplication rapide) a été donné, cet algorithme étant très utilisé en cryptographie. En l’occurence, libsparkcrypto a été utilisé, et l’assistant Isabelle dirigé par Why3.

Real Behavior of Floating Point Numbers - François Bobot (CEA List)

Cet exposé commence par le constat que les nombres flottants sont utilisés comme dans nombres réels par les développeurs C ou SPARK, alors qu’il y a des contre-exemples très simples montrant qu’ils ne partagent certaines propriétés, même très basiques. Par exemple : soient x et y deux nombres flottants, alors x + y = x n’implique pas que y = 0. De plus, les outils utilisant les méthodes formelles au niveau de l’état de l’art ont beaucoup de difficultés à prouver des propriétes concernant les nombres flottants. La techinque utilisée par les résolveurs SMT est le bit-blasting. Le problème est qu’elle ne scale pas du tout. Par exemple, si on additionne 8 nombres flottants dont la valeur est comprise entre 1 et 10, et qu’on veut vérifier que le résultat obtenu est bien compris entre 8 et 80, le temps pris par un SMT est de l’ordre de 3 secondes. Si on veut vérifier une propriété similaire sur 20 flottants, cela explose à 31 minutes.

Le projet SOPRANO a permis, grâce à une collaboration fructueuse, de parvenir à descendre ce temps à environ 0,1 seconde dans les deux cas, avec l’outil nommé COLIBRI. Plusieurs techniques sont utilisées : propagation précise de domaines, graphe de distance sur les nombres flottants, fonctions monotones et la linéarisation de contraines afin d’utiliser l’algorithme du simplexe (connu en optimisation linaire).

Structuring an Abstract Interpreter through State and Value Abstractions - David Bühler (CEA List)

L’interprétation abstraite est une théorie générale d’approximation des programmes informatiques, qui consistent à ne les exécuter que partiellement afin d’obtenir leur sémantique. Un vieux module Frama-C existe pour exploiter cette technique : VALUE. Il utilise des domaines abstraits pour approximer le comportement du programme analyser et déduit ensuite sa sémantique concrète en utilisant des fonctions à état. Il rapport alors toutes les opérations illégales ; tous les programmes incorrectes sont détectés, mais cela peut mener à des fausses alarmes. De nombreux domaines abstraits sont bien connus et utilisés dans ce cadre. VALUE est construit autour d’un important domaine abstrait scalable, mais il n’est pas extensible et ne traite pas les propriétés relationnelles.

D’où le développement d’un nouveau module pour Frama-C : EVA. Pour le rendre modulaire, l’idée principale est de structurer les sémantiques abstraites avec l’utilisation de valeurs abstraites et d’états abstraits. Cela permet une interaction entre les abstractions et une combinaison des domaines abstraits plus puissante. Le flux d’informations entre les domaines circulent grâce aux valeurs abstraites. EVA propose également la propagation en arrière afin d’évaluer toutes les expressions d’une instruction, permettant alors d’émettre les alarmes.

Cette journée fourmillant de connaissances techniques pointues s’est achevée sur l’annonce pour SPARK de la prise en charge future de pointeurs sûrs (ce que les développeurs du langage rechignaient à faire jusqu’ici) ainsi que la sortie le jour même de Phosphorus, une nouvelle version de Frama-C, l’équipe se donnant ensuite pour objectif de vises les logiciels non-embarqués.