Klever

Klever is a software verification framework designed to automate the checking of industrial systems written in GNU C against a variety of requirements. It employs software model checkers — automatic static verification tools that apply advanced static analysis techniques such as Counterexample-Guided Abstraction Refinement (CEGAR) (Mandrykin, 2013).

Software model checking (Handbook, 2018) enables the detection of faults that are often difficult to uncover with other quality assurance methods, including code review, testing, and conventional static analysis. Moreover, it can formally prove the correctness of programs with respect to specific requirements under certain assumptions.

Klever currently supports verification of Linux kernel loadable modules, Linux kernel subsystems and BusyBox applets. This can be further extended by developing corresponding configurations, specifications and, perhaps, adapting Klever components to specifics of target software.

Klever uses our fork of CPAchecker as its primary verification engine, but other tools from the Competition on Software Verification (SV-COMP) can also be used. Klever can detect:

• memory safety errors using Symbolic Memory Graphs (SMG) (Vasilyev, 2020), (Dudka, 2024);
• data races using thread-modular analysis with projections (Andrianov, 2021), (Andrianov, 2020);
• incorrect usage of the most popular Linux kernel API (LDV, 2015) using predicate analysis (CPAchecker, 2024).

Using formal specifications, Klever generates environment models that simulate interrupts, timers, callbacks for various device types (USB, PCI, SCSI, NET, etc.), file system operations, and other widely used interfaces. This approach achieves over 50% code coverage for Linux device drivers and subsystems. False alarm rates range from 0% to 80%, depending on the checked requirements. Verification results can be incrementally improved by refining existing specifications and adding new ones.

Klever includes a multi-user web interface to manage verification processes and support expert assessment of results. The interface displays code coverage, error traces, and statistics such as the number of detected bugs and false alarms. An error trace contains all statements from the program entry point to the detected error, supplemented with with possible values of variables and function arguments. Most details are collapsed by default to keep traces comprehensible. Experts can assign marks that are automatically associated with all similar error traces, so the results can be compared across different runs.

Found bugs

Klever has been used to find a several hundred acknowledged bugs in the Linux kernel:

• commits since 2024
• commits up to 2022
• Linux Driver Verification list up to 2019
• LDV list for CPAchecker

Publications

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

1. I.Zakharov, M.Mandrykin, V.Mutilin, E.Novikov, A.Petrenko, A.Khoroshilov, 2015. Configurable toolset for static verification of operating systems kernel modules. (doi)
2. E.Novikov, I.Zakharov, 2018. Towards automated static verification of GNU C programs. (doi) (forge)
3. E.Novikov, I.Zakharov, 2018. Verification of Operating System Monolithic Kernels Without Extensions. (doi) (forge)
4. E.Novikov, 2019. Klever: Enabling Model Checking for the Linux Kernel. (forge)
5. I.Zakharov, E.Novikov, I.Shchepetkov, 2023. Klever: Verification Framework for Critical Industrial C Programs. (doi)

Additional resources

Klever read-only mirrors:

• https://github.com/ldv-klever/klever.
• https://forge.ispras.ru/projects/klever

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

Klever Documentation

The Klever documentation provides detailed deployment instructions, a tutorial with basic workflow, manuals for various use cases and some instructions for developers. You can find it online at http://klever.readthedocs.io or build it yourself.

To build the Klever documentation you need:

• Install Python 3.4 or higher.

• Install Sphinx and its Read the Docs theme, e.g.:

  pip3 install sphinx sphinx_rtd_theme
  

  or in a more reliable way:

  pip3 install -r docs/requirements.txt
  

• Execute the following command from the source tree root directory (it should be executed each time when the documentation might be changed):

  make -C docs html
  

Then you can open generated documentation index "docs/_build/html/index.html" in a web browser.