Ivannikov Institute for System Programming of the RAS


Configurable toolset for static verification of operating systems kernel modules.

Authors

I.S. Zakharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, A.V. Khoroshilov.

Abstract

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.

Full text of the paper in pdf

Keywords

operating system kernel; kernel module; software quality; static verification; contract specification; environment model; specification of rule for correct usage of API

Edition

Programming and Computer Software, January 2015, Volume 41, Issue 1, pp 49-64.

DOI: 10.1134/S0361768815010065

Research Group

Software Engineering

All publications during 2015 All publications