Sidney Amani (NICTA and UNSW) |
Peter Chubb (NICTA and UNSW) |
Alastair F. Donaldson (Imperial College London) |
Alexander Legg (NICTA and UNSW) |
Leonid Ryzhyk (NICTA and UNSW) |
Yanjin Zhu (NICTA and UNSW) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.102.3 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |