Symbolic Execution of Virtual Devices

Device drivers are a principal source of failures in computer systems. Therefore, improving driver reliability greatly improves overall system reliability. However, driver development largely has to wait until a first stable version of the device becomes available. This dependency often leaves not enough time for driver validation. Recently, virtual machines and virtual devices have found their way into early driver development and validation. Virtual devices enable driver development even before real devices become available and bring complete observability and trace ability that evade real devices. We present an approach to static analysis of virtual devices which is central to achieving observability and traceability. This approach exercises the device model of a virtual device by symbolic execution. Based on the result of symbolic execution, a concrete test case is generated for each path through the device model, which has been exercised. We have applied this approach to virtual devices of five network adapters. The results show that this approach is feasible, efficient, and useful.