Klever: a verification framework for models of industrial software

Klever: a verification framework for models of industrial software

Klever is a framework for verifying models that are automatically extracted from large software systems’ source code written in the C programming language. Klever allows specifying various security and safety requirements and verifying them automatically with the preconfigured precision level.

Features and advantages

Klever is a result of advanced research and development in the field of automated extraction and verification of program models. The framework base includes per-component verification, environment modeling, and requirements specification methods. This allows applying formal methods to the industrial software of hundreds of thousands or millions of lines of the C source code. Klever is an open-source project (https://forge.ispras.ru/projects/klever).

Klever provides:

• Thorough sound analysis of industrial software (allows detecting all possible errors of of specified types and proving program correctness under explicitly stated assumptions).
• Scalability. Modular program verification allows applying the most rigorous program analysis methods to the large code base. The methods are model checking and symbolic execution.
• Adapting software verification framework to customer needs. Developing specifications for modeling target programs’ environments and for detecting violations of program specific requirements. This specific customization is performed in addition to checking regular safe programming rules for the C language.
• Comprehensive representation of found faults. When an error is detected, the verification system provides the detailed error trace that includes concrete variable values and called functions’ arguments.
• A convenient multi-user web-interface for setting and running verification and for expert analysis of verification results.

Who is Klever target audience?

• Companies developing safety-critical and security-critical software.
• Certification laboratories.

Klever deployment stories

The Klever verification system is mostly used for thorough checking of various operating system kernels and drivers. To showcase Klever features, it was used for verification of Linux kernel device drivers. As a result more than 400 errors of the following types have been found: buffer overruns, null pointer dereferences, uninitialized memory usages, double or incorrect memory deallocations, memory leaks, race conditions and deadlocks, incorrect function calls (depending on a certain context), incorrect initialization of Linux kernel data structures etc. Linux kernel developers have acknowledged these errors.

System Requirements

Ubuntu 18.04/20.04, at least 4 x86-64 CPU cores, 16 GB of memory, 100 GB of disk space.

Workflow

Developer/Participant

Software Engineering