Automatic Verification of Message-Based Device Drivers

TL;DR

This paper presents a practical approach for automatically verifying device driver interfaces in operating systems, enhancing bug detection capabilities beyond traditional methods.

Contribution

It introduces a new driver architecture combined with verification tools that support C drivers and can be integrated into existing OSes, improving verification effectiveness.

Findings

Enhanced bug detection in device drivers

Supports C language drivers in Linux

Improves verification reach beyond traditional techniques

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.