> Offres de formation > Offres de thèses

Vérification hors-ligne d'assertions à l'exécution

Défi technologique : Data intelligence dont Intelligence Artificielle (en savoir +)

Département : Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire : Laboratoire pour la Sûreté du Logiciel

Date de début :

Localisation : Saclay

Code CEA : SL-DRT-22-0132

Contact : Julien.Signoles@cea.fr

Notre équipe développe Frama-C (http://frama-c.com), une plateforme d'analyse de code C qui fournit plusieurs analyseurs de code. Frama-C est développé en OCaml. Il permet d'annoter des programmes C avec des spécifications formelles écrites dans le langage ACSL. Frama-C peut ainsi garantir qu'un programme C satisfait ses spécifications en se fondant sur des techniques formelles. E-ACSL est l'analyseur de Frama-C dédié à la vérification d'assertions à l'exécution. Il convertit un programme C étendu avec des annotations ACSL en un autre programme C vérifiant la validité des annotations pendant son exécution: par défaut, le programme s'arrête dès qu'une annotation est violée ou, sinon, il se comporte comme le programme original. Pour ce faire, E-ACSL repose sur une instrumentation invasive du code source original afin d'insérer du code qui surveille la validité des annotations ACSL. Cette technique, appellée vérification à l'exécution en-ligne, peut néanmoins s'avérer trop couteuse en temps et en consommation mémoire dans certains contextes d'utilisation. Elle peut aussi soulever des problèmes de sécurité. Le but de la thèse consiste à définir et à implémenter une version hors-ligne d'E-ACSL, compatible avec la version en-ligne existante. La vérification à l'exécution hors-ligne consiste à placer le moniteur dans une entité externe (par exemple, un autre processus sur la même machine ou sur un serveur distant) pour limiter l'instrumentation du code d'origine aux communications avec le moniteur à distance. Cette technique est bien connue et souvent appliquée pour la vérification dynamique de propriétés temporelles, mais elle n'a jamais été appliquée à la vérification d'assertions, qui soulève des problèmes spécifiques liés aux types des données qui doivent être manipulés.

Voir toutes nos offres Télécharger l'offre (.zip)

Email Bookmark and Share