Abstract
Formal verification is still rarely applied to the IoT (Internet of Things) software, whereas IoT applications tend to become increasingly popular and critical. This short paper promotes the usage of formal verification to ensure safety and security of software in this domain. We present a successful case study on deductive verification of a memory allocation module of Contiki, a popular open-source operating system for IoT. We present the target module, describe how the code has been specified and proven using Frama-C, a software analysis platform for C code, and discuss lessons learned.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Dunkels, A., Gronvall, B., Voigt, T.: Contiki - a lightweight and flexible operating system for tiny networked sensors. In: LCN (2014)
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)
Montenegro, G., Kushalnagar, N., Hui, J., Culler, D.: Transmission of IPv6 packets over IEEE 802.15.4 networks. RFC 4944, September 2007. http://www.rfc-editor.org/rfc/rfc4944.txt
Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 15–30. Springer, Cham (2015). doi:10.1007/978-3-319-19458-5_2
Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. http://frama-c.com/acsl.html
Acknowledgment
Part of the research work leading to these results has received funding for DEWI project (www.dewi-project.eu) from the ARTEMIS Joint Undertaking under grant agreement No. 621353. The second author has also been partially supported by a grant from CPER Nord-Pas-de-Calais/FEDER DATA and the distributed environment Ecare@Home funded by the Swedish Knowledge Foundation 2015–2019. Special thanks to Allan Blanchard, François Bobot and Loïc Correnson for advice, and to the anonymous referees for their helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Mangano, F., Duquennoy, S., Kosmatov, N. (2017). Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. In: Cuppens, F., Cuppens, N., Lanet, JL., Legay, A. (eds) Risks and Security of Internet and Systems. CRiSIS 2016. Lecture Notes in Computer Science(), vol 10158. Springer, Cham. https://doi.org/10.1007/978-3-319-54876-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-54876-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54875-3
Online ISBN: 978-3-319-54876-0
eBook Packages: Computer ScienceComputer Science (R0)