Applying SMT-Based Verification to Device Drivers (Powering the Static Driver Verifier using Corral)

Akash Lal and Shaz Qadeer

Abstract

he application of software-verification technology towards building

realistic bug-finding tools requires working through several

precision-scalability tradeoffs. For instance, a critical aspect while

dealing with C programs is to formally define the treatment of

pointers and the heap (usually termed as the “memory

model”). A machine-level modeling is often intractable, whereas one

that leverages high-level information (such as types) can be

inaccurate. Another tradeoff is modeling integer arithmetic. Ideally,

all arithmetic should be performed over bitvector representations

(like what happens in the hardware), whereas the current practice in

most tools is to use mathematical integers for scalability. A third

tradeoff, in the context of bounded program exploration, is to choose

a bound that ensures enough coverage without overwhelming the

analysis.

This paper works through these three tradeoffs when we applied Corral,

an SMT-based verifier, inside Microsoft's Static Driver Verifier

(SDV). Our decisions were guided by experimentation on a large set of

drivers; the total verification time exceeded well over a month. We

justify that each of our decisions were crucial in getting value out

of Corral and led to Corral being accepted as the engine that powers

SDV in the Windows 8.1 release, replacing the SLAM engine that had

been used inside SDV for the past decade.

Details

Publication typeInproceedings
Published inFoundations of Software Engineering (FSE)
> Publications > Applying SMT-Based Verification to Device Drivers (Powering the Static Driver Verifier using Corral)