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

[Mark S. Miller]

Mark Seaborn wrote:
>> > As I understand it, authority is defined as the ability to influence
>> > the world.  Sensory capabilities are then regarded as not conveying
>> > authority.  Information in general is also regarded as not conveying
>> > authority.

"Jonathan S. Shapiro" <shap@eros-os.org> writes:
>> This is incorrect. In the context of information systems, authority means
>> the ability by a subject to perform one or more operations on an object.
>> These operations can either change the state or *detect* the state of the
>> object. The first is what you seem to mean by "influence".

At 07:11 AM 10/19/2001 Friday, Mark Seaborn wrote:
>It seems that my different definition of authority has come from
>reading Marc Stiegler's `E in a Walnut'.  It says ``Only immutables
>that encapsulate no authority actually move across computational
>boundaries'' in the context of what gets passed by copy and by
>reference for remote method calls; I take this to imply that
>immutables don't convey authority.

Thanks for this line of questioning, it'll cause us to tighten up our 
precision a great deal.  As you'll see, MarcS and I have been sloppy here 
and there, and Jonathan is using words in somewhat different ways then we 
are, as explained on
http://www.eros-os.org/pipermail/e-lang/2001-October/005806.html .
I'll add that when Jonathan says "in the context of information systems" 
(which I missed before), I don't know what this qualifier is supposed to mean.

However, MarcS' statement is wrong too (note: I believe MarcS is simply 
quoting me).  But, before we confuse ourselves further, we need to 
distinguish between two forms of immutables: one-level immutables and 
transitive immutables.  These are both important concepts, and we need 
simple names for both.  It's not clear which should simply be called 
"immutable".  Our habit to date is to call one-level immutables "immutable", 
but I'll avoid that for now.


                Transitive Immutability == Authority Free


A transitive immutable is an object that cannot change, and in which all the 
objects reachable from that object cannot change.  Since causality is 
limited by reachability, a transitively immutable object also cannot cause 
change to anything other than its arguments.  

What about devices?  We think of devices as object references to the 
external world.  Since the world changes, and input can sense this change, 
and output can cause change, we magically deem devices to be mutable.  
Therefore no devices may be reachable from a transitive immutable.  (The 
time is considered part of the world, not part of computation, and the clock 
is an input device that can sense this part of the world.  Likewise with 
true non-determinism.)

But is even "3" really transitively immutable?  When asked to "+ 4", it
changes the program counter, and causes a "7" to be placed somewhere in 
memory.  Also, pages and cache lines may be faulted into various caches, and 
these changes persist even after "3 + 4" is done, in order to affect later 
computation.  Further, if a human is watching this through a utcb-level 
debugger, then the human, a part of the world, has been changed by seeing 
the computation continue.  And let's not forget the eavesdropping device in 
the ceiling picking up and reporting the electromagnetic radiation to the NSA.

For all these, E takes the same stance as all functional programming, and 
sweeps these issues under a definitional rug. Since E is trying to make 
security claims and they're not, this rug is potentially more dangerous for 
us, but so far I don't see any problems.

