[e-lang] Terminology for Joe-E's static auditors

[Adrian Mettler]

Last friday at the Joe-E meeting, the set of verifiable properties 
(corresponding to E auditors) and the names for them were discussed.  We 
(David, Mark, Marc, Tyler, Nikita Borisov (visiting from UIUC) and I) 
were able to reach consensus on the following set of names and 
definitions that we considered useful for Joe-E.  Mark suggested that 
this list be shared with other E projects in the interest of helping to 
standardize definitions and terminology.

Token:

In Java, all object types have unforgeable identity and thus could 
potentially be used as an unforgeable token for authority amplification 
(e.g. sealer-unsealer pattern).  However, if we know which types are 
actually being used for this purpose, we can make analyses that track 
where such objects are passed and thus reason more acurrately about the 
availability of capabilities conditionally granted upon presentation of 
a token.  The empty class Token is defined; Joe-E programs should use 
this class (or subclasses) for objects used for their object identity.

Selfless:

A class is selfless if any object of that class is indistinguishable 
from a "shallow clone" of itself, i.e. another object of the same class 
with all its fields set to the same values as the original class.  For a 
class C, this requires that:
1. All fields are final (can't be written once constructed)
2. The object identity of elements of the class is not visible.  This
    can be satisfied by one of:
    a. C's superclass is selfless
    b. C does not extend token, C overrides hashCode() and equals(),
       and C doesn't call super.hashCode() or super.equals()

The ability to mark a class as selfless isn't particularly useful by 
itself, but it is a weaker form of PassByCopy/Record whose verifier is 
easier to implement.

Immutable:

(Formerly called DeepFrozen.)  An immutable object cannot be used for 
communicating information and cannot be mutated.  Any methods of an 
immutable class that take only immutable arguments will be deterministic 
and "purely" functional without observable side effects.  This is a 
useful property for protecting against time-of-check-to-time-of-use 
attacks in which an attacker could take advantage of mutability of an 
object (or access to nondeterminism) by having the code that validates 
an action see one view of an object while the code that performs the 
action sees another (invalid) view of the object.

   To verify that a class is Immutable:
1. All fields final.
2. Types of all fields are Immutable.

The name "immutable" was chosen as it is a term that programmers are 
likely to know and it accurately describes the properties of an 
immutable object.  Other suggestions included DeepFrozen (more than one 
word), Final (accurate but would cause confusion with the overloading of 
the term "final class" to refer to a class that isn't subclassable), 
FieldsFinal (doesn't capture restriction on field types), Deterministic 
or Functional
(counterintuitive to be based on runtime behavior of methods, when 
restrictions are placed on fields)

Powerless:

(Formerly called Incapable.)  A powerless object is both immutable and 
does not contain any tokens.  Therefore, it does not convey any 
authority that Joe-E can reason about; as far as our analyses are 
concerned it is harmless to pass a Powerless object anywhere.  (This 
abstraction does not in fact capture everything that one might worry 
about; for example, we have no way of reasoning about what information 
might be sensitive based just on its type).  Every powerless object is 
also an immutable object, and thus inherit the security properties of 
immutable objects.  In addition, a powerless object satisfies the 
invariant that a "deep clone" of a powerless object (i.e. a copy in 
which every element is replaced by a distinct one with the same field 
values) is indistinguishable from the original object.  The checks 
performed to verify that a class C is Powerless:
1. class is Selfless (implies that all fields are final)
2. all field types are Powerless

Powerless extends Selfless and Immutable.

Record:

(Reserved for the future; not scheduled for implementation in first cut 
version.  Intended to be equivalent to E's PassByCopy)  A Record object 
is selfless and also transparent.  One can actually construct a 
(shallow) copy of such an object that is indistinguishable from the 
original.  Currently proposed (not-finalized) requirements:
1. class is selfless
2. all fields are public
3. a trivial constructor is provided (one that takes values for the 
fields and assigns them to the fields)

The name is based on the resemblance of such a class to a record in a 
functional programming language like ML -- essentially a tuple with 
named fields and subtyping based on which fields are present.  Another 
suggested name was struct (after structs in C), but was not chosen 
because structs are mutable.  If for some reason, we wanted to add the 
concept of a read-write transparent object, it might be an appropriate 
term.  A Record can be serialized and deserialized by an unprivileged 
serializer.

The name PassByCopy was considered too long and seemed to emphasize one 
particular property of a Record object.

Data:

(Reserved for the future; not scheduled for implementation in first cut 
version.  Intended to be equivalent to E's DeepPassByCopy)
A Data object is Powerless and also transparent.  One can construct a 
deep copy of a Data object that is indistinguishable from the original:
in this way a Data object can be worth no more than the information it 
contains.  Currently proposed (not-finalized) requirements:
1. class is powerless
2. meets requirements for a record

The name DeepPassByCopy was considered too long and seemed to emphasize 
one particular property of a Data object.

--Adrian