Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C

Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), are becoming more and more widespread. Some of these devices are used in security-critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. It is therefore important to provide security guarantees for the software executed by simple devices, which often do not even provide memory protection units. This kind of guarantees can be brought using formal verification. In this tutorial, we focus on the use of Frama-C, a platform for the analysis of C programs, to verify IoT software. We illustrate it on several examples taken from Contiki, a lightweight operating system for Internet of Things.