Overview

Klever is a software verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of requirements using software model checkers (automatic software verification tools) implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement. Software model checking allows finding faults that can be hardly detected by other software quality assurance techniques like code review, testing and static analysis. In addition, it is capable to prove formal correctness of programs checked against particular requirements under certain assumptions.

Currently Klever supports verification of Linux kernel loadable modules, Linux kernel subsystems and BusyBox applets. One can extend this list further by developing corresponding configurations, specifications and, perhaps, appropriate Klever components that will adapt the framework for specifics of target software.

For the Linux kernel Klever includes requirement specifications for detecting memory safety issues, e.g. buffer over-reads/writes and null pointer dereferences, data races and incorrect usages of the most popular Linux kernel API. On the base of specifications Klever generate environment models for invoking interrupts, timers, callbacks of different device types (USB, PCI, SCSI, NET, etc.), file system operations and some other most widely used interfaces. These environment models allow reaching more than 50% code coverage for Linux device drivers and subsystems. At the moment a false alarm rate ranges from 0% to 80% depending on checked requirements. One can incrementally improve verification results primarily by fixing existing specifications and developing new ones.

As software model checkers Klever supports various flavors of CPAchecker. Moreover, one can integrate other tools participated in the Competition on Software Verification.

For managing verification processes and for expert assessment of verification results Klever provides a multi-user web interface. It shows both details, e.g. code coverage and error traces that contain possible values of variables and function arguments as well as all statements from program entry points to found errors, and statistics like the total number of bugs and false alarms. Experts can create marks associating automatically with all similar error traces and compare verification results obtained at different times.

Bugs found by Klever in the Linux kernel and acknowledged by the developers: http://linuxtesting.org/results/ldv (commits).

You can find more information about Klever in the following papers and presentations:

Klever documentation: https://klever.readthedocs.io/en/v3.7.

Klever read-only mirror: https://github.com/ldv-klever/klever.

If you have any questions, feel free to send an email to ldv-project@linuxtesting.org.