The Open Source
Innovation Spring 2019

Qualité logicielle | IoT | Cloud | Big Data | Systèmes d'information

Mars-juin 2019, Paris - Châtillon

Présidence : Roberto Di Cosmo, vice-président du GTLL, directeur de l’Irill, directeur de recherche Inria, Professeur à l’Université Paris-Diderot

Organisé par : logo Systematic & logo IRILL

Retour à l'OSIS

IoT & Embarqué critique

13 Juin 2019 — IoT & Embarqué critique

14h-17h

Sorbonne Université, Tour 15/16, 101, Paris "Open Source",IoT,Embarqué,"Sécurité critique"

Résumé

L'événement a pour but de présenter sur une après-midi les technologies permettant d'assurer la qualité des logiciels/OS embarqués dans les équipements IoT.

Direction de programme

Emmanuel Chailloux ( LIP6 - Unité Mixte de Recherche de Sorbonne Université et du Centre National de la Recherche Scientifique), Pierre Ficheux (SMILE)

Description détaillée

Programme résumé

  • 14:00: State of the art in security for embedded systems and IoT

    Pierre Ficheux

  • 14:40: Transparent remote connectivity to short-range IoT devices

    Natalya Rozhnova

  • 15:20: Pause

  • 15:40: Proof of Pointer Programs with Ownership in SPARK

    Yannick Moy

  • 16:20: WooKey: USB Devices Strike Back

    Philippe Trébuchet

  • 17:00: Pot


Programme détaillé

  • 14:00 - State of the art in security for embedded systems and IoT

    Pierre Ficheux

    The conference will describe the main concepts of security for embedded and IoT solutions : security vs safety, IT vs OT, main standards, level of security of available operating systems (Linux, Android, etc.), examples of attacks and secure solutions.

  • 14:40 - Transparent remote connectivity to short-range IoT devices

    Natalya Rozhnova

    Short-range wireless communication technologies such as Bluetooth or ZigBee represent an important part of the Internet of Things ecosystem.

    By design, this category of smart devices has physically limited reachability inside their Wireless Personal Area Network (WPAN) and are not directly compatible with the TCP/IP stack.

    However, users may need to access them from anywhere at any moment.

    To address this problem, we design a new application-agnostic approach called RCM (Remote Connection Manager) enabling transparent communication between an application and out-of-range devices.

    It creates new IoT use cases by seamlessly mixing remote and local devices.

    We implemented an open-source prototype for Bluetooth Low Energy (BLE) technology on top of Linux and Android BLE stacks and demonstrated its efficiency through experiments performed on real devices.

  • 15:20 - Pause

  • 15:40 - Proof of Pointer Programs with Ownership in SPARK

    Yannick Moy

    Pointers are a notorious "defect attractor", in particular when dynamic memory management is involved. Ada mitigates these issues by having much less need for pointers overall (thanks to first-class arrays, parameter modes, generics) and stricter rules for pointer manipulations that limit access to dangling memory. Still, dynamic memory management in Ada may lead to use-after-free, double-free and memory leaks, and dangling memory issues may lead to runtime exceptions.

    The SPARK subset of Ada is focused on making it possible to guarantee properties of the program statically, in particular the absence of programming language errors, with a mostly automatic analysis. For that reason, and because static analysis of pointers is notoriously hard to automate, pointers have been forbidden in SPARK until now. We are working at AdaCore since 2017 on including pointer support in SPARK by restricting the use of pointers in programs so that they respect "ownership" constraints, like what is found in Rust.

    In this talk, I will present the current state of the ownership rules for pointer support in SPARK, and the current state of the implementation in the GNAT compiler and GNATprove prover, as well as our roadmap for the future.

  • 16:20 - WooKey: USB Devices Strike Back

    Philippe Trébuchet

    The USB bus has been a growing subject of research in recent years. In particular, securing the USB stack (and hence the USB hosts and devices) started to draw interest from the academic community since major exploitable flaws have been revealed by the BadUSB threat.


    The work takes place in the design initiatives that have emerged to thwart such attacks. While some proposals have focused on the host side by enhancing the Operating System's USB sub-module robustness, or by adding a proxy between the host and the device, we have chosen to focus our efforts on the device side.


    More specifically, our work presents the WooKey platform: a custom STM32-based USB thumb drive with mass storage capabilities designed for user data encryption and protection, with a full-fledged set of in-depth security defenses. The device embeds a firmware with a secure DFU (Device Firmware Update) implementation featuring up-to-date cryptography, and uses an extractable authentication token. The runtime software security is built upon EwoK: a custom microkernel implementation designed with advanced security paradigms in mind, such as memory confinement using the MPU (Memory Protection Unit) and the integration of safe languages and formal methods for very sensitive modules. This microkernel comes along with MosEslie: a versatile and modular SDK that has been developed to easily integrate user applications in C, Ada and Rust.


    Another strength of this project is its core guiding principle: provide an open source and open hardware platform using off-the-shelf components for the PCB design to ease its manufacturing and reproducibility.

  • 17:00 - Pot

Intervenants

  • Natalya Rozhnova

    Natalya Rozhnova is a research engineer at Nokia

  • Philippe Trébuchet

    Philippe Trébuchet is an agent at Agence nationale de la sécurité des systèmes d'information (ANSSI)

  • Pierre FICHEUX

    Pierre FICHEUX is currently CTO at Smile ECS, a software company specialized in open source technologies. Pierre is also teacher and manager for the GISTRE (Génie Informatique des Systèmes Temps Réel et Embarqués) speciality at EPITA, a famous french school of computer science.

  • Yannick Moy

    Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a technology he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

Organisateurs et/ou sponsors

Organisateurs (2019)

Co-organisateurs et sponsors (2019)

Ils parlent de l'OSIS (2019)