Generation of Environment Model for Verification of Multi-module Device Drivers

by Ilja Zakharov for The Linux Foundation

Linux Driver Verification project has the goal to provide high quality framework which allows using different static analysis tools to verify whether drivers satisfy correctness rules. Linux device drivers can't be analyzed separately from the kernel core due to their large interdependency between each other. But source code of the whole Linux kernel is rather complex and huge to be analyzed by existing model checking tools. Therefore drivers should be analyzed with environment models instead of the real kernel core. Currently LDV tools analyze only a chunk of code that is a separate loadable kernel module. Sometimes analysis of only one module leads to sophisticated or even incorrect environment model, because drivers can contain several modules or common routines from a driver are picked out to a library module. Thus environment model should be generated for groups of interacting modules rather than for separate modules of these groups.