Virtualisation légère d'application arbitraire pour vérification formelle

Introduction et problématique

Le model checking est une méthode formelle de vérification des systèmes informatiques basée sur l'exploration exhaustive de toutes les évolutions possibles d'un modèle du système à vérifier. Cette méthode est plus facile à utiliser qu'un assistant de preuve qui demande à l'utilisateur d'inventer des objectifs intermédiaires quand l'objectif initial est hors de portée, mais demande encore à l'utilisateur de modéliser le système à vérifier.

La vérification formelle de logiciels (software model checking -- SMC) vise à utiliser les méthodes de model checking directement sur un logiciel à vérifier, sans modélisation préalable. Cela revient à exécuter toutes les exécutions possibles du système à partir d'une situation donnée et pour un input donné. C'est intéressant pour vérifier des applications concurrentes ou distribuées qui doivent fonctionner quel que soit l'ordre effectif des événements concurrents. Le model-checker explore les différentes histoires parallèles que l'application peut suivre en fonction de l'ordre d'exécution des threads et de l'ordre d'arrivée des paquets.

La mise en oeuvre pratique de cette approche pose deux types de problèmes bien différents. D'une part, l'explosion combinatoire du nombre des histoires possibles impose la mise en oeuvre de techniques algorithmiques avancées issues (comme [ODPOR] et [UDPOR]) pour détecter les symétries et réduire le nombre d'histoires à explorer. D'autres part, il faut exécuter l'application vérifiée dans un environnement d'analyse permettant d'une part d'intercepter les interactions de l'application avec son système et d'autre part en contrôlant l'ordre des événements et l'ordre d'exécution des threads. Le premier problème est classique en méthodes formelles, tandis que pour le second, la virtualisation est un problème très classique en OS tandis que l'extension visant à contrôler l'application virtualisée est bien étudié pour les sandboxes d'analyse de malware.

Contexte technique

[Mc SimGrid] est un outil SMC développé dans les équipes Magellan et Devine de l'IRISA. Il est basé sur le framework SimGrid qui permet d'étudier des applications concurrentes et distribuées, à l'origine pour profiler les performances de ces applications. [SimGrid] contient une implémentation du standard MPI permettant de simuler n'importe quelle application MPI pour en prédire les performances avec SimGrid, ainsi que des interfaces dédiées adaptées à la modélisation d'applications distribuées.

Mc SimGrid rajoute le nécessaire pour explorer exhaustivement des applications exprimées dans SimGrid avec les algorithmes ODPOR et UDPOR. Enfin, un troisième composant nommé sthread permet de virtualiser des applications non modifiées pthread pour les exécuter dans SimGrid. En combinant sthread et Mc SimGrid, on obtient un SMC capable de trouver tous les deadlocks potentiels d'une application pthread.

De façon orthogonale, [TANSIV] est un projet développé en collaboration par les équipes Magellan et Sushi de l'IRISA. Il vise à interconnecter des machines virtuelles KVM ou Xen avec un réseau simulé avec SimGrid. La difficulté majeure est de faire correspondre le temps discret du simulateur avec le temps continu des machines virtuelles et masquer les pauses d'exécution liées à l'analyse, de façon non-intrusive voire indétectable pour les applications virtualisées.

En 2023, Hugo Depuydt a proposé pendant son stage L3 une implémentation de TANSIV utilisant des containers Linux (cgroups) afin de permettre une virtualisation plus légère que KVM ou Xen, mais capturant le réseau et le temps. Ce travail est prometteur, mais la pile TCP étant gérée par le noyau dans ce cas, la virtualisation du réseau est défectueuse (on ne peut pas contrôler l'horloge que le noyau utilise pour dater les paquets TCP).

Objectif du stage

Dans un premier temps, il s'agira de compléter la virtualisation légère proposée par Hugo, en utilisant LWIP pour interconnecter les cgroups au lieu de laisser la pile TCP du noyau transmettre les paquets.

Si le temps le permet, on mettra cette virtualisation en oeuvre dans Mc SimGrid dans le second temps du stage. La difficulté est de contrôler suffisament finement l'application virtualisée pour permettre à Mc SimGrid d'explorer exhaustivement les histoires alternatives de l'application. En particulier, si le temps mesuré par l'application devient incohérent, il peu probable que l'application s'exécute suffisament longtemps pour nous permettre de l'étudier convenablement.

L'objectif à terme de ces travaux est de faire en sorte que Mc SimGrid rende les mêmes services que , mais en documentant scientifiquement restant un object scientifique

Bibliographie

AntiThesis est un outil commercial dont le fonctionnement interne est tenu secret. Certaines pages semblent indiquer qu'il s'agit d'une sorte de software model-checker virtualisant les applications au niveau de l'hyperviseur. Ce projet est à la fois inspirant car il montre que l'approche est possible, et frustrant car on ne sait pas comment ça marche. Mc SimGrid est un object scientifique, c'est à dire un projet logiciel servant de champ d'expérimentation pour nous permettre d'étudier scientifiquement la bonne façon de concevoir et implémenter un SMC.

[McSimGrid17] Verifying MPI Applications with Mc SimGrid, T. A. Pham, T. Jéron, M. Quinson. Workshop on Software Correctness for HPC Applications (Correctness’17) https://hal.inria.fr/hal-01632421

[ODPOR] Optimal dynamic partial order reduction, Abdulla, Aronis, Jonsson, Sagonas - ACM Symposium on Principles of Programming Languages (POPL’14). https://user.it.uu.se/~bengt/Papers/Full/popl14.pdf

[UDPOR] Unfolding-based Partial Order Reduction. Cesar Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening - 26th International Conference on Concurrency Theory (CONCUR'15). https://arxiv.org/abs/1507.00980

[TANSIV] Simulating the Network Environment of Sandboxes to Hide Virtual Machine Introspection Pauses. Léo Cosseron, Louis Rilling, Matthieu Simonin, Martin Quinson. 17th European Workshop on Systems Security (EuroSec'24). https://inria.hal.science/hal-04537165