This paper reports on verification of a simple Linux USB keyboard driver using VeriFast. Except, of course, Linux drivers are not simple: they have asynchronous callbacks, dynamically allocated memory, synchronization and interact with complex Linux driver APIs including USB, input and spinlocks. This work found bugs in the driver and the fixes have been accepted by the maintainer.
The properties verified include freedom of data races, freedom of illegal memory accesses and correct API usage. (Though, as they point out themselves, the API spec could have bugs.)
The driver is 426 lines long, of which there are 329 lines of non-blank, non-comment code. To this, they add 769 lines of reusable API specifications and 53 lines of annotation (or maybe it is 822 lines – it is not clear whether the 822 lines of annotations includes the 769 lines of spec or not). Verification takes about 1 second.
They report that some of the concurrency patterns involved in LED handling was tricky to verify and required the introduction of “ghost counters”. They also had to reason about permissions passed between callbacks.
Notes related to Sound formal verification of Linux’s USB BP keyboard driver
Papers related to Sound formal verification of Linux’s USB BP keyboard driver
- Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]