Configurable Toolset for Static Verification of Operating Systems Kernel Modules
| Autor: | I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, A. V. Khoroshilov |
|---|---|
| Rok vydání: | 2014 |
| Předmět: |
статическая верификация
модель окружения General Earth and Planetary Sciences контрактная спецификация lcsh:Electronic computers. Computer science качество программной системы ядро операционной системы спецификация правила корректного использования программного интерфейса lcsh:QA75.5-76.95 модуль ядра General Environmental Science |
| Zdroj: | Труды Института системного программирования РАН, Vol 26, Iss 2, Pp 5-42 (2018) |
| ISSN: | 2220-6426 2079-8156 |
| DOI: | 10.15514/ispras-2014-26(2)-1 |
| Popis: | An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of a modern OSs kernel is high enough. Another situation is with kernel modules, e.g. device drivers, which 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 of correct usage of a kernel API. One can identify all such the violations in modules or prove their correctness with help of static verification tools which needs contract specifications describing formally obligations of a kernel and modules with respect to each other. The paper considers existing methods and toolsets for static verification of kernel modules of different OSs. It suggests a new method for static verification of Linux kernel modules that allows to configure checking at each of its stages. The paper shows how this method can be adapted for checking kernel components of other OSs. It describes an architecture of a configurable toolset for static verification of Linux kernel modules, which implements the proposed method, and demonstrates results of its practical application. Directions of further development are considered in conclusion |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|