Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1) , (2) , (3) , (3)
1
2
3
Nikolai Kosmatov
  • Function : Author
  • PersonId : 940734
Simon Duquennoy
  • Function : Author
  • PersonId : 1015564
Shahid Raza
  • Function : Author
  • PersonId : 1025309

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.
Fichier principal
Vignette du fichier
RED-IoT 2018 Paper#3.pdf (120.03 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01670119 , version 1 (21-12-2017)

Identifiers

  • HAL Id : hal-01670119 , version 1

Cite

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⟩
402 View
440 Download

Share

Gmail Facebook Twitter LinkedIn More