(This seems a good opportunity to explain a possible additional use to make 
of this rug: tracing (or logging).  If we think of a tracing channel as an 
output-only debugging channel that can only be read by using utcb-level 
debugging access, then this one device can be magically deemed transitively 
immutable with, as far as I can tell, no further loss of security.  This was 
the stance in Original-E regarding 
http://www.erights.org/elib/Tracing.html .  I've been thinking of adding 
such a "device" to E's universal scope, about which more in future email.)

So, finally, with all this said, I can now define what E means by 
"authority" to be anything that isn't transitively immutable.  Note that 
bits, even secret bits, are transitively immutable, and therefore, by E's 
definitions, convey no authority.  This suggest that perhaps a word other 
than "authority" is needed.  For now, I'll just use "transitively immutable".


                             One-Level Immutable


Naively, this seems simple to define: the object itself cannot change, but 
the objects reachable from the object may change.  Unfortunately, it's hard 
to get a handle on "the object itself" -- it would seem to depend on the 
level of abstraction of the observer.  Consider the ConstList: it may be 
implemented primitively (using a Java array or something), or it may be use 
a linked list or a tree inside or something.  However, all the state needed 
to *fully explain the external behavior* (modulo performance) of a ConstList 
is simply the sequence of list elements.  Given such an explanation we may 
then define "the object itself" to consist of this state plus code that 
would bring about the object's external behavior given this state.

There may be multiple ways to explain the external behavior of an object, so 
one-level immutable by itself is still slippery.  Fortunately, for 
user-defined objects, none of this slipperiness matters, as an automated 
process must decide simply and in a fail-safe manner.  Therefore, for 
user-defined objects, the obvious syntactic rule applies, which is usually 
good enough anyway.  The deeper semantic analysis is only done by us UTCB 
designers in order to classify the UTCB-provided data types, and for these, 
the UTCB designer can pick the reference explanation of interest.  I present 
this more complex explanation-relative definition above to account for both 
the manual classification of the UTCB datatypes and the automated 
classification of user-defined datatypes.  Also, we can imagine someday 
allowing user-defined datatypes with proof-carrying code to make use of the 
more flexible explanation-relative rule, in which case the proof will 
provide the reference explanation of interest.  In no case does any actually 
ambiguity remain about "state".


           External Reachability, Transparency, and Encapsulation


An object is 'transparent' if it's open-source and open-state.

An object is 'open-source' if it will reveal its source (Kernel-E parse 
tree or the fully qualified name of a standard primitive) in response to a 
standard query.  (E does not yet provide support for this.)

A part of an object's state is "externally reachable" if a client of the 
object can obtain it from the object by a query requiring no special 
privilege (undefined for the moment).

An object 'encapsulates' that state which is not externally reachable.

A part of an object's state is "obviously externally reachable" if a client 
of the object can obtain it from the object by an 'obvious query'.  The 
following definition of 'obvious query' is new and experimental:

All no-argument message name provided by the object's stable response to 
'getAllegedType()' are 'obvious queries'.

If an object stably says it 'respondsTo("size", 0)' and 'respondsTo("get", 
1), and if 'size()' returns an integer, then for all i in 0..!(size()), 
'get(i)' is an 'obvious query'.  (This still needs work.  Probably we should 
use 'iterate' instead.)

An object is 'open-state' if all its state is obviously externally reachable.

For state that is externally reachable but not obviously externally 
reachable, we neither say it is 'encapsulated' nor 'open'.  An object with 
such state is neither encapsulating nor transparent.


                            Auditable vs Audited Properties


(Note: auditors are not currently implemented)

Most of the properties above can be automatically checked for by auditing an 
object expression, at the price of making well defined errors of exclusion 
(which is both fail safe and understandable).  An example is the auditor for 
transitive immutability, which we've always planned to call "confined" for 
reasons explained in Stage #2 of 
http://www.erights.org/elib/capability/factory.html .  It would reject the 
following Point1 expression -- it would throw an exception rather than allow 
the expression to evaluate:

    def PointMaker(x, y) :any {
        def Point1 ::confined {
            ...
        }
    }

    def pt :confined := PointMaker(3, 5)

Even though Point1 is perfectly capable of evaluating to transitively 
immutable objects, such as 'pt' above were we to have gotten that far.  This 
is because auditors-as-auditors (the '::confined' syntax above) audit only 
code, not data.  Auditors are normally usable as guards as well. The 
':confined' guard on 'pt' guarantees that 'pt' may only hold transitively 
immutable objects.

The following Point2 expression auditably always makes only transitively 
immutable objects:

    def PointMaker(x :confined, y :confined) :any {
        def Point2 {
            ...
        }
    }

    def pt :confined := PointMaker(3, 5)

However, although Point2 is auditable, it does not declare that it should be 
audited.  Therefore, although it happens to only make transitively immutable 
objects, that's no one else's business.  Therefore, the ':confined' guard on 
'pt' still fails.  Auditor-as-guards normally check only that the specimen 
object is either:

