Partner INRIA and partner CEA attended the 34th ACM SIGAPP Symposium on Applied Computing (SAC 2019). During the Software Verification and Testing slot, they gave a presentation on “Logic Against Ghosts: Comparison of two Proof Approaches for Linked Lists”. In addition to that they gave a tutorial on “Formal Verification for an Internet of Secured Things”.
Connected devices and services, also referred to as the Internet of Things (IoT), are becoming more and more popular. These devices are now used in many security-critical domains. Moreover, even in non-critical domains, 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 these devices. This kind of guarantees can be brought using formal verification. In the tutorial, we describe several formal verification techniques and present them by applying 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. Participants will learn how to use the different Frama-C analyzers and how to combine them. Several examples and use cases presented during the tutorial give them a clear practical vision of possible usages of the underlying static and dynamic analyses in their everyday work.