Sound formal verification of Linux's USB BP keyboard driver

Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 29 January 2020

NASA Formal Methods
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 210-215
2012
Topic(s): os tools verification
Note(s): permission logic, separation logic, concurrent-separation logic, VeriFast verifier

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.

VeriFast verifier