Trustworthy Systems

Automatic verification of active device drivers

Authors

Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu

NICTA

Imperial College London

University of Sydney

Abstract

We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our methodology supports drivers written in C and can be implemented in any existing OS. Our Linux- based evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.

BibTeX Entry

  @article{Amani_CDLORZ_14,
    author           = {Amani, Sidney and Chubb, Peter and Donaldson, Alastair and Legg, Alexander and Ong, Keng Chai and
                        Ryzhyk, Leonid and Zhu, Yanjin},
    journal          = {ACM Operating Systems Review},
    keywords         = {dingo, device drivers, verification},
    month            = may,
    number           = {1},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8142.pdf},
    title            = {Automatic Verification of Active Device Drivers},
    volume           = {48},
    year             = {2014}
  }

Download