24-Jun-2014: The LDV team gave a talk at the 9th Ershov Informatics Conference

LDV team member Ilja Zakharov gave a talk “Modeling Environment for Static Verification of Linux Kernel Modules” at the 9th Ershov Informatics Conference. The talk presented results of joint research with Alexey Khoroshilov, Vadim Mutilin and Evgeny Novikov dedicated to modeling environment of Linux kernel modules for the purpose of their static verification using modern software model checking tools.

The 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 the modules and their environment. In the talk Ilja presented 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. Generated C code that being combined with original kernel module source code provides verification tools a program which contains all feasible interactions. The method allowed to perform verification of almost all kernel subsystems with help of LDV Tools obtaining sufficiently low number of false alarms and low rate of missed errors.

See details in [Khoroshilov A., Mutilin V., Novikov E., Zakharov I. Modeling Environment for Static Verification of Linux Kernel Modules. Proceedings of PSI, pp. 116-125, 2014.]