Linux Driver Verification

• Main Authors: D. Beyer, A. K. Petrenko
• Format: Article
• Language: English
• Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
• Series: Труды Института системного программирования РАН
• Subjects: ядро операционной системы; linux; инструменты верификции; анализ программ; верификация моделей; анализ указателей; анализ структур данных; свойства безопасности; ограничиваемая проверка моделей; символьная верификация; анализ с явными значениями; условная верификация моделей; анализ завершимости; верификация параллельных программ; сравнение методов верификации
• Online Access: https://ispranproceedings.elpub.ru/jour/article/view/992

Linux driver verification is a large application area for software verification methods, in particular, for functional, safety, and security verification. Linux driver software is industrial production code — IT infrastructures rely on its stability, and thus, there are strong requirements for correctness and reliability. Linux driver software is complex, low-level systems code, and its characteristics make it necessary to bring to bear techniques from program analysis, SMT solvers, model checking, and other areas of software verification. These areas have recently made a significant progress in terms of precision and performance, and the complex task of verifying Linux driver software can be successful if the conceptual state-of-the-art becomes available in tool implementations.The paper is based on experience of the research groups led by authors in verification of industrial software. It is important to develop verification tools that are efficient and effective enough to successfully check software components that are as complex as device drivers. In this area verifiers/researchers and Linux society find mutual benefits in cooperation because: for the society it is important to get such crucial software verified; for the verification community it is important to get realistic verification tasks in order to tune and further develop the technology. The paper provides an overview of the state-of-the-art and pointed out research directions in which further progress is essential. In particularly the paper considers most promising verification techniques and tools, including predicate abstraction, counter example generation, explicit-state verification, termination and concurrency analysis. One of main topic of Linux driver verification research is combination of verification techniques.