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.
1 slic_error() { assert(false); }
2
3 bool {state==Locked};
4
5 SLIC_KeAcquireSpinLock_call() {
6 if( {state==Locked}) slic_error();
7 else {state==Locked} := true;
8 }
9
10 SLIC_KeReleaseSpinLock_call() {
11 if( !{state==Locked}) slic_error();
12 else {state==Locked} := false;
13 }
14
1...
2...
3 {state==Locked} := false;
4 KeInitializeSpinLock();
5...
6...
7 if(*)
8 { SLIC_KeAcquireSpinLock_call();
9 KeAcquireSpinLock(); }
10 skip;
11 skip;
12 if(*)
13 { SLIC_KeReleaseSpinLock_Call();
14 KeReleaseSpinLock(); }
15...
16...
1 bool {x > 0};
2...
3 {state==Locked} := false;
4 KeInitializeSpinLock();
5...
6...
7 if({x>0})
8 { SLIC_KeAcquireSpinLock_call();
9 KeAcquireSpinLock(); }
10 skip;
11 skip;
12 if({x>0})
13 { SLIC_KeReleaseSpinLock_Call();
14 KeReleaseSpinLock(); }
15..
16...
(a)
(b)
(c)