DiffKemp: Automatic analysis of semantic differences in kernel options
DiffKemp is a framework for automatic static analysis of semantic differences between different versions of large-scale C projects. Our main target is the Linux kernel, in particular the kernel of Red Hat Enterprise Linux (RHEL).
The RHEL kernel contains a list of functions, so-called Kernel Application Binary Interface (KABI), which are guaranteed to remain stable across a single major RHEL release. The purpose of DiffKemp is to automate checking of semantic stability of these functions, allowing the process of the kernel development and deployment to be more efficient and reliable.
The approach of DiffKemp is based on compiling the code to be compared into LLVM IR followed by using a combination of light-weight program transformations and pattern matching to analyse the code. Thanks to this unique method, DiffKemp is able to analyse semantic equivalence of code of the size of the Linux kernel in the order of minutes while providing a very low number of false positive results. To the best of our knowledge, this is beyond capabilities of any other existing approach.
For more information, please refer to the article by Viktor Malik in Red Hat Research Quarterly magazine Volume 1, Issue 4, available here.