1) An instance of an object expression approved by this very auditor.  The 
hook is the Miranda Method 'optMeta(brand)' 
http://www.erights.org/javadoc/org/erights/e/elib/prim/MirandaMethods.html#optMeta(java.lang.Object,%20org.erights.e.elib.sealing.Brand)

2) Or, an instance of a primitive that this auditor deems to have the 
property it guarantees.

So, finally, this works (or will, once we have auditors):

    def PointMaker(x :confined, y :confined) :any {
        def Point3 ::confined {
            ...
        }
    }

    def pt :confined := PointMaker(3, 5)

We may say that Point3 and its instances are 'manifestly confined' or 
'manifestly transparently immutable'.  Auditors-as-auditors ('::') cause 
properties to be manifest.  Auditors-as-guards (':') check for manifest 
properties.  When auditable property A implies auditable property B, then, 
should the auditors for these properties be designed together, they should 
be designed such that manifest property A implies manifest property B -- if 
Point is audited by ::A, its instance should also be acceptable to the :B 
guard.


                      The Real Point


So finally getting back to MarcS statement (quoting MarkM, and as quoted by 
Mark):

>It seems that my different definition of authority has come from
>reading Marc Stiegler's `E in a Walnut'.  It says ``Only immutables
>that encapsulate no authority actually move across computational
>boundaries'' in the context of what gets passed by copy and by
>reference for remote method calls; I take this to imply that
>immutables don't convey authority.

In order for an object to be passed by copy, it must be manifestly 
PassByCopy.  This implies that is manifestly Selfless, One-level immutable, 
and Transparent.  It does not imply transitive immutability, and so does not 
imply that it does not convey authority.  This is intuitive: If I may pass 
'purse' by proxy, then I should be able to pass the ConstList '[purse]' by 
copy, where the copy of the list arrives with a far rather than near pointer 
to the very same purse.  The list has clearly conveyed all the authority 
that 'purse' conveys.

The above "encapsulates no authority" should really be "encapsulates 
nothing".  Turn this into "obviously and manifestly encapsulates nothing" 
and we get manifestly transparent.  The reason for this is so malicious 
remote vats cannot violate the security implied by encapsulation, and we 
get to preserve the rest of our tarnished mantra from the Ode:

>Put another way, mistrust of a vat is equivalent to ignorance of the 
>internal relationships among the objects hosted by that vat. A malicious vat 
>hosting one set of objects can only cause external effects equivalent to a 
>correct vat hosting some different (maliciously coded) set of objects. This 
>is the main economy of the distributed capability model: we can, without 
>loss of generality, reason as if we are only suspicious of objects.

(Why tarnished?  Your earlier observation that a malicious vat can cause two 
remote occurrences of the same promise to resolve to different values.  Damn.)

Requiring Selflessness and one-level immutability have similar motivations.  
With these, and object is indistinguishable from a copy of the object, so 
the implementation should feel free to make copies as it wishes.  Of course, 
between vats this is a strange rationale, since the original is in one vat 
and the copy is in another, so the fact that a copy was made is quite 
apparent: we have a near rather than a far reference.  But it guarantees 
that some (to be said well) deeper level of semantics has not be corrupted 
by making and passing such copies.


                                   Imports


>[Walnut] says ``...it only imports those
>parts of the Java API that have been audited for capability security
>and found to convey no authority'' when talking about `import:',
>referring to APIs like java.lang.Math, and it then says explicitly
>that ``the Vector class conveys no authority''.

That is all correct.

>Do you regard immutable values (as well as read-only values that might
>be modified by someone else with write access) as carrying authority?

"read-only values that might be modified by someone else with write access" 
don't seem immutable at all.  They can change!

Regarding immutability, transitive immutables, given the careful weasel words 
above about devices, I regard as conveying no authority.  One level 
immutables, like '[purse]' clearly can.


>What do you consider to be an operation? -- are operations required to
>change or detect state?

'operation' is not part of my shtick, so I un-ask the question.


        Cheers,
        --MarkM