Ivannikov Institute for System Programming of the RAS


LDV. A technology for static verification of Linux kernel drivers

Bugs in Linux kernel drivers directly affect security, reliability and performance of the kernel and user space applications. Code review, automated testing and static analysis allows detection quite a lot of bugs in Linux kernel drivers. However, just static verification aims at identifying all bugs of a particular type.

Configurable framework for static verification of Linux kernel drivers LDV KLEVER provides means for automated preparation of source code of drivers for verification on the base of environment model specifications and checking it against correctness rule specifications using static verification tools.

LDV KLEVER includes environment model specifications of the 20 most widely used interfaces for drivers such as interrupt handlers, timers, USB and PCI device interfaces, network interfaces and interfaces for character device drivers.

LDV KLEVER includes 34 rule specifications for checking correct usage of the Linux kernel API in drivers to detect bugs, such as:

  • specific resource leaks,
  • incorrect usage of synchronization primitives,
  • function calls with inappropriate argument values depending on execution context,
  • incorrect initialization of specific data structures.

Besides, the configurable framework for static verification of Linux kernel drivers allows detecting other kinds of bugs, for instance:

  • buffer overflow,
  • null pointer dereference,
  • uninitialized memory usage,
  • memory leak,
  • double or incorrect memory release.

Currently, LDV KLEVER uses such static verification tools as CPAchecker, BLAST and CBMC.

Depending on verification results LDV KLEVER renders verdict for each pair of a driver and a correctness rule:

  • Safe – rule satisfiability is proven,
  • Unsafe – a rule violation is found,
  • Unknown – failed to check the rule.

In case of verdict LDV KLEVER Unsafe provides a user with an interactive error trace describing a full annotated execution path in driver source code that leads to an error with all particular variable values. For conducting verification and result analysis LDV KLEVER provides a Web interface.

LDV KLEVER helped to detect more than 250 bugs in Linux kernel drivers that were accepted by the kernel developers (http://linuxtesting.org/results/ldv).

LDV. A technology for static verification of Linux kernel drivers

For instance, for Linux 3.14 driver drivers/usb/serial/kobil_sct.ko a violation of rule linux:alloc:irq was detected for configuration allmodconfig on the x86_64 architecture. This rule requires that resources should be allocated in the nonblocking manner when being in the interrupt context. Otherwise performance degradation or even halts can happen.

When initializing the driver — ldv_insmod — USB Serial callbacks were registered. Then the main scenario ldv_usb_serial_scenario was executed.

The environment model simulated a connection of a USB Serial device. This device was successfully initialized by the driver during execution of callbacks probe and attach. Then the environment model simulated invocation of terminal level callbacks: opening a port open (kobil_open) and writing data write (kobil_write).

In kobil_open the driver allocates memory in the blocking way. This operation is correct since this callback is called in the process context. In kobil_write memory is also allocated in the blocking manner but this is a bug since this callback is being invoked within the interrupt context.

Error Trace Visualization

LDV. A technology for static verification of Linux kernel drivers

LDV page

Developer/Participant

Software Engineering

Back to the list of technologies of ISP RAS