Static verification of operating system monolithic kernels

Abstract

The most of modern widely used operating systems have monolithic kernels since this architecture aims at reaching maximum performance. Usually monolithic kernels without various extensions like device drivers consist of several million lines of code in the programming language C/C++ and in the assembly language. With time, their source code evolves quite intensively: a new functionality is supported, various operations are optimized, bugs are fixed. The high practical value of operating system monolithic kernels defines strict requirements for their functionality, security, reliability and performance. Approaches for software quality assurance which are currently used in practice help to identify and to fix quite a number of bugs, but none of them allows to detect all possible bugs of kinds sought for. This article shows that different approaches to static verification, which are aimed at solving this task, have significant restrictions if applied to monolithic kernels as a whole, primarily due to a large size and complexity of source code that is constantly evolving. As a first step towards static verification of operating system monolithic kernels a method is proposed for decomposition of kernels into subsystems.

Keywords

• операционная система
• монолитное ядро
• микроядро
• качество программной системы
• статическая верификация
• формальная спецификация
• декомпозиция программной системы