From CVEs to proof: Make your USB device stack great again

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 [12,45], 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 [35], with proofs and various use cases (DFU, HID, 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.