[e-lang] LockBox and static typing (was: Newbie Joe-E questions)

[Toby Murray]

On Mon, 2008-10-27 at 21:55 -0700, David Wagner wrote:
> A Token is an object that
> exists solely for its unique object identity.  If you do
>     Token t = new Token();
>     Token u = new Token();
> then you are guaranteed that t!=u, and in particular no two Token
> objects will have the same object identity.  There are some cases
> where it's useful to have a bunch of "key" objects that exist solely
> for their object identity (e.g., when building sealer/unsealers), and
> then the idiomatic way to implement that in Joe-E is to use Tokens.
> The recommended Joe-E idiom is that you normally shouldn't use object
> identity (the "address" of an object) as a way to escalate privileges;
> in those cases where you do want to do that, use a Token, not any
> old object.  e.g.,
>     public class Lockbox {
>         private final Token key;
>         private final Object contents;
>         public Lockbox(Token k, Object o) {
>             key = k; contents = o;
>         }
>         public Object unlock(Token k) {
>             if (k == key)
>                 return contents;
>             else
>                 throw new SecurityException("wrong key");
>         }
>     }
> Here I can create a Lockbox using a new Token t, then hand Alice
> the Lockbox and hand Bob the Token; now Alice and Bob can only retrieve
> the contents of the Lockbox if they both cooperate.

In E, this implementation would be vulnerable to malicious (supposed)
LockedBoxes stealing Tokens. I'm wondering, does the Java static type
system prevent this sort of problem?

To expand, suppose Alice creates a LockedBox l using Token t. She hands
t to Bob. Bob is subsequently handed what he thinks is l but is really
l' -- an Object whose unlock() method simply keeps a copy of whatever
token it was passed, thereby accumulating keys to LockedBoxes. When Bob
tries to unlock l', he inadvertently passes t (a powerful capability,
when used with l) to some (possibly malicious, certainly untrusted)
thirdparty.

However, to what extent does the static typing in Java prevent this from
happening? Bob is expecting a LockedBox; does the type system guarantee
that if an object is assigned to a field of this type, then its unlock
method behaves as Bob would expect (in that it won't steal his Token)?

Cheers

Toby