31-Aug-2020: Development of environment model specifications for static verification of Linux Kernel

Nadezda Lutovinova has finished the GSoC 2020 Project "Development of environment model specifications for static verification of Linux Kernel" for The Linux Foundation.

In the project she has used Klever - a software verification framework that is created for automated checking of programs developed in the C programming language. Klever includes requirement specifications for detecting memory safety issues in the Linux kernel. Klever analyzes code and issues warnings about possible errors. Not all of them are real bugs. Nadezda has analyzed Klever’s verdicts and marked them into true bugs and false alarms. False alarms can occur due to inaccuracies in the various components of Klever. In particular, in SMG (Symbolic Memory Graph) technique, which is used for detecting memory safety issues, and in EMG (Environment Model Generator), which generates environment models for analyzed functions.

Klever is a quite convenient tool. It displays not only the sequence of calls that led to the error, but also the conditions on the variables necessary for this. When there is no necessary information, it continues to work, assuming its value. Also it is possible to compare jobs with different models and see in detail the differences in the results. At the same time there are some negative points, which she has noticed. There are some problems with display of error traces (incomplete display of lines of code, lack of a clear correspondence between passed arguments and internal names of functions in trace, some files cannot be opened by link from the trace, etc). Also the tagging system is not completely clear. Necessity to make models for a lot of functions to improve accuracy also complicates work with this tool.

Initially, it was supposed to develop and improve models for operations with strings. But no errors related to incorrect string models found during the analysis. So the models for strings functions did not need to be improved. More often errors were incomplete kernel environment models, especially with operations from debugfs.h and incomplete models for lists operations.

Analysis of warnings

Nadezda analyzed 62 issued warnings for the Linux kernel modules of version 5.7-rc7.
She found two bugs and reported it. For the first bug she prepared a patch which was accepted, see LKML. Report for the second bug is here.

60 false positive warnings were analyzed and marked into the following classes:

• 1 related to problem in KLEVER (e.g. error in displaying of a track)
• 13 related to problem in SMG (e.g. SMG assumes opposite statements)
• 5 related to EMG models (e.g. memory leaks because of incorrect freeing of memory)
• 41 related to incomplete models of functions (e.g. without model for __builtin_mul_overflow() model of devm_kcalloc() working incorrect and NULL pointer dereference occurs)
  • 12 of them related to lack of models for some functions from debugfs.h (e.g. without model for debugfs_create_dir() subsequent execution of debugfs_remove(), which works with pointer returned from debugfs_create_dir(), does not occur correctly) [Tags: EMG, EnvSpec, debugfs]
  • 6 of them related to incomplete models for lists operations (e.g. __list_add do not add new element to list so memory leak occurs) [Tags: KernelModel, list_add]
  • 4 of them related to lack of model for nvmem_cell_read() [Tags: EMG, EnvSpec]
  • 2 of them related to lack of model for acpi_evaluate_object() [Tags: KernelModel]
  • 2 of them related to lack of model for is_acpi_device_node() [Tags: KernelModel]
  • 2 of them related to lack of model for drm_dev_init() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for kvfree() [Tags: KernelModel]
  • 1 of them related to lack of model for acpi_evaluate_object_typed() [Tags: KernelModel]
  • 1 of them related to lack of model for memdup_user() [Tags: KernelModel]
  • 1 of them related to lack of model for __builtin_mul_overflow() [Tags: KernelModel]
  • 1 of them related to lack of model for i2c_smbus_read_block_data() [Tags: KernelModel, i2c_smbus_read_block_data]
  • 1 of them related to lack of model for devm_hwrng_register() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for vchan_init() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for iscsi_boot_create_acpitbl() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for mipi_dsi_device_register_full() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for drm_random_order() [Tags: EMG, EnvSpec]
  • 1 of them related to lack of model for gb_hd_create() [Tags: EMG, EnvSpec]
  • 1 of them related to incomplete model for acpi_get_object_info() [Tags: CIF]
  • 1 of them related to incomplete model for krealloc() [Tags: CIF]

Lists specification

Nadezda developed improvements for list model for the Klever and tested them on the Linux kernel version 5.7-rc7. The improvements can be found on github.

Results of implementation of new lists models: