Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C

Résumé : Les appareils et services connectés, aussi appelés internet des objets (Internet of Things : IoT) sont de plus en plus populaires dans des domaines où la sécurité est critique. Ces questions de sécurité sont une cible de choix pour l'usage de méthodes formelles. Ce travail se concentre sur Contiki, un système d'exploitation open-source populaire pour les objets connectés, qui propose notamment une pile IPv6 pour environnements contraints. Il est implémenté en C avec une attention particulière pour l'optimisation de la consommation mémoire et énergétique, et est disponible pour de nombreuses plateformes physiques. Au début du développement de Contiki en 2002, la sécurité n'était pas un objectif central. La sécurité des communications a été ajoutée plus tard, mais la vérification formelle du code n'a commencé que très récemment. Nous présentons la vérification formelle du module de listes chaînées de Contiki. Ce module est critique pour le système d'exploitation, il est utilisé par 32 modules de Contiki et appelé plus de 250 fois dans la partie coeur du système. Son API est riche, il est possible d'ajouter ou enlever des éléments à n'importe quelle position dans la liste. Elle garantit l'unicité des éléments au sein des listes : avant toute insertion, le module s'assure de supprimer l'élément de la liste avant de l'ajouter à la position voulue. Finalement, Contiki ne permet pas l'allocation dynamique, contrairement aux implémentations classiques des listes, le module de Contiki ne fait donc pas de telle opération. La vérification formelle du module est effectuée grâce au langage de spécification ACSL et au greffon WP de la plate-forme FRAMA-C. Notre approche se base sur des tableaux fantômes (ghost) utilisés comme représentation des listes chaînées.
Complete list of metadatas

https://hal.inria.fr/hal-01811932
Contributor : Allan Blanchard <>
Submitted on : Monday, June 11, 2018 - 9:17:42 AM
Last modification on : Friday, October 18, 2019 - 1:31:28 AM
Long-term archiving on : Wednesday, September 12, 2018 - 1:12:45 PM

File

nfm_summary_for_afadl.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01811932, version 1

Citation

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C. 17èmes Journées AFADL : Approches Formelles Dans L'assistance Au Développement De Logiciels, Jun 2018, Toulouse, France. ⟨hal-01811932⟩

Share

Metrics

Record views

165

Files downloads

46