Towards Secure Things, or How to Verify IoT Software with Frama-C

The technical subject and its importance
Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), are gaining wider and wider adoption, in both the industry and the everyday life. That means on one side that IoT is being more and more popular in many security critical domains. But also, that in domains that were not necessarily critical, we have devices that can now collect and transmit a lot of personal information.

This raises important security challenges. As commonly said, the “S” in IoT stands for “Security”: if it is not absent, it is at least unnoticeable. Formal methods have been used successfully for years in highly critical domains, now they can help to bring security into the IoT field. Frama-C is a source code analysis platform that aims at conducting verification of industrial-size programs written in ISO C99 source code. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language: ACSL

Tutorial goals
Participants will learn how to use the different FramaC analyzers and how to combine them. Several examples and use cases presented during the tutorial will give them a clear practical vision of possible usages of the underlying static and dynamic analyses in their everyday work. The presented code fragments are part of Contiki , a realworld lightweight operating system for the IoT. Each part consists of a presentation using slides and live demonstration, and a session of exercises. To work on the exercises, the attendees will be provided a virtual machine image for VirtualBox containing all the tools ready to use. We will also provide additional exercises and we will be available during the conference (and after) to help the attendees who may want to go beyond the tutorial material.