Configurable toolset for static verification of operating systems kernel modules
Configurable toolset for static verification of operating systems kernel modules
复制标题
用于操作系统内核模块静态验证的可配置工具集
DOI：
10.1134/s0361768815010065
复制
发表时间：
2015
影响因子：
0.7
通讯作者：
A. Khoroshilov
中科院分区：
文献类型：
--
作者：
I. Zakharov;M. Mandrykin;V. Mutilin;E. Novikov;A. Petrenko;A. Khoroshilov
操作系统 (OS) 内核是关系到可靠性和效率的关键软件。现代操作系统内核的质量已经足够高了。然而，内核模块的情况并非如此，例如设备驱动程序，由于各种原因，其质量水平明显较低。内核模块中最严重和最普遍的错误之一是违反了正确使用内核 API 的规则。人们可以在模块中找到所有此类违规行为，或者可以使用静态验证工具来证明其正确性，这些静态验证工具需要描述内核和模块相对于彼此的义务的合同规范。本文考虑了用于不同操作系统的内核模块静态验证的现有方法和工具集。提出了一种新的Linux内核模块静态验证方法。此方法允许在所有阶段配置验证过程。展示了它如何适用于检查其他操作系统的内核组件。描述了实现所提出的方法的用于静态验证 Linux 内核模块的可配置工具集的体系结构，并给出了其实际应用的结果。最后讨论了所提出方法的进一步发展方向。
An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of modern OS kernels is already high enough. However, this is not the case for kernel modules, like, for example, device drivers that, due to various reasons, have a significantly lower level of quality. One of the most critical and widespread bugs in kernel modules are violations of rules for correct usage of a kernel API. One can find all such violations in modules or can prove their correctness using static verification tools that need contract specifications describing obligations of a kernel and modules relative to each other. This paper considers present methods and toolsets for static verification of kernel modules for different OSs. A new method for static verification of Linux kernel modules is proposed. This method allows one to configure the verification process at all its stages. It is shown how it can be adapted for checking kernel components of other OSs. An architecture of a configurable toolset for static verification of Linux kernel modules that implements the proposed method is described, and results of its practical application are presented. Directions for further development of the proposed method are discussed in conclusion.