Defining a Safety Policy

The first order of business is to define precisely what constitutes safe code behavior. We do this by specifying a safety policy in three parts:

1. A Floyd-style verification-condition generator (also referred to as the VC generator) [6], which is a procedure that computes a predicate in first-order logic based on the code to be certified. We will refer to this predicate as the safety predicate.

2. A set of axioms that can be used to validate the safety predicate.

3. The precondition, which is essentially a ``calling convention'' that defines how the code consumer will invoke the binaries.

It is the job of the designer of the code consumer (e.g., the operating system designer) to define the safety policy. In practice, several different safety policies might be used, each one tailored to the needs of specific tasks or services.

We obtain the VC generator by first specifying an abstract machine (also called the operational semantics), that simulates the execution of safe programs. The abstract machine is not strictly required but it simplifies the design of the safety policy and provides a basis for proving the soundness of the whole approach.

In order to make all of this more concrete, we will now present an example of an abstract machine that specifies a general form of memory safety for the DEC Alpha processor, and then show how the safety policy of a simple resource access service can be defined by a precondition. The VC generator and axioms will then be given in the next subsection.