At 10:57 PM 10/25/99 , Ka-Ping Yee wrote:
>[+] I like the flexibility that we'd be getting out of guarded return values
>and guarded slots. (This sounds like the "auditor" concept you described a
>while ago, MarkM -- or are auditors a different thing?)
[#] Auditors are different but related.
The following is speculative, as auditors aren't implemented yet, and unfortunately probably won't be for a while.
The second PointMaker example of http://www.erights.org/elang/same-ref.html section "Selfish and Selfless Objects" shows both SlotGuards (": final") and an auditor (":: selfless", which should now be ":: PassByCopy"). An auditor must be defined at top level since it is asked to audit after expansion and and before evaluation of the top level expression it appears in. The auditor is given the parseTree of the definition it is asked to audit, as well as the parse tree for the definitions (including guards) of all variables that the first definition uses freely. (Actually, it must also be given the definitions of the variables used freely by the guards for these previous variables, etc, transitively.)
In any case, and auditor either approves or disapproves. It does not transform the tree, so you can have multiple auditors auditing the same tree without worrying about order of transformation. If any auditor in a tree disapproves of the subtree it is asked to audit, then the code is statically rejected prior to any evaluation, just like a conventional system statically rejects code that fails a static type-safety audit.
By some magic protocol that isn't worked out yet, but is related to
sealer/unsealer rights amplification
http://www.erights.org/elib/capability/ode/ode-capabilities.html#rights-amp
and/or to KeyKOS's branding rights amplification, the parse trees are
specially marked, so that their instances are effectively specially marked,
so that the same auditor used as a ValueGuard or a SlotGuard can verify that
a runtime value is an instance of a parseTree that it approved. Concretely,
having audited that the above "point" is "PassByCopy", the following
definition would succeed:
? define c : PassByCopy := PointMaker new(3, 5)
The auditors I expect to be important are:
Marking an object as PassByCopy also causes the comm system to pass it by copy rather than by proxy. This last isn't additional magic, as a hypothetical unprivileged comm system would, by the above explanation, have enough information to do so as well.
Although I'm not expecting to, one could define separate auditors for each of the three conditions above.
"stable" is really "transitively immutable", which is to say, transitively non-authority granting. Everything defined at top-level in a *.emaker file must be stable, so that *.emaker files can import: each other by name with no capability controls. This is the E analog of the Original-E rule that E-safe Java classes could not have native methods, could only import classes known to be E-safe, and that all their static state had to be transitively immutable. Rees's recent paper about Scheme security imposes a logically identical constraint. For syntactic convenience, as top level, all undeclared variable definitions are provided with the definition ": (final(stable))", and all top-level behavior definitions are provided with the auditor ":: stable".
Using Norm's terminology http://www.mediacity.com/~norm/CapTheory/term.html , our "stable" provides both Norm's "capability-confinement" and his "capability-isolation". However, it doesn't provide either bit-confinement or bit-isolation. Without bit-isolation, capability confinement isn't very meaningful because a confined Bob http://www.erights.org/elib/capability/confinement.html can always take instructions from Mallet (bits) for how to use a capability he cannot leak to Mallet. This is the proxying attack ( http://www.ietf.org/rfc/rfc2693.txt section 4.1.4 and http://www.erights.org/elib/capability/conspire.html ). Symmetrically, without bit confinement, we effectively don't have capability isolation, since a capability-isolated Bob can send instruction to Mallet for the use of a capability Mallet cannot pass to Bob.
To confine bits, one would have to completely plug wall banging attacks. E doesn't even try. On some problems, it's better to just give up. Alternatively, we can easily bit-isolate Bob by ensuring that he cannot be listening to anyone's wall banging. It Bob is deterministic, then he's deterministically replayable. If he's deterministically replayable, then we have accounted for all his external causal inputs. If we know about all his possible causal inputs, and we believe Mallet isn't overtly writing them, then we know Bob cannot listen to Mallet.
With bit-isolation but not bit-confinement, in addition to stability, we effectively have capability confinement but not capability isolation. Therefore I think "confined" is a fine name for this auditor.
Only throwable things can be thrown. An attempt to throw an unthrowable thing instead throws a throwable complaint to this effect. Throwables must be stable so we don't need to worry about the exception-exit control flow path in worrying about leakage of authority. Since problem reports are often our best early diagnostic tool for spotting bugs, PassByCopy ensures that we transmit a problem report over the network, rather than just a proxy to one.
Of course, all Java Throwable that can be thrown from E will be hand-audited to ensure that they have these properties from the point of view of E computation.
Whew!
Cheers,
--MarkM