Protecting Against Malicious Bits On the Wire: Automatically Generating a USB Protocol Parser for a Production Kernel

Recent efforts to harden hosts against malicious USB devices have focused on the higher layers of the protocol. We present a domain-specific language (DSL) to create a bit-level model of the USB protocol, from which we automatically generate software components that exhaustively validate the bit-level syntax of protocol messages. We use these generated components to create a stateful, connection-tracking firewall for USB. We integrate this firewall with the FreeBSD kernel and demonstrate that it achieves complete mediation of USB traffic, thus protecting the rest of the kernel, including higher-level policy mechanisms such as USBFilter, from low-level attacks via maliciously crafted packets.

In addition to in-kernel data structures and packet validation routines, our system generates a user-level policy engine that allows for flexible and expressive firewall behavior beyond mere message syntax validation, as well as functions for pretty-printing packets (which can be used in both the kernel and in protocol analysis software). We use a Haskell back-end to generate C code that we integrate with the FreeBSD kernel, thus making our entire system amenable to formal verification.