/ talks

Auditors An Extensible, Dynamic Code Verification Mechanism

New: Auditors in Joe-E

• Powerpoint

Old Paper

• Auditors

Old Talk

• html
• OpenOffice

Abstract

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.