Static verification for memory safety of Linux kernel drivers

Memory errors in Linux kernel drivers are a kind of serious bugs that can lead to dangerous consequences but such errors are hard to detect. This article describes static verification that aims at finding all errors under certain assumptions. Static verification of industrial projects such as the Li...

Full description

Bibliographic Details

Published in:	Труды Института системного программирования РАН
Main Author:	A. A. Vasilyev
Format:	Article
Language:	English
Published:	Russian Academy of Sciences, Ivannikov Institute for System Programming 2019-02-01
Subjects:	анализ рекурсивных структур данных статическая верификация символические графы памяти модели памяти
Online Access:	https://ispranproceedings.elpub.ru/jour/article/view/1125