Check out the new USENIX Web site.

next up previous
Next: Proving the safety predicate Up: Certifying the Safety of Previous: Certifying the Safety of

Computing the safety predicate

To compute the safety predicate, we first generate a vector tex2html_wrap_inline1394 of predicates, one for each instruction as specified by the rules in wp. The notation tex2html_wrap_inline1396 denotes the predicate for the current instruction. Since the rules specify tex2html_wrap_inline1398 in terms of tex2html_wrap_inline1400 , the verification-condition tex2html_wrap_inline1402 for the beginning of the program can be computed by starting at the end of the program and working back towards the beginning.gif

The rules in wp are derived in a straightforward manner from the abstract machine specification of abs-mach; in fact, we imagine that experienced kernel and safe-ty policy designers would skip the abstract machine specification and give only the VC generator rules. The notation tex2html_wrap_inline1404 stands for the predicate obtained from P by substituting tex2html_wrap_inline1408 for tex2html_wrap_inline1410 .

After computing the vector tex2html_wrap_inline1412 , the safety predicate is computed simply by plugging the program tex2html_wrap_inline1414 , precondition tex2html_wrap_inline1416 , and postcondition tex2html_wrap_inline1418 into the following formula:

displaymath1420

The intuition behind a valid safety predicate is that for any initial state that satisfies the precondition tex2html_wrap_inline1422 , the code tex2html_wrap_inline1424 starting at the first instruction executes without failure and, if it terminates, the final state satisfies the postcondition tex2html_wrap_inline1426 .

  figure418
Figure 5: DEC Alpha assembly code for resource access. Initially register tex2html_wrap_inline1464 holds the address of the tag. The data is at the offset 8 from tex2html_wrap_inline1466 .  

For a concrete example of client code for the resource access service, consider the small program in ex-code. The overall effect of this program is to increment the data word if it is writable. We first compute tex2html_wrap_inline1468 for this program using the rules in wp; then we compute the safety predicate tex2html_wrap_inline1470 using the above formula with the precondition tex2html_wrap_inline1472 and the postcondition . After a few trivial simplifications, the resulting safety predicate is the following:

displaymath1474

Informally, the tex2html_wrap_inline1476 predicate says that for all values of register tex2html_wrap_inline1478 and states of memory tex2html_wrap_inline1480 satisfying the precondition tex2html_wrap_inline1482 , the memory locations tex2html_wrap_inline1484 and tex2html_wrap_inline1486 must be readable and if the tag (at address tex2html_wrap_inline1488 ) is non zero, the data (at address tex2html_wrap_inline1490 ) must be writable. All these conditions must be true for the code to be safe with respect to the resource access safety policy.



next up previous
Next: Proving the safety predicate Up: Certifying the Safety of Previous: Certifying the Safety of



Peter Lee
Tue Sep 17 15:37:44 EDT 1996