Methods of Modular Verification of Linux KernelIlya Zakharov. Starts at May 7, 2014.
The LDV verification system is aimed at the checking of Linux core interfaces usage consistency rules by dynamically loadable modules through statistical verification tools. Simultaneous analysis of both module source code and the rest of the core code is difficult for existing verification tools due to large volume and complexity of such system’s code. Therefore, in LVD system an environment model is generated for target module, and the source code is checked by verification tools along with it. At present, it is possible to build an environment model for each individual module in the LDV system, but such model includes only interaction of module and the core. In this report we will address the problem of module interaction modeling and propose a method of solving it under the LDV system.The presentation of the report can be found here.