Vérification formelle du programme en pratique

66

En tant qu’ingénieur logiciel, j’écris beaucoup de code pour les produits industriels. Trucs relativement compliqués avec des classes, des threads, des efforts de conception, mais aussi des compromis sur les performances. Je fais beaucoup de tests, et j'en ai marre, alors je me suis intéressé aux outils de preuve formels, tels que Coq, Isabelle ... Pourrais-je en utiliser un pour prouver formellement que mon code est sans bug et qu'il est prêt avec ça? - mais chaque fois que je vérifie l'un de ces outils, je ne suis pas convaincu qu'ils soient utilisables pour le génie logiciel au quotidien. Maintenant, ça ne peut être que moi, et je cherche des pointeurs / opinions / idées à ce sujet :-)

Plus précisément, j’ai l’impression que, pour que l’un de ces outils fonctionne, il faudrait un investissement considérable pour bien définir les objectifs, les méthodes ... du programme considéré. Je me demande alors si le prouveur ne s'essoufflerait pas compte tenu de l'ampleur de tout ce qui lui incomberait. Ou peut-être devrais-je me débarrasser des effets secondaires (ces outils de démonstration semblent bien fonctionner avec les langages déclaratifs), et je me demande si cela aurait pour résultat un "code éprouvé" qui ne pourrait pas être utilisé car il ne serait pas rapide ou assez petit. De plus, je n'ai pas le luxe de changer le langage avec lequel je travaille, il faut que ce soit Java ou C ++: je ne peux pas dire à mon supérieur que je vais coder en OXXXml à partir de maintenant, car c'est le seul langage en ce que je peux prouver l'exactitude du code ...

Est-ce que quelqu'un avec plus d'expérience des outils de preuve formels pourrait commenter? Encore une fois - j'adorerais utiliser un outil de démonstration formel, je les trouve géniaux, mais j'ai l'impression qu'ils se trouvent dans une tour d'ivoire que je ne peux pas atteindre depuis le petit fossé de Java / C ++ ... (PS: I J'AIME aussi Haskell, OCaml ... ne vous méprenez pas: je suis un fan des langages déclaratifs et des preuves formelles, j'essaie simplement de voir comment je pourrais concrètement rendre cela utile au génie logiciel)

Mise à jour: Puisque c'est assez large, essayons les questions plus spécifiques suivantes: 1) existe-t-il des exemples d'utilisation de prouveurs pour prouver l'exactitude des programmes industriels Java / C ++? 2) Coq conviendrait-il à cette tâche? 3) Si Coq convient, dois-je d'abord écrire le programme en Coq, puis générer C ++ / Java à partir de Coq? 4) Cette approche pourrait-elle gérer les optimisations de threading et de performance?

Franc
la source
3
Je comprends et j'apprécie votre problème, mais je ne comprends pas quelle est la question après (en tant que message SE). Discussion? Expérience? Ni est adapté pour SE. Le "Que puis-je faire?" le ton me fait sentir que c'est une question trop large, aussi.
Raphaël
3
Je vois ... je conviens que cette question n'a pas été formulée clairement. Donc, disons: 1) existe-t-il des exemples d'utilisation de prouveurs pour prouver l'exactitude des programmes industriels Java / C ++? 2) Coq conviendrait-il à cette tâche? 3) Si Coq convient, dois-je d'abord écrire le programme en Coq, puis faire en sorte que Coq génère C ++ / Java à partir de cela? 4) Cette approche est-elle compatible avec les optimisations de threading et de performance?
Frank
2
Donc, ça fait quatre questions, alors. 1) est probablement mieux loti en génie logiciel, car il est peu probable que vous rencontriez (beaucoup) de professionnels de l'industrie ici. 2) goûts quelque peu subjectifs, mais nous pouvons avoir des gens ici qui peuvent offrir une perspective objective. 3) est, à ce que je sache, complètement subjectif. 4) Est une bonne question pour ce site. En résumé: veuillez séparer vos questions, allez à Génie logiciel avec le premier et réfléchissez bien pour savoir si vous pouvez vous attendre à une réponse objective (!) Ici (!) Avant de poster 2).
Raphaël
10
Vous décrivez le rêve de la vérification formelle, mais nous sommes très loin d’être là. Autant que je sache, la vérification de programme est une tâche inhabituelle et ne concerne que des programmes très simples. Cela dit, je pense que cette question est très pertinente pour le site et j'apprécierais que quelqu'un de la région admette les limites de son domaine, explique l'état de la technique et les limites (en reliant peut-être certains ).
Yuval Filmus
9
Le problème avec la vérification des programmes C ++ est que C ++ n'est pas un langage bien défini. Je ne pense pas que la vérification à grande échelle soit possible avant que de nombreux composants de systèmes logiciels (systèmes d'exploitation, bibliothèques, langages de programmation) soient réellement repensés pour prendre en charge la vérification. Comme on le sait, vous ne pouvez pas simplement décharger 200 000 lignes de code sur quelqu'un et dire "vérifier!". Vous devez vérifier et écrire du code ensemble, et vous devez adapter vos habitudes de programmation au fait que vous vérifiez également.
Andrej Bauer

