Verification of usbkbd

What is it?

This project verified Linux's USB Boot Protocol Keyboard Driver (usbkbd), shipped with the Linux kernel.

As far as we know, prior to this work, no device driver verification has been carried out that successfully combines:

• verifying software not written with verification in mind, and
• using a sound approach (we don't "try to find bugs", but "prove absence of bugs"), and
• not avoiding concurrency (concurrency is common in this driver, and we do prove absence of race conditions), and
• not relying on any bounding (there's an unbounded number of threads, unbounded number of keyboards, unbounded amount of time the driver is running, ...)

By performing verification, we found two bugs in the driver, of which the fixes are both accepted by the maintainer (patch1, patch2).

Download sourcecode

• Download VeriFast from [link] and look in the examples/usbkbd directory.

Paper

• Paper [PDF]: Sound formal verification of Linux’s USB BP keyboard driver,
  Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens,
  in: NFM 2012, Vol. 7226 of LNCS, Springer, Heidelberg, 2012, pp. 210-215.

Additional documentation

• Slides [PDF] : only high-level overview
• usbkbd-ghost-counters-draft.pdf: (draft) explanation on how the proof with all the counters works.
• Paper [PDF] Software verification with VeriFast: industrial case studies
  By Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, and Frank Piessens.
  Science of Computer Programming, 2014.

Which file is what

• src/usbkbd_unpatched.c: the driver as it was before fixing the bugs found during the verification process
• src/usbkbd_patch*.patch: patches to fix these bugs. These patches are accepted by the maintainer (update: since Linux 3.3 the patches are part of Linux releases)
• src/usbkbd_verified.c: driver with VeriFast annotations
• src/*/*.{h,gh}: API specifications and other ghostcode
• build/*: files to compile src/usbkbd_verified.c into a kernel module

How to launch verification

If $DIR is the directory where usbkbd_verified.c is located, execute

prompt$ cd $DIR
prompt$ verifast -I . -prover redux -c usbkbd_verified.c

How to build and load the kernel module

If $DIR is the directory where usbkbd_verified.c is located, execute as root

prompt# cd $DIR/../build/
prompt# make
prompt# insmod usbkbd_verified_build.ko

Keep in mind another kernel module (typically usbhid) might also handle USB keyboards, and "steal" away the keyboard from usbkbd_verified_build.ko. The usbhid kernel module might be autoloaded by your Linux distribution when you plug in a keyboard.

---