Linux Driver Verification
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 corre...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
Series: | Труды Института системного программирования РАН |
Subjects: | |
Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/992 |
id |
doaj-748697acad7d4a37b5ed3b10dc73b528 |
---|---|
record_format |
Article |
spelling |
doaj-748697acad7d4a37b5ed3b10dc73b5282020-11-25T00:44:09Zeng Ivannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0123010.15514/ISPRAS-2012-23-23992Linux Driver VerificationD. Beyer0A. K. Petrenko1Университет Пассау, ГерманияИСП РАН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.https://ispranproceedings.elpub.ru/jour/article/view/992ядро операционной системыlinuxинструменты верификциианализ программверификация моделейанализ указателейанализ структур данныхсвойства безопасностиограничиваемая проверка моделейсимвольная верификацияанализ с явными значениямиусловная верификация моделейанализ завершимостиверификация параллельных программсравнение методов верификации |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
D. Beyer A. K. Petrenko |
spellingShingle |
D. Beyer A. K. Petrenko Linux Driver Verification Труды Института системного программирования РАН ядро операционной системы linux инструменты верификции анализ программ верификация моделей анализ указателей анализ структур данных свойства безопасности ограничиваемая проверка моделей символьная верификация анализ с явными значениями условная верификация моделей анализ завершимости верификация параллельных программ сравнение методов верификации |
author_facet |
D. Beyer A. K. Petrenko |
author_sort |
D. Beyer |
title |
Linux Driver Verification |
title_short |
Linux Driver Verification |
title_full |
Linux Driver Verification |
title_fullStr |
Linux Driver Verification |
title_full_unstemmed |
Linux Driver Verification |
title_sort |
linux driver verification |
publisher |
Ivannikov Institute for System Programming of the Russian Academy of Sciences |
series |
Труды Института системного программирования РАН |
issn |
2079-8156 2220-6426 |
publishDate |
2018-10-01 |
description |
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. |
topic |
ядро операционной системы linux инструменты верификции анализ программ верификация моделей анализ указателей анализ структур данных свойства безопасности ограничиваемая проверка моделей символьная верификация анализ с явными значениями условная верификация моделей анализ завершимости верификация параллельных программ сравнение методов верификации |
url |
https://ispranproceedings.elpub.ru/jour/article/view/992 |
work_keys_str_mv |
AT dbeyer linuxdriververification AT akpetrenko linuxdriververification |
_version_ |
1725276115241533440 |