Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C

Alexandre Peyrard 1 Nikolai Kosmatov 2 Simon Duquennoy 3 Shahid Raza 3
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : The number of Internet of Things (IoT) applications is rapidly increasing and allows embedded devices today to be massively connected to the Internet. This raises software security questions. This paper demonstrates the usage of formal verification to increase the security of Con-tiki, a popular open-source operating system for the IoT. We present a case study on deductive verification of encryption-decryption modules of Contiki (namely, AES–CCM*) using Frama-C, a software analysis platform for C code.
Type de document :
Communication dans un congrès
RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT, Feb 2018, Madrid, Spain
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01670119
Contributeur : Simon Duquennoy <>
Soumis le : jeudi 21 décembre 2017 - 10:10:57
Dernière modification le : jeudi 12 avril 2018 - 16:25:51

Fichier

RED-IoT 2018 Paper#3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01670119, version 1

Citation

Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Shahid Raza. Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C. RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT, Feb 2018, Madrid, Spain. 〈hal-01670119〉

Partager

Métriques

Consultations de la notice

161

Téléchargements de fichiers

147