Linux Kernel Space Verification
Linux kernel consists of core components implementing basic functionality of an operation system (scheduling, memory management, interprocess communication, etc.) and loadable modules that implement additional functionality (file systems, network protocols, device drivers, etc.). Loadable modules make up 70% of source code of Linux kernel, while attention paid to them is much less than attention paid to the core components. No wonder that the loadable modules are the main source of kernel crashes, hangs, and other issues.
There are two active projects of Linux Verification Center aimed to improve quality of the loadable kernel modules.
- Linux Driver Verification - a comprehensive toolset for static source code verification of Linux device drivers.
- KEDR Framework - an extensible framework for dynamic analysis and verification of kernel modules.
Static analysis and dynamic analysis complement each other nicely. Strengths and weaknesses of the two approaches are considered in details here.
Another ongoing project is Linux File System Verification that aims to develop a dedicated toolset for verification of Linux file system implementations. The central component of the toolset is Spruce system that provides run-time tests to check behaviour of file system drivers under various circumstances.
The most advanced verification techniques are investigated within Linux Deductive Verification project. The goal of the project is to improve open source deductive verification tools, so they can be used to prove properties of Linux kernel code. A target for the first round of the project is a custom LSM implementation that is a part of the Astra Linux Special Edition distribution.