Here are some ideas about a program, the ‘sceptic’, that tries to derive limits to what some other given program, the ‘guest’ will do, all to the ultimate end that the guest will not perform some class of anti social acts against which we wish to be protected. The acts we study here are storing in locations ‘belonging’ to other system components, or reading data in its address space to which it is unauthorized. Which data is authorized to a program is not a static property of a program, but varies with how it is ‘called’. A program dynamically acquires the right to store in a location when that location is passed to the program as a pointer with write access.

By a ‘program’ we mean here bits stored in an address space that are meant to be obeyed by a CPU as instructions. That the program is not modified might be a result of the derivation, or might be ensured by exogenous considerations. We do not assume that the program is the only agent that modifies storage accessible to the program.

While for some purposes it will be unnecessary for the sceptic to produce formal proof, the ideas that I have in mind allow for that to be done efficiently. Such a proof would be inductive in nature.

As the sceptic runs it accumulates hypotheses about the program. I now see to sorts of hypotheses:

For the useful guest programs that I have in mind the sceptic will need a theory of data types for the guest program. This theory might be deduced by the sceptic, or some nefarious scheme such as instrumenting a compiler, or asking someone who understands the program.

The hypotheses are a collection of assertions in a tree structure. This is important for there will be much structural sharing among these propositional fragments.

The goal of the sceptic is to find an ultimate induction hypothesis which is verified as follows: There will be a set of PC values, pcs, which include all targets of branches. There will be a type state claim in the hypotheses of the form (PC = n → …) where the ellipses are most or all the assertions of the conventional RAM plan. Parts of the RAM plan may not be asserted for particular PC values for just that code that must temporarily violate the data structure in order to change what it represents.

Starting from any point in pcs the sceptic follows the flow mainly evolving the type state in accordance with the guest program’s instructions. There will be specialized assertions about 32 bit integers of the form [A<x<B] which mean that some named register holds a value between stated values A and B. An instruction that adds 4 to that register easily modifies that assertion to [A+4<x<B+4].

When this interpretation comes to a point in the pcs the recorded type state at that point is considered. If the later state implies the current state we are done for now with the current ‘basic block’. Otherwise we must liberalize the recorded type state at the target whereupon we must put that PC value into the list to be reconsidered.

Sometimes the sceptic will extrapolate and tentatively over liberalize a type state in order to accommodate situations where some register values are not relevant to security.

nexus