Projects

The Wookey project

_images/link.png

The USB bus has been a growing subject of research in recent years. More specifically, securing the USB stack (and hence the USB hosts and devices) started to draw interest from the academic community since major and massively exploitable flaws have been revealed with the BadUSB threat [1].

The work presented in this project takes place in the design initiatives that have emerged to thwart such attacks, targetting the USB device security. The security model is based on both hardware and software primitives designed to bring in-depth security.

ewok

Hardware security relies on an extractable token embedding a secure element. This token is meant to provide a pre-boot authentication feature as well as a secure storage area for the sensitive master keys of WooKey user data encryption.

Software security relies on a microkernel that enforces privilege separation, memory isolation, W⊕X principle, stack and heap anti-smashing techniques. The most sensitive parts are implemented with a safe language (SPARK/Ada).

The secure update mechanism over USB is based on the DFU (Device Firmware Update) protocol. It also uses the pre-boot user authentication feature to strengthen the security of the platform. Firmware integrity and authenticity are based on state of the art cryptography.

[1]BadUSB-On accessories that turn evil, Karsten Nohl and Jakob Lell, Black Hat USA, 2014

The EwoK secured micro-kernel

_images/link.png

EwoK microkernel is a part of the Wookey project. It targets micro-controllers and embedded systems. It aims to bring an efficient hardening of embedded devices with a reduced impact on the device performances.

EwoK has been designed to host complex drivers in userspace. Unlike most of other microkernels, the goal is to support complex software stacks (ISO7816, etc.) as well as high performance (USB, SDIO, CRYP) drivers. This makes EwoK valuable for multiple use cases, including high speed and security targeted devices.

ewok

Security properties

EwoK supports the following properties:

  • Strict memory partitioning
  • Strict partitioning of physical resources (devices, etc.)
  • Fixed permissions management, set at compile time and easily verifiable
  • Kernel Random Number Generation support (based on TRNG HW on STM32)
  • Stack smashing protection (SSP) in both kernel and userspace tasks
  • Userspace Heap/Stack smashing protection
  • Proved W^X memory mappings
  • Strict temporal separation between declarative phase and execution phase
  • Fully userspace and partitioned drivers execution (including ISR execution)
  • Written in a safe language (Ada), with various proven components using SPARK