DiffKemp: Automatic analysis of semantic differences in kernel options

The project aims at creating a tool for automatic analysis of differences in the code between versions of the Linux kernel. The goal is to determine whether the semantics (the effect) of some kernel option, function, or parameter, changed between two kernel versions. The tool will help to partialy automate checking of compatibility of kernel options which will make the process of the kernel development and deployment more efficient and reliable. The approach is based on static analysis of the source code. It uses transformation of the compared programs into the intermediate representation of the LLVM (clang) compiler and advanced formal methods to prove equivalence of syntactically different programs.

For more information, please refer to the article by Viktor Malik in Red Hat Research Quarterly magazine Volume 1, Issue 4, available here.

Status

Research Area(s)

Project Resources

RIG(s)

Affiliations

Project Team

Publications