Klever

Let’s start the new year 2021 with new Klever 3.0!

Among a lot of improvements and bug fixes, most significant changes in Klever 3.0 are as follows:

• Support for verification of kernel loadable modules of Linux 5.5.
• Support for verification of Linux kernel loadable modules on the ARM architecture.
• Fixing and developing specifications for verification of Linux kernel loadable modules:
  • Fixing specifications for checking usage of clocks in drivers.
  • Support for checking usage of the RCU API.
  • Developing detailed specifications for USB serial drivers.
  • Improving environment models for runtime power management callbacks.
  • Using device identifiers from the driver tables.
  • Developing models for devm memory allocating functions.
  • Fixing framebuffer_alloc/release models.
  • Adding models for request/release_firmware(), v4l2_i2c_subdev_init() and i2c_smbus_read_block_data().
• More user-friendly configuration for target program fragments and requirement specifications.
• Development of preset tags for assessing most common false alarms.
• Support for new internal data formats for enhancing and optimizing representation and assessment of verification results.
• Support for cross-references for original program source files and models.
• Update of all variants of the CPAchecker verification back-end.
• Switching to a special version of Frama-C developed within project Deductive Verification Tools for Linux Kernel from outdated and unmaintained CIL. Both tools are used for merging source files and optimizations like removing unused functions.
• Using systemd scripts instead of init.d ones for Klever services.
• Development of Tutorial.

Klever 3.0 is not backward compatible with former versions of Klever, so, you need to remove existing instances if so and deploy Klever from scratch.

As usual many thanks are to everyone who participated in this release of Klever!