Vous êtes ici

Vérification formelle légère pour les programmes fonctionnels

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
https://www.irisa.fr/celtique/
Directeur de thèse
Thomas Genet
Co-directeur(s), co-encadrant(s)
Jensen
Contact(s)
Sujet de thèse
Descriptif

Contexte et état de l’art:

L’utilisation des langages fonctionnels se démocratise. D’une part, les fonctions d’ordre supérieur font maintenant partie des environnements de développement comme .NET (F#) ou Java (Java 8, Scala). D’autre part, les langages fonctionnels sont utilisés comme des langages de spécification exécutable pour le développement de logiciels critiques. Comme exemple, on peut citer l’utilisation de Haskell dans le développement de l’OS sécurisé seL4 [KAE+14], ou le formalisme SMART développé par la PME Prove & Run pour certifier des micro-noyaux et des hyperviseurs [BJS16].

Pour démontrer une propriété sur un programme, il est nécessaire de définir cette propriété en logique (ou dans un système de type enrichi de formules logiques) puis de démontrer cette propriété. Les outils de vérification formelle de ce type de langages sont essentiellement la vérification déductive (comme Coq [Coq] qui a permis le développement de CompCert [Ler09, LB08]), et les systèmes de types enrichis (les outils F* [Fst, SHK+16], Leon [MKK17, Leo], les Liquid Types [RKJ08], et les types intersection [CNX+14]).

La tâche de démonstration, même si son automatisation progresse, reste très ardue. D’une part, il est nécessaire de maîtriser l’outil de vérification pour savoir comment définir la propriété et avoir une chance d’aboutir dans sa preuve. D’autre part, il faut faire preuve d’inventivité et de bonnes connaissances en logique pour déduire les lemmes intermédiaires (parfois ésotériques) nécessaires pour mener la preuve à son terme. Ces deux points difficiles ont la même origine: le raisonnement logique sur le programme est généralement décorrelée de l’exécution du programme lui-même. A tel point qu’il est parfois nécessaire de redéfinir un programme pour que son exécution soit plus proche des étapes d’un raisonnement logique et permette, ainsi, d’achever la preuve.

Un autre point faible de ces techniques de vérification est la détection de contre-exemple: il est difficile de distinguer entre une propriété fausse (qui admet un contre-exemple) et un chemin de preuve malheureux qui ne permet pas de conclure. On voit ainsi émerger des outils de vérification complémentaires, inspirés du test, générant des contre-exemples pour réfuter les propriétés énoncées sur un programme. Cette technique s’est montrée très efficace aussi bien pour des programmes (e.g. QuickCheck [CH00] pour Haskell) que pour des spécifications formelles (e.g. Nitpick [BN10] pour Isabelle/HOL et Nunchaku [CB16] pour Isabelle/HOL et Coq). Dans tous les cas, cette tâche est déléguée à un outil externe à l’outil de vérification: Nitpick et Nunchaku. Ces générateurs de contre-exemples réalisent une interprétation logique particulière du programme, parfois décorrelée de l’exécution du programme réel, et peuvent donc générer des faux contre-exemples.

Outre les techniques de vérification et outils déjà mentionnés au dessus, une autre veine de travaux s’est spécialisée dans l’application du model-checking à la vérification de programmes fonctionnels d’ordre supérieur. Ces travaux ont mené à de nombreuses publications des groupes de Luke Ong [Ong15, OR11, KO11] et de Naoki Kobayashi [TTK16, KL15, Kob13, KI13, KTU10]. Par rapport aux approches précédentes, la vérification par model-checking se rapproche beaucoup plus de l’exécution du programme réel, elle peut générer des contre-exemples et ne demande pas au programmeur d’inventer des lemmes intermédiaires. Les travaux de Kobayashi et Ong sont généralement théoriques. Leur objectif central est de repousser les limites de la décidabilité du problème du model-checking des programmes fonctionnels. Cependant, ils ont montré à plusieurs reprise que leurs algorithmes étaient implantables et utilisables sur des cas d’études non triviaux [OR11, KL15]. Antérieurement à ces travaux, Neil Jones avait exploré l’exécution symbolique (ou abstraite) des programmes fonctionnels sur des ensembles infinis de valeurs [JA07, Jon87]. Le principe sous-jacent est d’approcher l’image d’une fonction par un langage régulier de termes. Les résultats obtenus étaient intéressants mais imprécis à cause de la rusticité des techniques d’approximation utilisées à l’époque. Récemment, dans l’équipe Celtique, nous avons montré comment utiliser la technique de complétion d’automates d’arbres [GR10] pour approcher de façon régulière et précise l’image d’un système de réécriture [GS15, Gen16]. La précision de l’approximation est définie par un ensemble d’équations qui explicitent les termes du calcul qui peuvent être confondus. Ceci permet d’obtenir des approximations beaucoup plus précises que celles de Neil Jones.

Objectif de la thèse:

Partant du constat que les outils de vérification formelle nécessitent un solide bagage en logique et une expertise dans l’outil de vérification, l’objectif de cette thèse est de concevoir une nouvelle méthode de preuve/vérification formelle, proche de l’intuition du programmeur. En particulier, elle sera corrélée avec l’exécution du programme et conciliera preuve automatique et recherche de contre-exemples. Les programmeurs ont adopté, depuis longtemps, les techniques de validation à base de test: ils exécutent le programme réel et vérifient le résultat obtenu par rapport à un oracle, i.e. un résultat attendu. Cette méthode offre l’avantage de de détecter des contre-exemples par rapport à une propriété définie par l’oracle. Cependant, comme la quantité de tests réalisée est finie cette technique ne permet pas de garantir que la propriété définie par l’oracle est vraie pour toute valeur d’entrée.

Dans cette thèse nous nous proposons de combiner le meilleurs de ces deux mondes: une technique de preuve formelle démontrant automatiquement une propriété en testant le programme de façon symbolique sur un nombre non borné de valeurs d’entrée. Si la propriété n’est pas vérifiée, un contre-exemple est généré à partir de l’un des tests échoués. Pour concevoir cette technique, nous souhaitons utiliser les progrès récents sur les abstractions d’images de systèmes de réécriture [GS15, Gen16] en les appliquant à la vérification de fonction par exécution symbolique proposée par Jones [JA07]. Des premières expériences [GS13] ont montré que cette combinaison permet de couvrir certains exemples traités par Ong et Kobayashi. Pour aller au delà nous avons identifié deux défis de recherche :

Défi 1: Génération automatique d’abstractions pour l’ordre supérieur

La première voie est d’étendre le type propriétés démontrables, automatiquement, par ces techniques d’exécution symbolique. Ceci passe par un raffinement des résultats de [Gen16] pour inférer automatiquement un ensemble d’équation adapté à un programme fonctionnel particulier, éventuellement d’ordre supérieur. Lors d’expériences préliminaires, pour un programme du premier ordre donné, nous avons généré de façon exhaustive tous les ensembles d’équations possibles. Ceci a permis, par exemple, de démontrer automatiquement qu’une fonction de tri rendait une liste effectivement triée, sans avoir besoin de lemmes intermédiaires. A titre de comparaison, démontrer cette propriété en utilisant des méthodes déductives ou des systèmes de type enrichi, nécessite de déduire, de définir, et de prouver plusieurs lemmes intermédiaires non triviaux. De la même façon, cette preuve est, à notre connaissance, hors d’atteinte des outils de model-checking de Ong et Kobayashi. Cependant, pour un programme donné, la génération exhaustive des ensemble d’équations n’est, en général, pas réaliste. L’objectif de cette partie est d’utiliser la structure du programme lui-même pour restreindre les ensembles d’équations à considérer.

Principaux verrous :

  • Synthèse des équations pour les fonctions d’ordre supérieur;
  • Passage à l’échelle de la synthèse d’équations pour des programmes de taille et de complexité conséquente.

Défi 2: Preuves guidées par le polymorphisme

La seconde voie est d’exploiter les résultats obtenus au terme d’une exécution symbolique pour démontrer une propriété logique sur un programme. La force des approches déductive ou des système de types enrichis est d’autoriser la modularité dans la vérification. Une formule logique (ou un type enrichi) peut résumer une propriété sur une sous-fonction. Cette propriété est utilisée, par la suite, dans la vérification de la fonction principale. A l’inverse, les approches de Ong, Kobayashi et Jones ne facilitent pas la modularité car il est généralement difficile de reconstruire une formule logique à partir des résultats obtenus. Nous proposons ici de produire automatiquement des théorèmes logiques à partir des résultats d’exécutions symboliques. De la même façon qu’il est possible d’inférer des invariants polymorphes à partir du type d’une fonction [Wad89], nous proposons d’inférer des invariants quasi-polymorphes à partir de l’approximation de son image.

Principaux verrous :

  • Production d’invariants quasi-polymorphes à partir de résultats d’exécution symbolique;
  • Application à la vérification de programmes écrits dans un langage de programmation réel, par exemple un sous-ensemble fonctionnel de Scala. Définition des interactions avec l’utilisateur;

Critères de succès pour la thèse:

  • Validation de la puissance de la technique de preuve. Un bon cas d’étude est la vérification de la fonction d’insertion d’un élément dans un arbre “rouge-noir”. Ceci reste un problème de vérification difficile même pour un utilisateur éclairé d’un outil de preuve assistée ou de système de types enrichis.
  • Publications dans des conférences de rang A+ comme ICFP, POPL, LICS et dans la conférence de référence en réécriture: FSCD (ex. RTA);
  • Implantation de l’outil de vérification pour un sous-ensemble fonctionnel du langage Scala, et utilisable par des étudiants en Master pour débugger et vérifier leurs programmes. Étude de l’impact sur les utilisateurs de ce langage.
Bibliographie
[BJS16]
P. Bolignano, T. Jensen, and V. Siles. Modeling and Abstraction of Memory Management in a Hypervisor. In Proc. of FASE’16, volume 9633 of LNCS, pages 214 – 230. Springer, 2016.
[BN10]
J.-C. Blanchette and T. Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In Proc. of ITP’10, volume 6172 of LNCS, pages 131–146. Springer, 2010.
[CB16]
Simon Cruanes and Jasmin Christian Blanchette. Extending nunchaku to dependent type theory. In Proc. of HaTT’16, volume 210 of EPTCS, pages 3–12, 2016.
[CH00]
Koen Claessen and John Hughes. Quickcheck: A lightweight tool for random testing of haskell programs. In Proc. of ICFP’00, pages 268–279. ACM, 2000.
[CNX+14]
G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet, and L. Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In POPL’14. ACM, 2014.
[Coq]
Coq proof assistant. https://coq.inria.fr/.
[Fst]
F* system. https://fstar-lang.org.
[Gen16]
T. Genet. Termination Criteria for Tree Automata Completion. Journal of Logical and Algebraic Methods in Programming, 85, Issue 1, Part 1:3–33, 2016.
[GR10]
T. Genet and R. Rusu. Equational tree automata completion. Journal of Symbolic Computation, 45:574–597, 2010.
[GS13]
T. Genet and Y. Salmon. Tree Automata Completion for Static Analysis of Functional Programs. Technical report, INRIA, 2013. http://hal.archives-ouvertes.fr/hal-00780124/PDF/main.pdf.
[GS15]
T. Genet and Y. Salmon. Reachability Analysis of Innermost Rewriting. In RTA’15, volume 36 of LIPIcs, Warshaw, 2015. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[JA07]
N. D. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theoretical Computer Science, 375(1-3):120–136, 2007.
[Jon87]
N. D. Jones. Flow analysis of lazy higher-order functional programs. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 103–122. Ellis Horwood, Chichester, England, 1987.
[KAE+14]
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive Formal Verification of an OS Microkernel. ACM Trans. Comput. Syst., 32(1):2:1–2:70, 2014.
[KI13]
N. Kobayashi and A. Igarashi. Model-Checking Higher-Order Programs with Recursive Types. In ESOP’13, volume 7792 of LNCS, pages 431–450. Springer, 2013.
[KL15]
Naoki Kobayashi and Xin Li. Automata-Based Abstraction Refinement for µHORS Model Checking. In Proc. of LICS’15, pages 713–724. IEEE Computer Society, 2015.
[KO11]
J. Kochems and L. Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In RTA’11, volume 10 of LIPIcs. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2011.
[Kob13]
N. Kobayashi. Model Checking Higher-Order Programs. Journal of the ACM, 60.3(20), 2013.
[KTU10]
N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In POPL’10, pages 495–508. ACM, 2010.
[LB08]
Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1–31, 2008.
[Leo]
The leon system. https://leon.epfl.ch/.
[Ler09]
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.
[MKK17]
Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In Proc. of POPL’17, pages 330–343. ACM, 2017.
[Ong15]
L. Ong. Higher-Order Model Checking: An Overview. In Proc. of LICS’15, pages 1–15. IEEE Computer Society, 2015.
[OR11]
L. Ong and S. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL’11. ACM, 2011.
[RKJ08]
P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid Types. In Proc. of PLDI’08, pages 159–169. ACM, 2008.
[SHK+16]
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. Dependent types and multi-monadic effects in F*. In Proc. of POPL’16, pages 256–270. ACM, 2016.
[TTK16]
Taku Terao, Takeshi Tsukada, and Naoki Kobayashi. Higher-Order Model Checking in Direct Style. In Proc. of APLAS’16, volume 10017 of LNCS, pages 295–313, 2016.
[Wad89]
Philip Wadler. Theorems for free! In Proc. of FPCA’89, pages 347–359. ACM, 1989.
Début des travaux: 
septembre 2017
Mots clés: 
Génie logiciel, Vérification formelle automatique, Exécution symbolique, Génération de contre-exemples.
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes