Klever

Klever 3.7 was primarily devoted to improving a quality of verification results for Linux kernel drivers. After all about 43% of original false alarms issued when checking memory safety have gone.

Following fixes and improvements in Klever 3.7 deserve an attention:

• Adding new environment models for the Linux kernel:
  • Modeling the list API.
  • Modeling the kref API.
  • Adding model for the input_ff_create_memless() function.
  • Adding models for check_add_overflow(), check_sub_overflow() and check_mul_overflow() macros that fixes the struct_size() model for new versions of the Linux kernel.
  • Modeling v4l2_device(un)register()_ functions.
  • Modeling the i2c_match_id() function.
  • Adding model for the dev_err_probe() function.
  • Adding models for the dynamic debug printing API.
• Fixing existing environment models for the Linux kernel:
  • Modeling failures for calloc() and zalloc().
  • Fixing the off-by-one error when choosing a device from MODULE_DEVICE_TABLE.
  • Passing the same resource to probe and remove for HID drivers.
  • Allocating memory for inode for file_operations callbacks.
  • Allocating memory for tty_struct for tty_operations callbacks.
  • Avoiding using implicit resources in environment model specifications.
• Adding a new section to the user documentation: Verifying New Program.
• Fixing tests for environment model specifications and Environment Model Generator.
• Updating CIF which main file was rewritten in C++ and that started to print keyword static for local variables.
• Updating CPAchecker that supports packed/aligned attributes and issues violation witnesses more efficiently.
• Updating Python dependencies.

We would like to thank very much everybody who made this great job possible!