Post-Doc

Conception de techniques de compilation pour améliorer l'efficacité d'E-ACSL, un vérificateur d'assertions à l'exécution pour programmes C

  • Cybersécurité : hardware et software,
  • Département Ingénierie Logiciels et Systèmes (LIST)
  • Laboratoire pour la Sûreté du Logiciel
  • 01-01-2025
  • Saclay
  • PsD-DRT-24-0117
  • SIGNOLES Julien (Julien.Signoles@cea.fr)

Notre équipe développe Frama-C (http://frama-c.com), une plateforme d'analyse de programmes C qui fournit plusieurs analyseurs sous forme de greffons. Frama-C lui-même est développé en OCaml. Cette plateforme permet à l'utilisateur d'annoter des programmes C à l'aide de spécifications formelles écrites dans le langage ACSL. Elle peut ensuite garantir qu'un programme C satisfait sa spécification à l'aide de techniques formelles comme l'interprétation abstraite, la preuve de programmes ou la vérification à l'exécution. E-ACSL est ainsi le greffon de Frama-C en charge de la vérification à l'exécution. Il convertit un programme C annoté avec des annotations formelles en un nouveau programme C qui vérifie la validité des annotations pendant l'exécution du programme: par défaut, l'exécution est arrêtée dès lors qu'une annotation est violée. S'il n'y a pas d'erreur, le programme s'exécute normalement. Une caractéristique importante d'E-ACSL est l'expressivité de son langage de spécification qui permet de décrire de nombreuses propriétés de sûreté et de sécurité. Une autre caractéristique importante est l'efficacité du code généré qui repose notamment sur une bibliothèque et des analyses statiques dédiées. Cependant, E-ACSL peut encore être amélioré sur de nombreux points pour étendre l'expressivité, tout en réduisant les temps d'exécution et la consommation mémoire. C'est l'objectif du post-doctorat.

fr_FRFR

Contact us

We will reply as soon as possible...