Réponses:

35

Je vais essayer de donner une réponse succincte à certaines de vos questions. Veuillez garder à l'esprit que ce n'est pas strictement mon domaine de recherche, donc certaines de mes informations peuvent être obsolètes / incorrectes.

  1. Il existe de nombreux outils spécialement conçus pour prouver formellement les propriétés de Java et de C ++.

    Cependant, il me faut faire une petite digression: que signifie prouver l’exactitude d’un programme? Le vérificateur de types Java prouve une propriété formelle d'un programme Java, à savoir que certaines erreurs, telles que l'ajout d'un floatet d'un int, ne peuvent jamais se produire! J'imagine que vous êtes intéressé par des propriétés beaucoup plus fortes, à savoir que votre programme ne peut jamais entrer dans un état indésirable, ou que la sortie d'une certaine fonction est conforme à une certaine spécification mathématique. En bref, il existe un large gradient de ce que "prouver qu'un programme est correct" peut signifier, allant de simples propriétés de sécurité à une preuve complète que le programme remplit une spécification détaillée.

    Maintenant, je vais supposer que vous êtes intéressé par la démonstration de propriétés fortes de vos programmes. Si les propriétés de sécurité vous intéressent (votre programme ne peut pas atteindre un certain état), alors, en général, il semble que la meilleure approche est la vérification du modèle . Toutefois, si vous souhaitez spécifier pleinement le comportement d'un programme Java, le mieux est d'utiliser un langage de spécification pour ce langage, par exemple JML . Il existe de tels langages pour spécifier le comportement des programmes C, par exemple ACSL , mais je ne connais pas le C ++.

  2. Une fois que vous avez vos spécifications, vous devez prouver que le programme est conforme à ces spécifications.

    Pour cela, vous avez besoin d’un outil qui comprenne formellement votre spécification et la sémantique opérationnelle de votre langage (Java ou C ++) afin d’exprimer le théorème d’adéquation , à savoir que l’exécution du programme respecte la spécification.

    Cet outil devrait également vous permettre de formuler ou de générer la preuve de ce théorème. Maintenant, ces deux tâches (spécifier et prouver) sont assez difficiles, elles sont donc souvent séparées en deux:

    • Un outil qui analyse le code, la spécification et génère le théorème d’adéquation. Comme Frank l'a mentionné, Krakatoa est un exemple d'un tel outil.

    • Un outil qui prouve le ou les théorèmes, automatiquement ou de manière interactive. Coq interagit avec Krakatoa de cette manière, et il existe de puissants outils automatisés tels que Z3 qui peuvent également être utilisés.

    Un point (mineur): il existe des théorèmes qui sont beaucoup trop difficiles à prouver avec des méthodes automatisées, et les prouveurs automatiques de théorèmes ont parfois des bogues de correction qui les rendent moins dignes de confiance. C'est un domaine où Coq brille en comparaison (mais ce n'est pas automatique!).

  3. Si vous voulez générer du code Ocaml, écrivez d'abord en Coq (Gallina), puis extrayez le code. Cependant, Coq est terrible pour générer du C ++ ou Java, si c'est même possible.

  4. Les outils ci-dessus peuvent-ils gérer les problèmes de threading et de performance? Probablement pas, les problèmes de performances et de threading sont mieux gérés par des outils spécialement conçus, car ce sont des problèmes particulièrement difficiles. Je ne suis pas sûr d'avoir des outils à recommander ici, bien que le projet PolyNI de Martin Hofmann semble intéressant.

En conclusion: la vérification formelle des programmes Java et C ++ "réels" est un domaine vaste et bien développé, et Coq convient à certaines parties de cette tâche. Vous pouvez trouver un aperçu de haut niveau ici par exemple.

