Discussion sur la preuve de programme

Je viens de découvrir le nouveau tutoriel Introduction à la preuve de programmes C avec Frama-C et son greffon WP et après en avoir rapidement lu une partie en diagonale¹, je me suis dit qu’il y avait matière à discussion.

Personnellement, je trouve qu’essayer de prouver un programme C (à grande échelle) est à peu près aussi désespéré que d’essayer de s’assurer que 30 gosses de 3-5 ans ne vont pas se blesser en passant une journée dans un atelier d’ébéniste mal rangé avec un seul encadrant. On le fait parce c’est de loin l’endroit que l’on connais le mieux et qu’on est bien rodé, mais il n’empêche que ça reste difficile et épuisant. Je sais bien qu’un programme C prouvé sera toujours mieux qu’un programme non prouvé, mais je reste étonné par la manière dont le problème est souvent abordé.

Je serais plutôt du genre à préférer un langage qui syntaxiquement et/ou sémantiquement ne permet pas de faire certaines conneries (pointeurs nuls, utilisation de mémoire désallouée, division par zéro, etc) plutôt que d’accepter ces programmes pour ensuite essayer de vérifier qu’ils n’ont pas ces problèmes. En gros, avoir un langage A pour lequel "il n’existe pas de programme A valide qui exhibe le problème X". Je sais bien que ça ne résout pas complètement le problème initiale de vérifier qu’un programme dans son entièreté vérifie certaines spécifications, mais ça reste un grand pas vers le généralisation de programmes qui ont moins de bugs, et ça aide certainement à se focaliser sur ce qui est actuellement important que sur les centaines de choses permis qu’il faut ensuite interdire.

Un autre point qui me chiffonne est la supposition que les spécifications sont parfaites et qu’elles ne contiennent aucun bug. Si c’est vraiment le cas², est-ce qu’il ne serait pas plus intéressant que le compilateur écrive lui-même le code à partir des spécifications? Si je dis ça, c’est que les spécifications (formelles) d’un programme sont la plupart du temps écrites dans un langage déclaratif plus expressif que le C. Si on fait plus confiance en ce code, la "bonne" approche ne serait-elle pas d’écrire le programme dans un langage similaire et de laisser le compilateur faire son travail?

Je serais plutôt du genre à préférer un langage qui syntaxiquement et/ou sémantiquement ne permet pas de faire certaines conneries (pointeurs nuls, utilisation de mémoire désallouée, division par zéro, etc) plutôt que d’accepter ces programmes pour ensuite essayer de vérifier qu’ils n’ont pas ces problèmes. En gros, avoir un langage A pour lequel "il n’existe pas de programme A valide qui exhibe le problème X".

Sauf que tu oublies que dans certains secteurs, du genre l’aéronautique, si ton programme est un peu critique (genre le contrôle moteur), les contraintes de développements seront très très forts rendant les alternatives au C non viables. Car il faut garantir une prédictibilité du résultat en toute circonstance, comment tu t’assures que la JVM ou l’interpréteur Python ne vont pas planter ? Comment tu t’assurer que le processeur ne réarrange pas les instructions ? Tu auras donc des puces pas assez puissantes et certifier Python ou la JVM est une tâche bien trop difficile pour un gain discutable.

On parle quand même d’un secteur où l’allocation dynamique de mémoire est interdite pour les programmes critiques.

Prouver que le programme en C respecte la spec est bien plus abordable et fiable. Ce qui peut paraître contradictoire mais c’est ainsi.

Un autre point qui me chiffonne est la supposition que les spécifications sont parfaites et qu’elles ne contiennent aucun bug. Si c’est vraiment le cas2, est-ce qu’il ne serait pas plus intéressant que le compilateur écrive lui-même le code à partir des spécifications? Si je dis ça, c’est que les spécifications (formelles) d’un programme sont la plupart du temps écrites dans un langage déclaratif plus expressif que le C. Si on fait plus confiance en ce code, la "bonne" approche ne serait-elle pas d’écrire le programme dans un langage similaire et de laisser le compilateur faire son travail?

Dans l’aéronautique, que je connais bien, si tu génères du code, la génération du dit code (donc le générateur) doit être prouvé ce qui est là aussi pas si trivial que cela étant donné les contraintes du secteur.

Concernant les specs, ce n’est pas pour rien que les parties critiques de l’avion sont réalisés par deux constructeurs différents et que tout cela est audité par l’assembleur (Airbus ou Boeing en général) et les autorités. Cela permet d’avoir beaucoup de monde qui relisent les specs et qui peuvent remonter les anomalies de la spec (ou délimiter les interprétations possibles).

Salut,

Il y a en effet matière à discussion. Je souhaite rebondir en particulier sur le passage suivant.

Les spécifications n’ont pas besoin d’être « parfaites » dans l’absolu.

