23-Aug-2021: Finding bugs related to memory errors in Linux Kernel

Submitted by Vadim Mutilin on Mon, 23/08/2021 - 16:31

Nadezda Lutovinova has finished the GSoC 2021 project “Finding bugs related to memory errors in Linux Kernel and improving environment model specifications for static verification”. Her project was related to finding memory errors in Linux drivers code. During the work Nadezda has used Klever - a software verification framework that is created for automated checking of programs developed in the C programming language. It was used to analyze the Linux kernel version 5.12-rc3 code.

She shared an opinion, that Klever is a quite convenient tool. If a possible error is detected it shows the necessary conditions for the variables and the order of function calls leading to the error. However, the principle of finding and highlighting errors is not always clear. It happens that Klever identifies something as a bug, while skipping the exact same possible error before.

Nadezda has analyzed 18 warnings, that were previously classified as bugs but remained in doubt:

  • 7 occurred to be false positive:
    • 3 related to EMG (Environment Model Generator).
    • 4 related to incomplete models of functions.
  • 8 bugs:
    • 5 reported, prepared patches, see below.
    • 3 similar bugs in different modules reported in one message.
  • 3 remain unclear.

Most of all warnings were related to requesting IRQ before initializing necessary data. In some files there were special conditions to prevent errors, but Klever wasn’t able to recognize them due to the above problems.

Patches: