[E-Lang] Authority -- what is its dual?

[Jonathan S. Shapiro]

> >Not that it made a practical difference, but i could think "3+4" as
> >operation on a memory object: 1) store 3  2) add 4.
>
> It is not the business of the memory
> object to know whether the process thinks of the word read or stored as a
> number or as something else.

Agreed.

> Also, in neither system, nor in any other
> capability system that I've ever heard of, does one require a capability
to
> access one's own ALU.  So, I think we can say that the universal
capability
> approach is to treat internal calculation as no one's business, and,
except
> for resources, not to have it require any capabilities that may be denied.

I do not agree.

>From a practical perspective, I do not see a problem with your conclusion
about internal computation, but at least in EROS your characterization about
authority to compute is incorrect.

In EROS, the activation structure actually contains a process capability to
the process it occupies. Strictly speaking, this should be something weaker
than a process capability, but it is never exposed outside the kernel, and I
decided not to introduce a new capability type purely for internal use.

The specification of the abstract EROS machine is exceptionally careful to
account for the execution of normal user-mode (including ALU) instructions
as capability authorized. In EROS, every user-mode instruction can be
simulated by an indivisible sequence of operations on the process capability
held by the activation. The inputs of the ALU computation are the
capabilities that contain the register state of the process. The outputs are
the capabilities that contain the revised register state.

We are getting down to a level of precision at this point that probably only
matters when the time comes for formal analysis, but it actually *does*
matter there. The model used in the confinement verification that Sam and I
did would not be a sufficiently faithful model if we could not account for
the execution of instructions within the terms of the model.


Jonathan