Generating a Statically-Checkable Device Driver I/O Interface
Lea Wittie, Chris Hawblitzel, Derrin Pierret · 2007
Device drivers are known to be a main source of operating system bugs. Several research groups have created driver specification languages that dynamically check pre- and postconditions on the IO operations of a device driver. The low-level type-safe language, Clay, has the facilities to statically check the safety of a device driver but is difficult to use directly. We have created a new device driver specification language, Laddie, which compiles the IO interface of a device driver to Clay thus leveraging its static safety checking while remaining simple to use.