Secure your Things: Secure Development of IoT Software with FRAMA-C

(CANCELLED)

Authors:

  • Frédéric Loulergue
    Universite d’Orleans, France
  • Alan Blanchard
    Inria Lille North Europe, France
  • Nikolai Kosmatov
    CEA List, Gif-sur-Yvette, France

Abstract:

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.

Short Bio:

Frédéric Loulergue obtained his PhD in Computer Science from the University of Orleans in 2000 and his Habilitation in Computer Science from Universite Paris Val-de-Marne in 2004. He is currently a full professor at Northern Arizona University, Flagstaff, USA. His research interests are the practical and formal aspects of the design, implementation and application, in particular to large-scale data-intensive software, of structured parallel programming languages and libraries, as well as applied formal methods and cyber security in this broad context. Software associated to his research work include Bulk Synchronous Parallel ML (BSML) and the SYDPACC framework for the systematic development of programs for scalable computing.
He co-organized several international workshops on High-Level Parallel Programming and Applications (HLPP) and on Practical Aspects of High-Level Parallel Programming (PAPP), and the PAPP ACM SAC Track in 2016 and 2017. He co-chaired the Formal Approaches to Parallel and Distributed System (4PAD) symposium in 2016 and 2018. He is a member of the editorial board of Scalable Computing: Practice and Experience. He was associate director of the Laboratory of Algorithms, Complexity and Logic (LACL), and associate director of the Laboratoire d’Informatique Fondamentale d’Orleans (LIFO). He founded and lead the Logic Modeling and Verification (LMV) research team at LIFO (2015-16).
Web site: http://frederic.loulergue.eu