 Auditors: An Extensible, Dynamic Code Verification Mechanism
started 12/28/2002; 2:50:46 PM - last post 1/2/2003; 11:32:51 AM
|
|
Ehud Lamm - Auditors: An Extensible, Dynamic Code Verification Mechanism 
12/28/2002; 2:50:46 PM (reads: 1032, responses: 2)
|
|
| Auditors: An Extensible, Dynamic Code Verification Mechanism |
|
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.
We discussed E and its capability-based security in the past. Auditors are an extension of this model.
Auditors can inspect the abstract syntax tree to ascertain a particular semantic property. In addition to that, access to auditors is controlled, and thus knowing that an auditor is being applied to an object gives us information about object identity.
Posted to general by Ehud Lamm on 12/28/02; 2:52:41 PM
|
|
|
|
Ehud Lamm - Re: Auditors: An Extensible, Dynamic Code Verification Mechanism
12/29/2002; 12:45:58 PM (reads: 549, responses: 0)
|
|
|
Proving properties of code is hard. This fact makes me prefer ideas like PCC and certifying compilers to things like Auditors. But I may well be missing something.
|
|
Darius Bacon - Re: Auditors: An Extensible, Dynamic Code Verification Mechanism
1/2/2003; 11:32:51 AM (reads: 479, responses: 0)
|
|
|
Interesting question. It should be possible to supply a PCC certificate to an auditor -- the ways that occur to me include passing an argument to the auditor's constructor or embedding the certificate as a constant in the audited subprogram, although it's been a while since I read up on auditors and I'm not sure how well those ideas would fly in practice.
When I mentioned this post to Mark Miller last night he pointed out that auditors and PCC are meant to solve different problems, and should be complements rather than competitors. I think I'd better reread Ping's paper.
|
|
|
|