October 7-11, 2019
Porto, Portugal
The tutorial will take place on 10th of October in the morning.
The Virtual Machine is available here.
The slides are available here.
Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), have proliferated very quickly in the past years. There are now billions of interconnected devices, and this number is growing. It is anticipated that by 2021, about 46 billions of devices will be in use.
Some of these devices are in service in safety and 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. Moreover insufficiently secured devices may be used for example for massive distributed denial of service attacks. This raises important security challenges. Formal methods have been used successfully for years in highly critical domains, now they can help to bring security into the IoT field.
While the correctness of an implementation with respect to a formal functional specification provides the strongest form of guarantee, it can be very costly to achieve. In practice it is therefore more common to rely on a combination of formal methods to achieve an appropriate degree of guarantee: static analyses to guarantee the absence of runtime errors, deductive verification of functional correctness, dynamic verification for parts that cannot be proved using deductive verification.
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size programs written in ISO C99 source code. Frama-C fully supports the combination of formal methods approach, by providing to its users with a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. Moreover 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.
Recently Frama-C has been applied [1, 2, 3, 4, 5, 6] to the verification of software in the context of the Internet of Things, more specifically the verification of modules of Contiki, an open source operating system for the IoT.
This tutorial will be of interest for both researchers and practitioners interested in software verification in general, and in particular in IoT software, as well as for students in Software Engineering. The tutorial only assumes knowledge of the C programming language.
Participants will learn how to use the different formal analysis techniques 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 real-world lightweight operating system for the IoT.
A (VirtualBox) Virtual Machine containing Frama-C and the examples is available through this link.
The proposed tutorial duration is 180 minutes: about 20 minutes for the introduction including an overview of Frama-C and Contiki, 50 minutes for each of the 3 main parts, and 10 minutes for conclusion.
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 containing all the tools ready to use.
In more detail, the tutorial will be structured as follows:
A similar tutorial was presented at