[e-lang] Side Channels (was: E-on-Common-Lisp now available)

[David Wagner]

Mark Miller wrote:
>> David Wagner wrote:
>>> Allocate two identical instances of a DeepFrozen type; call them D1, D2.
>>> Then for all environments Env,
>>>   Env[Alice[D1], Bob[D2]].run()
>>>     is indistinguishable from
>>>       Env[Alice[D1], Bob[D1]].run()
>>> Is DeepFrozen the right concept here?
>
>DeepFrozen implies transitively immutable. The right terms is 
>Selfless.  [...]  DeepFrozen by itself is not adequate, as 
>DeepFrozen objects can be Selfish -- they can carry an EQ identity, and so be 
>distinguished by E's ==.
>
>Objects in E are either Selfish or Selfless. If D1 and D2 are both Selfless 
>and D1 == D2, then regarding overt computation (and therefore authority but 
>not side channels), the above indistinguishability hold.

I'm still trying to figure out why the indistinguishability doesn't hold
for side channels.  But let me come back to that.

As for your comment that DeepFrozen isn't good enough: Ah!  You're right.
I see what you mean about the need for Selfless; I had forgotten about ==.
Great catch.  Thanks.  I'm learning a lot.

Now that I re-read the auditors paper, I'm struck by the impression that
Selfless, as defined in the auditors paper, seems unnecessarily strong.
In particular, I'm having trouble justifying the OpenState and OpenSource
requirements as they are stated.

Let me try an alternative way of thinking about it, and maybe you can
tell me if I'm missing anything further?  Suppose we have a Java class C.
Call C "JustBits" if:
  (a) C is immutable, i.e., all method arguments and fields are final;
  (b) C is transitively JustBits, i.e., all fields are JustBits;
  (c) No one is permitted to call == on any instance of C; this is
      somehow prevented or forbidden statically or at runtime.
      (Alternatively, it might be sufficient if calls to == on JustBits
      objects were translated into calls to equals().);  and,
  (d) C's methods are "pure": every method is deterministic, and its
      return value depends only on its arguments and fields, but not on
      any source of non-determinism or on the object's creation identity.
      A method is allowed to allocate new objects and return them, but
      note that by (a) it cannot store them (unless this method is a
      constructor, and the newly allocated object is JustBits).
Instances of a JustBits class are JustBits.  Also, interned strings,
scalars, and null are "JustBits".

Instead of calling == on JustBits objects, you should call equals().
Note that since equals() and hashCode() must be "pure", these methods
do not divulge creation identity; two objects with the same value compare
equal.

Since the fields of a JustBits object depend only on the arguments to the
constructor, and since all methods (including constructors) are "pure",
the state of the object can be re-derived if you know the arguments to
the constructor.  This is my replacement for the OpenState requirement
found in the auditors paper.

As for the OpenSource requirement, I assume that the source code to the
program is known to the attacker.

My intuition is that a JustBits object is "just bits".  If I get handed a
JustBits object O, and I know the constructor arguments used to create O,
then I can create my own instance O' which has the same state as O, and
thus is indistinguishable from O.  Likewise, methods on a JustBits object
are just convenience code ("sugar").  Instead of calling a method on O,
I could have just inlined the code of that method myself.  So having a
reference to O gives me nothing more than knowledge of the state of O.
In particular, a reference to a JustBits object does not convey authority.

Is this JustBits notion a workable replacement Selfless, with respect
to the replacement conjecture that I listed?  (I care about Selfless-like
concepts primarily for their value for reasoning about code on a single
host.  I don't want to think about distributed systems just yet.)

Consider this pair of code segments:
  // C is any JustBits class; x is any value; f is any method
  C c1 = new C(x);
  C c2 = new C(x);
  f(c1, c2);   ... or ...    f(c1, c1);
Given the above code, I want to conjecture that f(c1, c2) is
indistinguishable from f(c1, c1), for all f.

What about for side channels?  Is there any reason that indistinguishability
with respect to non-overt computation would be violated?  I'm not seeing it.
For instance, I don't see how GC or memory allocation could enable a side
channel that would violate indistinguishability.  What am I overlooking?