Automatic Verification of Message-Based Device Drivers
Operating Systems
2012-11-28 v1 Software Engineering
Abstract
We develop a practical solution to the problem of automatic verification of the interface between device drivers and the OS. Our solution relies on a combination of improved driver architecture and verification tools. It supports drivers written in C and can be implemented in any existing OS, which sets it apart from previous proposals for verification-friendly drivers. Our Linux-based evaluation shows that this methodology amplifies the power of existing verification tools in detecting driver bugs, making it possible to verify properties beyond the reach of traditional techniques.
Cite
@article{arxiv.1211.6185,
title = {Automatic Verification of Message-Based Device Drivers},
author = {Sidney Amani and Peter Chubb and Alastair F. Donaldson and Alexander Legg and Leonid Ryzhyk and Yanjin Zhu},
journal= {arXiv preprint arXiv:1211.6185},
year = {2012}
}
Comments
In Proceedings SSV 2012, arXiv:1211.5873