Development of Contract Specifications Method for Verification of Linux Kernel Modules.

Authors

E.M. Novikov.

Abstract

The PhD thesis is devoted to development of a contract specifications method for verification of Linux kernel modules. Nowadays there is not any contract specifications methods taking into account the development process of the Linux kernel and allowing checking modules against rules for correct usage of a kernel API with help of various software verification tools. Scientific advances of the PhD thesis are as follows: a new method for describing rules for correct usage of the kernel API as contract specifications; a new aspect-oriented extension for the C programming language with GCC compiler extensions; a new method for automated instrumenting Linux kernel modules source code that allows to use different software verification tools for checking it against rules specified by contract specifications; a new method of automated support of contract specifications correctness and compatibility under circumstances of Linux kernel API mutations. Using the suggested contract specifications method specifications for 34 rules for correct usage of the kernel API were developed and used on practice. The toolset implementing the suggested contract specifications method was integrated into a configurable toolset for static verification of Linux kernel modules. Verification of modules of several Linux kernel versions revealed 125 bugs acknowledged by the kernel developers.

Full text of the paper in pdf (in Russian)

Edition

Diss. Institute for System Programming of the Russian Academy of Sciences, 2013.

Research Group

Software Engineering

All publications during 2013

All publications