Automatic Construction of Kernel Core Model

by Ilya Shchepetkov for The Linux Foundation

Linux Driver Verification (LDV) program is devoted to developing an integrated framework for device drivers verification and adopting leading edge research results to enhance quality of verification tools. Currently LDV tools are used to check Linux device drivers against several safety rules, each of them formally defines what is correct usage of a particular part of kernel core API. This project is intended to develop tools that can construct the kernel core model in the automatic way, which will allow to improve the drivers analysis quality for devices and also will give an opportunity to formalize a number of additional safety rules.