Une spécification est d’ailleurs essentiellement la définition du comportement attendu en rapport avec les besoins. Si ta spécification ne répond pas au besoin, tu auras beau prouver tout ce que tu veux, tu n’obtiendras rien d’intéressant avec ton programme.

Un autre problème qui peut arriver avec les spécifications, c’est qu’elles soient incohérentes ou incomplètes. Dans le premier cas, un assistant de preuve échouera à prouver toutes les propriétés et cela peut permettre de trouver un bug dans les spécifications. Dans le deuxième cas, il existe des techniques pour trouver les trous dans un ensemble de spécifications (pour une entreprise qui vend ce genre de solutions, voir « Argosim »).

Et le compilateur ne pourra dans bien des cas jamais écrire le code à partir des spécifications, justement parce que les spécifications sont déclaratives, et qu’il y a beaucoup de contraintes qui empêchent le compilateur de choisir une solution si tant est qu’il en trouve une automatiquement. Par exemple, si tu spécifies un algorithme qui doit extraire le maximum d’un ensemble de nombres, il suffirait de dire "max(E) appartient à E et est supérieur ou égal à tous ses éléments". Et là tu as l’embarras du choix en fonction des performances et des spécificités du problème.

Salut,

Ça tombe bien, c’était l’objectif .

Je dirai que ça dépend de ce que tu appelles "grande échelle". C est souvent utilisé pour des programmes qui sont pas si énormes¹ que ça dans l’embarqué (ils peuvent comprendre beaucoup de lignes, mais ne sont pas si complexes qu’ils peuvent le paraître au premier abord). Pour des programmes de taille relativement restreintes mais avec des hauts degrés de criticité, il commence à y avoir pas mal de success-story. Maintenant des micronoyaux avec des éléments prouvés, on commence à en avoir le tour du ventre.

Pour information le 30 mai à Paris, il y a le Frama-C & SPARK Day (programme), il va regrouper des gens de l’académique mais aussi de l’industriel (le premier Frama-C Day c’était plus d’une moitié d’industriels). C’est souvent du R&D, mais ils utilisent ça sur du vrai code. Qui est correctement ciblé, ce qui m’amène au second point déjà abordé par @LoupSolitaire.

On le fait là où il y en a besoin. Là où le coût d’un problème est supérieur au coût de vérification. Il ne faut pas rêver, Airbus n’utilisent pas Frama-C parce que c’est joli et que ça leur met une casquette "on est gentil et on bosse avec la recherche", ils le font parce qu’après avoir évalué plein de critères, ça semble leur coûter un poil moins cher comme ça.

Concernant la partie sur les langages de programmations sûrs. Oui, évidemment, ce serait super. Seulement attention parce que s’accorder certaines constructions rend les spécifications et la preuve plus difficile (le second ordre ou l’application partielle par exemple), notamment parce qu’elles créent des propriétés qui assassinent les prouveurs automatiques.

L’autre point est que parfois tu ne peux juste pas avoir accès à ces langages :

• parce que tu n’as de compilateur pour ton micro-contrôleur,
• parce que le runtime du logiciel serait trop lourd pour ton micro-contrôleur,
• parce que ton compilateur n’a pas la certification "truc-muche",
• ....

Il faut bien commencer tes suppositions quelque part. Déjà on passe de "mon code et mes spécifications sont parfaites" à "mes spécifications sont parfaites", on y gagne. D’autre part, comme le mentionne @Aabu, on peut les fouiller pour trouver des oublis.

Mais le point qui m’intéresse c’est plus ce qui concerne la partie "compilation". En fait, réaliser "un programme" à partir de spécifications déclaratives, ça existe, depuis longtemps. Il y a même un langage qui nous permet cela. Et il s’appelle Prolog apparu en 1972, la même année que C. Le langage nous permet d’exprimer les propriétés de notre résultat en logique de premier ordre. Et c’est le moteur de Prolog qui se charge de résoudre le problème. Cependant, comme l’a mentionné @Aabu, avoir du contrôle sur la manière dont est résolu le problème est assez difficile.

Il y a déjà eu des travaux pour faire cela dans Frama-C. Voir le greffon E-ACSL (Executable ACSL) dont je parle dans la conclusion. Cependant, le fragment d’ACSL considéré est actuellement relativement restreint, il y a des travaux plus conséquents en ce moment pour intégrer de nouvelles fonctionnalités et traiter des spécifications plus complexes.

Y’a plein d’aspects qui rentre en compte dans la preuve de programme

Sur la question du langage:

• En général, on va prouver là où y’a une demande. Comme ca a été dit, c’est en général sur des systèmes critiques avec des capacités limités qui vont vivre très longtemps avec des contraintes fortes (on trouve des microprocesseur d’il y a 30 ans / 40 ans dans les avions de tous les jours)

• Il y’a aussi la question de la main d’oeuvre. Ces projets sont en général très complexes et même s’il existait un super langage, encore faudrait-il disposer d’assez de développeurs compétents. En supposant qu’un super langage sorte aujourd’hui, il serait dans un avion commercial dans 20-30 ans (temps d’adoption grand public puis par les industriels, certification, …).