Cody
la source
Merci pour ce post et les références que vous avez ajoutées. IMHO, l'objectif des ingénieurs en logiciel est de pouvoir libérer rapidement des systèmes qui 1) fourniront toujours des résultats corrects, 2) ne feront jamais défaut. Je pourrais voir un problème de régression ici, où vous voudrez peut-être prouver que la spécification elle-même est "sans bug": un peu comme essayer de définir la "proposition vraie d'un langage" avec un méta-langage, puis besoin d'une autre méta langue pour ça, puis une autre ...
Frank
6
Le problème est que ce que l'utilisateur "veut" n'est généralement pas exprimé dans un langage formel! Il n'y a généralement pas de réponse formelle à la question: "cette spécification formelle est-elle conforme à mon idée informelle?". Il est possible de tester une spécification formelle et de prouver qu'elle possède certaines propriétés mathématiques, mais vous devez en définitive relier les mathématiques au monde réel, qui est un processus non formel.
Cody
Oui, bien sûr. J'ai toujours compris que les méthodes formelles ne pouvaient partir que d'un point bien défini. Si cette spécification est conforme ou non aux besoins conscients / inconscients / non découverts des utilisateurs de la vie réelle est un autre problème, qui ne peut être résolu par des méthodes formelles (mais qui pose certainement un problème pour les ingénieurs).
Frank
Un théorème est par définition une proposition prouvée. Donc, vous ne voulez probablement pas "prouver le théorème".
nbro
@nbro Wikipedia semble être d'accord avec vous. Mathworld, cependant, définit un théorème comme une proposition qui " peut être démontrée comme vraie par des opérations mathématiques acceptées". Dans ce cas, donner des preuves de théorèmes est non seulement possible, mais nécessaire pour justifier de les appeler ainsi! :) (c'est un contre-jugement, bien sûr)
cody
15

Je voudrais mentionner trois applications remarquables de méthodes formelles / d’outils de vérification formels dans l’industrie ou de systèmes réels non triviaux. Notez que j'ai peu d'expérience sur ce sujet et que je ne les apprends qu'en lisant des articles.

  1. L'outil open source Java Pathfinder (JPF, en abrégé) publié par la NASA en 2005 est un système permettant de vérifier les programmes de bytecode Java exécutables (voir Java Pathfinder @ wiki ). Il a été utilisé pour détecter des incohérences dans le logiciel exécutif du K9 Rover de la NASA Ames.

  2. Ce document: Utilisation de la vérification de modèle pour rechercher des erreurs de système de fichiers graves @ OSDI'04 montre comment utiliser la vérification de modèle pour rechercher des erreurs graves dans les systèmes de fichiers. Un système appelé FiSC est appliqué à trois systèmes de fichiers largement utilisés et largement testés: ext3, JFS et ReiserFS, et 32 ​​bogues sérieux sont détectés. Il a remporté le prix du meilleur article.

  3. Ce document: Utilisation des méthodes formelles par Amazon Web Services @ CACM'15 décrit comment AWS applique des méthodes formelles à ses produits tels que S3, DynamoDB, EBS et le gestionnaire de verrous distribués internes. Il se concentre sur l' outil TLA + de Lamport . À propos, Lamport a utilisé de manière intensive sa propre boîte à outils TLA. Il donne souvent une vérification formelle (assez complète) dans TLA des algorithmes / théorèmes proposés par lui-même (ainsi que par les coauteurs) dans les annexes des articles.

Hengxin
la source
4

Une spécification formelle d'un programme est (plus ou moins) un programme écrit dans un autre langage de programmation. En conséquence, la spécification inclura certainement ses propres bogues.

L'avantage de la vérification formelle est que, comme le programme et la spécification sont deux implémentations distinctes, leurs bogues seront différents. Mais pas toujours: une source commune de bugs, les cas négligés, sera souvent identique. Ainsi, la vérification formelle n'est pas une panacée: il peut encore rater un nombre non négligeable de bugs.

Un inconvénient de la vérification formelle est qu’elle peut imposer deux fois le coût d’implémentation, probablement plus (vous avez besoin d’un spécialiste en spécification formelle, et vous devez utiliser les outils plus ou moins expérimentaux qui vont avec; cela ne va pas coûter cher ).

J'imagine que la configuration de cas de test et d'un échafaudage pour les exécuter automatiquement serait une meilleure utilisation de votre temps.

vonbrand
la source
L' avantage de la vérification formelle est que ... Un deuxième inconvénient de la vérification formelle est que ... C'est déroutant.
Hengxin
Je pense que l'inadéquation entre la spécification et la tâche informelle est un problème d'analyse des exigences logicielles et non un problème de programmation.
Kaveh
3

La vérification formelle est désormais possible pour les programmes écrits dans un sous-ensemble de C ++ conçu pour les systèmes intégrés critiques pour la sécurité. Voir http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt pour une brève présentation et http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf pour le texte intégral.

