One million (LOC) and counting: Static analysis for errors and vulnerabilities in the Linux kernel source code

Abstract

This article describes an analysis tool aimed at the C code of the Linux kernel, having been first described as a prototype (in this forum) in 2004. Its continuing maturation means that it is now capable of treating millions of lines of code in a few hours on very modest platforms. It detects about two uncorrected deadlock situations per thousand C source files or million lines of source code in the Linux kernel, and three accesses to freed memory. In distinction to model-checking techniques, the tool uses a configurable "3-phase" programming logic to perform its analysis. It carries out several different analyses simultaneously. © Springer-Verlag Berlin Heidelberg 2006.