Efeu: generating efficient, verified, hybrid hardware/software drivers for I2C devices

Writing device drivers is notoriously hard, and driver bugs are a major cause of system failures and vulnerabilities. The problem is particularly acute in bus-based protocols like I 2 C, where driver correctness is only half the story: correct functioning of the complete subsystem depends on all components on the bus interoperating correctly. Unfortunately, developers cannot control all aspects of a platform, and must interact with existing devices (peripherals and/or hardware bus controllers) which may misbehave. Failures in a protocol like I 2 C, often used in critical low-level system management, can result in permanent damage to the hardware, whether a server or a satellite.

Existing techniques for creating high assurance drivers rarely tackle this interoperability issue. We present Efeu, a framework for implementing verifiably interoperable drivers for I 2 C devices. Using model checking-based verification, Efeu generates driver implementations in software, reconfigurable logic for FPGAs, and, notably, combinations of both. The split between software and hardware can be varied at implementation time and the hardware/software interface is generated automatically, enabling efficient exploration of the design space. Using Efeu, we design and evaluate a verified I 2 C driver stack, and demonstrate that Efeu finds optimal hardware/software tradeoffs to favor either throughput, CPU usage or FPGA footprint. For each objective, Efeu generates drivers with performance comparable with hand-optimized hardware/software drivers.