• La base de code existante est gigantesque. N’importe quel industriel n’a pas envie de tout changer alors que ca marche et c’est approuvé. Même avec un nouveau langage safe et des développeurs disponibles, ca couterait des millions/milliards.

=> On est encore coincé avec le C pendant plusieurs (dizaines) années.

Ensuite, dans le domaine de l’analyse statique y’a un compromis entre automaticité/précision de la preuve. Des preuves manuelles de code via Coq & Co vont être lourdes et pénibles mais on est sûr qu’elles sont justes. Si on souhaite automatiser, on va en général perdre en correction et/ou soundness et donc se retrouver avec des faux négatifs (code remonté mais juste) ou des bugs loupés.

Après, on fait de l’analyse de code avec les méthodes dont la recherche dispose. Y’a 3 grandes classes de techniques d’analyse statique:

• Model checking
• Interprétation abstraite (gros succès de ASTREE)
• Système déductif et logique de Hoare (ce sur quoi porte le cours).

Toutes les techniques n’offrent pas le même degré d’automatisation, de précision et ne recherche pas le même genre d’erreur. Les 2 premieres sont en général automatiques, la 3ême est semi automatique (annotation du code à la main) mais preuve automatique si possible.

Enfin, pour prouver des choses formellement sur du code, il faut avant tout être d’accord sur ce que veut dire un bout de code (sa sémantique). En général, la sémantique d’un langage mainstream est non formellement définie. Et définir formellement la sémantique d’un langage mainsteam est très compliqué (il faut formaliser les 200-1500 pages du standard), faire des choix à propos des comportements indéfinis (!),… C’est un travail de titan. De mémoire (ca a peut évolué), Frama-C avait quelques limitations avec les pointeurs.

En fait, réaliser "un programme" à partir de spécifications déclaratives, ça existe, depuis longtemps. Il y a même un langage qui nous permet cela. Et il s’appelle Prolog apparu en 1972, la même année que C. Le langage nous permet d’exprimer les propriétés de notre résultat en logique de premier ordre. Et c’est le moteur de Prolog qui se charge de résoudre le problème.

Je ne suis pas vraiment d’accord avec cette caractérisation de Prolog; à l’usage on se rend vite compte que ce n’est pas un langage déclaratif, dans le sens où le fait de bien comprendre le modèle d’exécution du langage est essentiel pour écrire correctement ses programmes en pratique (c’est moins le cas dans des fragments plus limités comme Datalog).

Áujourd’hui la synthèse de programme à partir de spécifications ne marche que dans certains cas assez restreints et un peu de niche (ce qui suffit à répondre à la question de "pourquoi on ne le fait pas", bah on ne sait pas faire). On a des langages plus haut niveau que C pour exprimer des propriétés (même dans le domaine embarqué/critique SCADE par exemple est assez utilisé il me semble), beaucoup étant "plus déclaratifs", mais il n’y a pas de langage que l’on puisse désigner universellement comme "un langage impératif", et dans le fond je ne suis pas sûr que ça existe, puisque spécifier et définir restent des activités très différentes.

Attention, je n’ai pas dit que le programme résultant serait efficace, j’ai dit qu’il serait. Du reste, le programme reste une spécification en logique du premier ordre. Typiquement, en beaucoup moins extrême, on a les langages à GC : si on veut vraiment être efficace, mieux vaut bien comprendre la mécanique d’allocation et le fonctionnement du GC pour éviter de péter la tête au runtime. Et c’est parfois difficile de voir comment ça marche justement parce que le langage ne le montre pas.

C’est toujours une affaire d’équilibre, plus on délègue de travail au langage, moins on a de prise dessus. Quand on relâche que la gestion des ressources, c’est souvent invisible, quand on relâche jusqu’à la production de l’algorithme, ça devient bien plus violent.

Tiens puisque j’aime bien mettre les événements à propos des FMs, ce mercredi, il y a la journée AFSEC à Paris. On va parler approches formelles pour la sécurité.

Non, je ne suis toujours pas d’accord. Ce n’est pas qu’une question d’efficacité : en pratique en Prolog si tu ne fais pas attention aux modes que tu veux gérer, tes programmes vont boucler à l’infini si tu les utilises d’une façon différente de ce que tu as testé. (Dans un langage avec un bon GC, connaître les détails du GC n’est utile que dans des cas très, très exceptionnels. En prolog c’est important en permanence ou presque, même quand on n’utilise pas les coupures – qui sont pourtant très fréquentes.)

Par ailleurs, Prolog n’a pas toute la puissance de la logique de premier ordre, puisque la structure des clauses de Horn restreint beaucoup les formules que tu peux exprimer. Même les extensions comme les formules héréditaires de Harrop gardent des restrictions fortes (sur l’emboîtement de disjonctions/existentielles dans les implications).