We released Klever 3.5 that has following noticeable changes:
- Improving support for verification of Linux 5.10 and Linux 5.17 (new specifications set "5.17" was added).
- Environment models generated at verification of Linux loadable kernel modules do not contain infinite loops anymore. This accelerated analysis and did not result in any degradation in the quality of verification results.
- Using Ubuntu 20.04, Debian 11 and openSUSE 15.3 as preferable Linux distributions for deployment of Klever.
- Switching to Python 3.10. You should carefully read this comment if you are going to update existing local instances of Klever.
- Supporting regular expressions for assessing unsafes (you can see #11513 for more details).
- Updating Klever Tutorial, in particular using verification of loadable kernel modules of Linux 5.5 as an example.
- Updating add-ons and verification back-ends (various bug fixes and optimizations).
- More advanced authorization of new users. Now the administrator should activate new users while somebody should grant them access to some jobs.
Many thanks to everybody involved!
Уважаемые коллеги!
Redmine обновился до версии 5.0.0.
Просьба сообщать об обнаруженных проблемах.
Ilya Shchepetkov gave us a lot of brilliant ideas, considerably improved Klever deployment facilities, developed Clade and contributed to CIF (Klever actively uses both these tools at various stages of its operation). We would like to thank him from the bottom of our hearts and wish him new great achievements as a Senior Research Developer at Kaspersky.
Klever 3.4 includes the following prominent features:
- Several improvements contributing development and generation of environment models:
- Ability to specify savepoints for the main process.
- Ability to select scenarios for particular savepoints manually.
- Ability to configure the number of iterations for invocation of callbacks.
- Providing users with a graphical representation of environment models directly in the Klever web UI.
- Models for kmem_cache functions for the Linux kernel.
- Updating add-ons and verification back-ends (various bug fixes and optimizations).
- New sections in the user documentation: Configuring Program Decomposition and Development of Verifier Profiles.
- Besides, you can find the CIF’s user documentation that may be helpful at development of advanced specifications and models.
- Many fixes and minor improvements that make the specification development and verification workflow more easy, correct and reliable.
We highly appreciate efforts of developers and the feedback from users who made this release possible!
We are glad to announce the release of CIF 1.0!
You can download binaries suitable for your architecture from the Files section.
The user documentation is available at https://cif.readthedocs.io.
Many thanks to everybody, who developed CIF, tested it and reported various issues.
Уважаемые коллеги!
Redmine обновился до версии 4.2.3.
Просьба сообщать об обнаруженных проблемах.
Ilja Zakharov was one of the greatest contributors to the Klever project. He was the primary developer of such components as Environment Model Generator, Program Fragment Generator, Schedulers and Controller. Besides, he created a lot of environment model specifications for different kinds of target programs and made considerable scientific researches. We appreciate his work very much.
Recently Ilja Zakharov became a Verification Engineer at the Runtime Verification company. There he will be engaged in application of formal methods for smart contracts and tools used for their verification. We wish him good luck and hope that the gained experience will help him at the new position.
The most noticeable work in Klever 3.3 is a new section Development of Environment Model Specifications in the user documentation. Besides, there are following considerable improvements:
- Fixing allocation of memory for arguments of callbacks of several vital Linux device driver types.
- Enhancing environment model specifications for file systems.
- Simplifying development of environment model specifications and fixing some bugs at their processing
- Numerous enhancements of the Klever web UI that simplify several common use cases.
- Updating dependencies and addons that make them more functional and robust.
- Development of unit tests for deployment of Klever within the OpenStack cloud
- Supporting deployment at openSUSE.
- New section Development of Common API Models in the user documentation.
We would like to thank those developers and users who actively contributed to Klever 3.3!
The major improvement of Klever 3.2 is a new environment model generator that supports automated splitting of complex environment models into sets of smaller ones. This is extremely helpful at verification of large programs and program fragments when verification tools often can not provide definite answers within specified time limits.
Other important changes are as follows:
- Substantially fixed and enhanced representation of violation witnesses (error traces) and code coverage reports as well as navigation through them.
- New environment models for the Linux kernel (the bitmap API and several functions working with strings).
- New validation set on the base of faults found by Klever and fixed in the Linux kernel.
- Supporting more reliable and efficient deployment of Klever within the OpenStack cloud.
- New section Analysis of Code Coverage Reports in the Klever tutorial.
In addition, Klever 3.2 includes numerous minor improvements and bug fixes.
This release would not be possible without intensive work of developers and testers. Also, we always look forward and welcome a feedback from users.