Sorbonne Université, Tour 15/16, 101, Paris "Open Source",IoT,Embarqué,"Sécurité critique"
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.
Emmanuel Chailloux ( LIP6 - Unité Mixte de Recherche de Sorbonne Université et du Centre National de la Recherche Scientifique), Pierre Ficheux (SMILE)
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.
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.
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.
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.
Natalya Rozhnova is a research engineer at Nokia
Philippe Trébuchet is an agent at Agence nationale de la sécurité des systèmes d'information (ANSSI)
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 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.