This is yet another attempt to introduce an idea that goes back a long way. It is a form of partial program correctness. It is a property of a program that insures that the program will play by certain capability rules as if it were in fact constrained by a dynamic capability mechanism. It is a property rather like what Java’s byte code verifier may attest that its input has. It applies however to machine code. It is rather like “type safe”. I assert that a small fast program can do for a broad class of machine language programs, what the byte code verifier does for Java. Broader security claims can result from such compliance, however, than Java can claim, due to a few unfortunate properties of the Java language. Broader code patterns are also possible, patterns inexpressible in Java or any stack oriented language. There are scraps here and there about “tuncol” but I don’t like that name for lack of euphony.

Peter Deutsch did a limited form of this for the 940 in about 1968. His scheme also reported an upper bound on the time in which the vetted program would complete.

Correctness proofs for machine language programs require, I think, early lemmas that assert that data structures built and consulted by the program remain uncorrupted. Proofs and proof plans that I have understood prove some such anti-corruption lemma before proceeding to the original purpose of the program. Capability compliance verification presumes to stop after anti-corruption is verified for that allows incorporation of such code in a larger secure system. In a hierarchically composed software system, compliance of the whole stems, in part, from compliance of the parts. Just as a classic loader assembles collections of code into larger collections, so would our verifier. Indeed the verifier might come to be seen as an adjunct to the loader. Alternatively, the loader might obliviously load the compiler generated “proof” that the verifier will need after the code has been assigned to absolute addresses. This falls within the general scheme of Proof Carrying Code (PCC) but is less ambitious.

Useful programs generally have some logic to their data. That logic is captured partly by data declarations in programs higher level languages with static types. With dynamically typed languages or languages with latent types, capability safety is imposed by the interpreter. Java uses both techniques.

The system that I seek will probably benefit from starting with information derived from static type declarations but that will not suffice.

If program logic depends on a bilateral linked list then there will probably be at least a few instructions in the program during which the list is not intact. To cope with this from a predicate calculus approach would seem to require that the bilaterality assertion be conditioned on the program counter value. I think we cannot avoid this hair but that does not mean that we must necessarily produce such predicate calculus expressions to succeed, but I suspect that our program logic will necessarily be able to produce such expressions with little extra work.

A common idea is that a complex heuristic program find a safety proof and present it to a simple proof checker. This is a good idea, I think, in case of complex proof finders, or high paranoia. I don’t know a better language in which to format a proof than the predicate calculus. I have not yet concluded, however, that complex heuristic proof finders are needed.

One sort of desirable property to verify would be that for some specific constant machine language program loaded perhaps at a specific address, with a specified entry point, that if control were given to the program at that entry then that program would store only within a predetermined range of addresses and within some specified time control would be passed back to an address that was one of the input parameters. Such a result would be near the least ambitious result. A time limit is always nice not always strictly necessary.

A more typical challenge would presume as a precondition that upon entry some data located by one of the register values upon entry, designated data conforming to some provided plan. Typically it would be necessary to verify that the data conformed to the same or a different plan upon completion.

See Princeton’s intro to Proof-Carrying Code. My further notes are Ram Plan and Proof notes.