I have a hypothesis about device drivers that I haven't quite worked out how to test yet.
First, I suspect many drivers would benefit from model checking as a particular kind of formal verification; I think that might be particularly good for eliminating hangs and race conditions, especially on cancelation and error paths. (I'd appreciate pointers to people who've done this; somebody must have tried, right?)
Second, I think the models to be checked can be split into an OS-behavior model that's generic across a whole class of devices, plus a device-behavior model that's OS-independent, as demonstrated by the Termite research project (https://trustworthy.systems/publications/nictaabstracts/Ryzhyk%5FWKLRSV%5F14.abstract). Termite 1 leaned fully into program synthesis to completely automatically generate device drivers; Termite 2 came from the observation that human judgment was still necessary for quality but that synthesis could be used as a specialized auto-complete; and I'm suggesting that even the auto-complete isn't necessary. Formal verification alone would be a huge improvement over the current state, and I think existing tooling is closer to supporting that goal on real drivers. (Maybe spin and modex can do much of this today? I also considered CBMC but I think some support for temporal logic might be important.)
Third, I bet OS-independent device models would be useful for capturing and validating beliefs formed while reverse engineering closed-source drivers. I envision tools for checking that a register trace conforms to the model, or model-checking a reverse-engineered binary.
Fourth, I hope those OS-independent models could be shared between well-established operating systems like Linux and the BSDs, while also enabling new experimental operating systems to get up to speed more quickly. I feel like the biggest barrier to building new operating systems is the lack of device drivers, but sharing C source code between different kernels is super messy because OS-specific design decisions get mixed in, the result is hard to review or maintain, and of course I'd prefer not to be limited to C. If sharing is at the level of "this is how this device works, do whatever you want with that", but it's machine-checkable that each driver matches the model, I think that might be the best possible option for sharing this knowledge and effort.
I'd love pointers to related work or just discussion of pros and cons of these thoughts!
Mastodon Feed
