Modeling environment for static verification of Linux kernel modules

Abstract

Linux kernel modules operate in an event-driven environment. Static verification of such software has to take into consideration all feasible scenarios of interaction between modules and their environment. The paper presents a new method for modeling the environment which allows to automatically generate an environment model for a particular kernel module on the base of analysis of module source code and a set of specifications describing patterns of possible interactions. In specifications one can describe both generic patterns that are widespread in the Linux kernel and detailed patterns specific for a particular subsystem. This drastically reduces a specification size and thus helps to verify more modules with less efforts. The suggested method was implemented in Linux Driver Verification Tools and was successfully used for static verification of modules from almost all Linux kernel subsystems.