Communications - July 2011

100%, and for Windows Driver Model (WDM) drivers, the figure is 97%.

Example. We illustrate the CEGAR process using the SLIC rule from Figure 1a and the example code fragment in Figure 1b. In the program, we have a single spinlock being initialized at line 4. The spinlock is acquired at line 8 and released at line 12. However, both calls KeAcquireSpinLock and KeReleaseSpinLock are guarded by the conditional (x > 0). Thus, tracking correlations between such conditionals is important for proving this property. Figures 3a and 3b show the Boolean program obtained by the first application of the abstract function to the code from Figures 1a and 1c, respectively.

Figure 3a is the Boolean program abstraction of the SLIC event handler code. Recall that the instrumentation step guarantees there is a unique error state. The function slic _ error at line 1 represents that state; that is, the function slic _ error is unreachable if and only if the program satisfies the SLIC rule. There is one Boolean variable named {state==Locked}; by convention, we name each Boolean variable with the predicate it stands for, enclosed in curly braces. In this case, the predicate comes from the guard in the SLIC rule (Figure 1a, line 8). Lines 5–8 and lines 10–13 of Figure 3a show the Boolean procedures corresponding to the SLIC event handlers SLIC _ KeAcquireSpinLock _ call and SLIC _ KeReleaseSpinLock _ call from Figure 1a.

Figure 3b is the Boolean program abstraction of the SLIC-instrumented C program from Figure 1c. Note the Boolean program has the same control flow as the C program, including procedure calls. However, the conditionals at lines 7 and 12 of the Boolean program are nondeterministic since the Boolean program does not have a predicate that refers to the value of variable x. Also note that the references to variables count, devicebuffer, and lo-calbuffer are elided in lines 10 and 11 (replaced by skip statements in the Boolean program) since the Boolean program does not have predicates that refer to these variables.

The abstraction in Figure 3b, though a valid abstraction of the instrumented C, is not strong enough to prove the program conforms to the SLIC rule. In particular, the reachability analysis of the Boolean program performed by the check function will find that slic _ error is reachable via the trace 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, which skips the call to SLIC _ KeAcquireSpinLock _ call at line 8 and performs the call to SLIC _ KeReleaseSpinLock _ call at line 13. Since the Boolean variable state==Lock is false, slic _ error will be called in line 11 of Figure 3a.

SLAM feeds this error trace to the
symexec function that executes it
symbolically over the instrumented C
program in Figure 1c and determines
the trace is not executable since the
branches in “if” conditions are cor-
related. In particular, the trace is not
executable because there does not ex-
ist a value for variable x such that (x
> 0) is false (skipping the body of the
first conditional) and such that (x > 0)
is true (entering the body of the sec-
ond conditional). That is, the formula
∃x.(x ≤ 0) (x > 0) is unsatisfiable. The
result of the refine function is to add
the predicate {x>0} to the Boolean
program to refine it. This addition
results in the Boolean program ab-
straction in Figure 3c, including the
Boolean variable {x>0}, in addition to
{state==Locked}.

Using these two Boolean variables, the abstraction in Figure 3c is strong enough to prove slic _ error is unreachable for all possible executions of the Boolean program, and hence SLAM proves this Boolean program satisfies the SLIC rule. Since the Boolean program is constructed to be an overapproximation of the C program in Figure 1c, the C program indeed satisfies the SLIC rule.

From SLAM to SDV SDV is a completely automatic tool (based on SLAM) device-driver developers can use at compile time. Requiring nothing more than the build script of the driver, the SDV tool runs fully automatically and checks a set of prepackaged API usage rules on the device driver. For every usage rule violated by the driver, SDV presents a possible execution trace through the driver that shows how the rule can be violated.

Figure 3. (a) Boolean program abstraction for locking and unlocking routines; (b) Boolean program: CEGAR iteration 1; (c) Boolean program: CEGAR iteration 2.