/ elang / kernel

Auditors

Auditors: An Extensible, Dynamic Code Verification Mechanism by Ka-Ping Yee and Mark Miller is our paper on the auditor rationale and design.

An object expressions has an optional list of names, which must be bound in the outer scope to Auditors. These auditors check for properties of objects, like confinement, that can be statically determined by examination of the object expression the object instantiates. The auditor can then verify that instances of approved parse trees have these properties.

BNF:	["::" Noun ("," Noun)*]
XML DTD:	<!ELEMENT auditors (Noun*)>
Java:
Example:
in Kernel-E:
in XML:
in Java:

At load time, each of these auditors will be provided with the Kernel-E parse tree of the object expression and asked for its approval. The auditor demonstrates its approval by providing XXX. If any of these auditor disapprove of perform a non-local exit, the object expression is not loaded. If all the auditors approve, the object expression is loaded, and the association between the object expression and the XXXs provided by these auditors is remembered by the TCB. When an auditor is then asked to coerce an object (usually while serving as a ValueGuard or SlotGuard), the auditor may then determine whether the object is an instance of an object expression it has already approved. If so, it returns the object, since it knows the object must have whatever properties this auditor represents. Otherwise, it should throw an informative exception.

XXX show the auditing protocol: