research-article

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

Authors:

Alexandre Peyrard,

Nikolai Kosmatov,,

Simon Duquennoy,

Shahid RazaAuthors Info & Claims

EWSN ’18: Proceedings of the 2018 International Conference on Embedded Wireless Systems and Networks

Pages 264 - 269

Published: 12 February 2018 Publication History

Abstract

The number of IoT (Internet of Things) 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 Contiki OS, a popular open-source operating system for 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.

References

[1]

E. Alkassar, E. Cohen, M. Kovalev, and W. J. Paul. Verification of TLB virtualization implemented in C. In Proc. of the 4th International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2012), volume 7152 of LNCS, pages 209–224. Springer, 2012.

Digital Library

[2]

E. Alkassar, W. Paul, A. Starostin, and A. Tsyban. Pervasive verification of an OS microkernel. In Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2010), volume 6217 of LNCS, pages 71–85. Springer, 2010.

Digital Library

[3]

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proc. of the 23rd International Conference on Computer Aided Verification (CAV 2011), volume 6806 of LNCS, pages 171–177, 2011.

Digital Library

[4]

G. Barthe, G. Betarte, J. D. Campo, J. M. Chimento, and C. Luna. Formally verified implementation of an idealized model of virtualization. In Proc. of the 19th International Conference on Types for Proofs and Programs (TYPES 2013), pages 45–63, 2013.

[5]

P. Baudin, P. Cuoq, J.-C. Fillitre, C. March, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language. http://framac.com/acsl.html.

[6]

E. Biham and A. Shamir. Differential Cryptanalysis of the Data Encryption Standard. Springer, 1993.

Digital Library

[7]

A. Blanchard, N. Kosmatov, M. Lemerre, and F. Loulergue. A case study on formal verification of the anaxagoros hypervisor paging system with frama-c. In Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015), volume 9128 of LNCS, pages 15–30. Springer, June 2015.

[8]

S. Conchon et al. The Alt-Ergo Automated Theorem Prover. http://altergo.lri.fr.

[9]

J. Daemen and V. Rijmen. The Design of Rijndael: AES - The Advanced Encryption Standard. Information Security and Cryptography. Springer, 2002.

Digital Library

[10]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), pages 337–340. Springer, 2008.

Digital Library

[11]

A. Dunkels, B. Gronvall, and T. Voigt. Contiki - a lightweight and flexible operating system for tiny networked sensors. In Proc. of the IEEE Conference on Local Computer Networks (LCN 2014). IEEE, 2004.

Digital Library

[12]

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C: A software analysis perspective. Formal Asp. Comput., 27(3):573–609, 2015.

Digital Library

[13]

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an operatingsystem kernel. Communications of the ACM, 53(6):107–115, 2010.

Digital Library

[14]

F. Mangano, S. Duquennoy, and N. Kosmatov. A memory allocation module of Contiki formally verified with Frama-C. A case study. In Proc. of the 11th International Conference on Risks and Security of Internet and Systems (CRiSIS 2016), volume 10158 of LNCS, pages 114–120. Springer, 2016.

[15]

S. Raza, S. Duquennoy, J. Höglund, U. Roedig, and T. Voigt. Secure Communication for the Internet of Things - A Comparison of Link-Layer Security and IPsec for 6LoWPAN. Security and Communication Networks, Wiley, 7(12):2654–2668, Dec. 2014.

[16]

S. Raza, T. Helgason, P. Papadimitratos, and T. Voigt. Securesense: End-to-end secure communication architecture for the cloud- connected internet of things. Future Generation Computer Systems (Elsevier), 77:40–51, December 2017.

Digital Library

[17]

S. Raza, L. Seitz, D. Sitenkov, and G. Selander. S3K: Scalable Security with Symmetric Keys - DTLS Key Establishment for the Internet of Things. IEEE Transactions on Automation Science and Engineering, 13(3):1270–1280, July 2016.

[18]

V. van der Veen, N. dutt-Sharma, L. Cavallaro, and H. Bos. Memory errors: The past, the present, and the future. In Proc. of the International Symposium on Research in Attacks, Intrusions, and Defenses, volume 7462 of LNCS, pages 86–106. Springer, 2012.

Digital Library

Cited By

Mousavi HEbnenasir AMahmoudzadeh E(2023)Formal Specification, Verification and Repair of Contiki’s SchedulerACM Transactions on Cyber-Physical Systems10.1145/36059487:4(1-28)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1145/3605948
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495

Towards Formal Verification of Contiki: Analysis of the AES-CCM* Modules with Frama-C
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Analysis of crypto module in RIOT OS using Frama-C
Abstract
With the growing advances in Internet of Things (IoT) technology, it has become an indispensable part of many areas like home automation, industries, medical equipment, etc. Thus, the security of the IoT hardware and software is of utmost ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Towards Formal Verification of Node RED-Based IoT Applications
Verification and Evaluation of Computer and Communication Systems
Abstract
The world has been witnessing a proliferation of Internet of Things (IoT) applications in the last decade thanks to the growing awareness of the opportunities they can bring in various domains. However, the widespread adoption of IoT technologies ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

EWSN ’18: Proceedings of the 2018 International Conference on Embedded Wireless Systems and Networks

February 2018

295 pages

ISBN:9780994988621

General Chairs:
Domenico Giustiniano
IMDEA Networks Institute, Spain
,
Dimitrios Koutsonikolas
University at Buffalo, USA
,
Program Chairs:
Albert Banchs
UC3M
,
Enzo Mingozzi
University of Pisa, Italy
,
Kaushik Roy Chowdhury
Northeastern University, USA

Sponsors

EWSN: International Conference on Embedded Wireless Systems and Networks
SUNY Buffalo: State University of NY at Buffalo
IMDEA

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Junction Publishing

United States

Publication History

Published: 12 February 2018

Check for updates

Author Tags

Qualifiers

Research-article

Acceptance Rates

Overall Acceptance Rate 81 of 195 submissions, 42%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mousavi HEbnenasir AMahmoudzadeh E(2023)Formal Specification, Verification and Repair of Contiki’s SchedulerACM Transactions on Cyber-Physical Systems10.1145/36059487:4(1-28)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1145/3605948
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495

View Options

View options

Media

Figures

Other

Tables

View Table of Contents