From CVEs to proof: Make your USB device stack great again — Cyril Deberge, Patricia Mouy, Philippe Thierry, Ryad Benadjila
Date : 03 June 2021 à 11:30 — 30 min.
Nowadays, many devices embed a full USB stack, whose main components are made of software elements dealing with hardware IPs. USB sticks, hard-disk drives, smartphones, vehicles, industrial automatons, IoT devices: they all usually offer a USB physical connection, and a USB software driver dealing with it. In critical environments where attackers are able to tamper with this interface, any exploitable software Run Time Error (RTE) such as a buffer overflow might lead to a remote code execution on the vulnerable device, usually in privileged mode. This is even worse when the USB stack runs from a BootROM, yielding unpatchable software. This matter of fact exhibits the need for a portable RTE-free USB stack with concrete proofs: the current article proposes an open-source implementation of such a stack using the Frama-C framework, with proofs and various use cases (DFU, HID and mass storage, and more to come). Beyond providing the mere implementation, we bring a generic methodology to adapt complex protocols software stacks to Frama-C with strong embedded contexts constraints.
Les piles USB sont très représentées dans le monde de l'embarqué, et sont composées de modules logiciels pilotant une IP matérielle dédiée. En effet, des clés USB aux véhicules en passant par les smartphones, les systèmes industriels et les objets connectés, tous comportent en général au moins une interface de ce type. Dans les environnements sensibles et critiques où cette interface est accessible à des attaquants, la moindre vulnérabilité (RTE) exploitable peut se transformer en prise de contrôle de l'équipement, souvent au niveau de privilège le plus élevé. Les conséquences deviennent dramatiques lorsque cette pile USB est implémentée dans une BootROM, rendant la vulnérabilité impatchable sans révision matérielle. Cet état de fait soulève l'importance d'avoir à disposition une pile USB portable et possédant des garanties de sécurité contre les RTEs. Le présent travail propose donc une pile USB open source avec des preuves utilisant le framework Frama-C, implémentant les classes DFU, MSC et HID, modulaire et extensible. Au delà du code source de cette pile, nous discutons de la méthodologie de preuve qui possède un aspect générique et adaptable à d'autres cas d'usage de l'embarqué.