[E-Lang] Auditing Protocol (was: Rights Amplification: The Next Layer Up)

[Mark S. Miller]

At 11:51 PM 9/5/00 , Dean Tribble wrote:
>At 05:30 PM 9/5/2000, Mark S. Miller wrote:
>>              match _ { meta getDefaultOptSealedFacet(self, brand) }
>
>This seems, um, inelegant...  :-)
>
>>This expression provides the default system-defined meta-level behavior
>>for those cases not overridden by the programmer.  This requires the TCB to
>>have prior knowledge of certain sealers, which is fine.  The object itself may
>>not have access to some of these sealers, such as for equality, in which
>>case it can only override requests with those brands to deny service.
>>getDefaultOptSealedFacet() itself will default to returning null.
>
>Why is this ever better than just returning null?  Or rather why is this not the default behavior when returning null?  My only speculation is that the meta-system would provide some access that the caller would otherwise be unable to achieve with respect to this object.  An alternative way to accomplish that is using a function in the TCB that is closely held by the appropriate meta subsystem.  For comm, let's call it getCommReplacement:  getCommReplacement exclusively holds the unsealer.  The Comm system invokes getCommReplacement with the original object.  getCommReplacement first sends the getOptMeta request with the brand, and if the result is not null, returns.  If the result is null, it returns whatever the "meta getDefaultOptSealedFacet(self, brand)" above would have returned.  That seems to cover all the issues, bogus clients can't screw it up, it's much simpler to implement the overrides, and it is probably easier to make efficient.

Your proposal may be the right thing.  But here's a motivating case that 
possibly argues in the other direction.

Auditing, where the auditors are unprivileged user-written code.  When the E 
virtual machine is asked to load a parse-tree for an audited object expression

     define foo :: Confined, Blue {
         to ...
         ...
     }

the virtual machine asks all the listed auditors to audit the object 
expression:

     Confined audit(e`define foo ...`)
     Blue audit(e`define foo ...`)

an auditor indicates its approval by returning the value of

     MetaAuditSealer seal([exprTree, myChopSealer])

which is a sealed box containing the pair of the parse-tree and the auditor's 
own sealer.  The auditor seals the box with MetaAuditSealer, confident that 
the MetaAuditUnsealer is held only within the TCB.  It needs to do this to 
be sure its own precious myChopSealer never escapes.

When the virtual machine compiles this parse tree into an internal script, 
this script object, a part of the TCB, encapsulates the various instance 
sealers gathered by the above process.  When an auditor is then asked to 
verify that an instance has the properties that this auditor audits for

     auditor coerce(specimen)

it does

         to coerce(specimen) :any {
             def optBox := specimen getOptMeta(myChopBrand)
             if (optBox == null) { throw(...) }
             myChopUnsealer unseal(optBox)
         }

The specimen itself never has access of the chop-sealers 
used to seal it, but these sealers must be stored on a per-script basis, and 
an instance whose script does contain such a sealer (by the above process) 
must be able to obtain a box containing itself as sealed by such a sealer.  
The key economy of this mechanism is that the auditor only needs to examine 
an expression in order verify all its instances.


To try this with your proposal, there would be a TCB provided service for 
use by unprivileged auditors called, let's say, GetOptVerified:

     GetOptVerified(specimen, chopBrand) :(nullOk(SealedBox))

We would then rewrite the verification function as

     define someAuditor {
         to coerce(specimen) :any {
             def optBox := specimen getOptMeta(myInstanceBrand)
             if (optBox == null) {
                 optBox := GetOptVerified(specimen, myInstanceBrand)
             }
             if (optBox == null) { throw(...) }
             myInstanceUnsealer unseal(optBox)
         }
         ...
     }

Ok, this is plausible.  Some issues:

Why have separate TCB provided services for the different reasons to 
getOptMeta(), such as your getCommReplacement and the above GetOptVerified?  
Why not have the TCB provide one widely available (but virtualizable) function,

     GetPrimOptMeta(specimen, brand :Brand) :(nullOk(SealedBox))

Then we can generalize our coerce code into generally useful function:

     define GetOptMeta(specimen, brand :Brand) :(nullOk(SealedBox)) {
         def optBox := specimen getOptMeta(brand)
         if (optBox == null) {
             GetPrimOptMeta(specimen, brand)
         } else {
             optBox
         }
     }

Better yet, we can have the TCB export only the above GetOptMeta function, 
rather than GetPrimOptMeta, giving back to the objects more control over how 
they react to such requests.

I think I like your direction as modified above better than my original.  
Reactions?


         Cheers,
         --MarkM