New: Auditors in Joe-E
We introduce auditors, a program annotation and verification scheme similar to type declarations, but more general in some ways: auditors can be dynamically generated and applied at run-time, and can inspect the source code of the annotated object. Auditors allow objects to make mandatory commitments about their behaviour (such as immutability, determinism, or lack of side effects), as contrasted with types, which constrain data but are only discretionary with respect to behaviour. The inspection facility is arbitrarily extensible since auditors can themselves be part of the program. In particular, we describe an implementation of auditors for E, a language platform for capability-secure distributed programming, and apply auditors to make E the first language capable of supporting secure confinement at the object level.
Unless stated otherwise, all text on this page which is either unattributed or by Mark S. Miller is hereby placed in the public domain.