dc42
la source
5
Merci pour les liens. Au moins un bref aperçu de leur contenu serait utile pour se protéger des liens, en particulier parce que vos liens dirigent vers un site Web d'entreprise: ceux-ci ont tendance à se réorganiser périodiquement, détruisant ainsi tous les liens vers le site.
David Richerby
2

Vous posez quelques questions différentes. Je conviens qu'il semble que les méthodes de vérification formelle pour les applications industrielles / commerciales ne soient pas si courantes. il faut toutefois savoir que les compilateurs intègrent un grand nombre de principes de "vérification formelle" pour déterminer la correction du programme! En un sens, si vous utilisez un compilateur moderne, vous utilisez une grande partie de l'état de l'art en matière de vérification formelle.

Vous dites "j'en ai assez des tests" mais la vérification formelle ne remplace pas vraiment les tests. D'une certaine manière, c'est une variante des tests.

Vous parlez de Java. Il existe de nombreuses méthodes de vérification formelle avancées intégrées dans un programme de vérification Java appelé FindBugs qui peuvent en effet être exécutées sur de grandes bases de code. Notez que les résultats seront "faux positifs et faux négatifs" et que les résultats doivent être revus / analysés par un développeur humain. Mais notez que même s’il ne présente pas de défauts fonctionnels réels, il indique généralement des «antipatterns» qui doivent de toute façon être évités dans le code.

Vous ne faites plus mention de votre application particulière autre que "industrielle". La vérification formelle dans la pratique a tendance à dépendre de l'application particulière.

Les techniques de vérification formelle semblent être largement utilisées en EE pour prouver la correction des circuits, par exemple dans la conception de microprocesseurs.

Voici un exemple d'enquête sur les outils de vérification formels dans le domaine de l' efficacité énergétique réalisée par Lars Philipson .

vzn
la source
2
Il est trompeur de dire qu '"un grand nombre de principes de" vérification formelle "sont intégrés aux compilateurs pour déterminer l'exactitude du programme". Vous faites référence à la vérification de type statique effectuée par certains compilateurs, mais les propriétés ainsi vérifiées sont plutôt simples, par exemple en évitant d’ajouter un nombre et une chaîne. C'est utile, mais loin de ce que l'on entend habituellement par "vérification formelle".
Martin Berger
2
ne fait pas spécifiquement référence à la vérification de type statique, bien que ce soit un exemple simple / commun. Les techniques d'optimisation du compilateur imho, qui sont répandues et avancées, sont à peu près similaires aux principes de vérification formels, car elles font appel à des techniques avancées pour déterminer / montrer l'équivalence de variantes de programmes optimisées. il semble donc important d’éviter la question des "objectifs en mouvement" et de ne pas supposer que le fait que le compilateur le réalise ou qu’il soit intégré au compilateur ne constitue pas une vérification formelle.
vzn
2
convenu que ce n'est pas une compréhension commune. les techniques d'optimisation consistent à créer un modèle de comportement de programme, par exemple une boucle ou un sous-programme, à optimiser ce modèle, puis à générer un nouveau code qui est manifestement équivalent. certaines de ces optimisations sont donc assez sophistiquées pour réorganiser le code et utilisent pour moi des principes de vérification formels. il semble y avoir de nombreux autres exemples de méthodes de vérification formelle dans le compilateur ... la question initiale posait de nombreuses questions différentes, comme beaucoup l'ont noté, mais n'essayons pas de répondre à toutes les questions qui y figurent.
vzn
2
en passant, il semble exister des principes de vérification formels également utilisés dans JRE, le moteur d'exécution Java, par exemple l'optimisation dynamique, etc ...
vzn
3
c’est "le rêve de la vérification formelle" évoqué par filmus ci-dessus, à mon avis une abstraction chimérique, et une industrie pragmatique / utilitaire / réaliste le reconnaît largement en tant que tel. Les grandes bases de code sont connues depuis des décennies pour avoir intrinsèquement bugs / défauts par des lignes K de code et cela ne changera jamais , peu importe les progrès de la théorie / technologie, c'est un fait de la nature humaine . et en fait, les théorèmes mathématiques créés par l'homme ont les mêmes propriétés, bien que cela ne soit pas largement apprécié! yxy
vzn
1

Peut-être qu'un vérificateur de modèle pourrait être utile.

http://alloytools.org/documentation.html Alloy est un vérificateur de modèles.

Une belle présentation expliquant le concept de vérification de modèle à l'aide d'Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Dans la même famille d'outils, il y a les «tests basés sur les propriétés», ils essaient tous de trouver un contre-exemple pour le modèle de spécification donné de votre logiciel.

TIC Tac
la source