[e-lang] LockBox and static typing

[David-Sarah Hopwood]

Toby Murray wrote:
> 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)
> [Lockboxes] stealing Tokens.

Note that analogous security abstractions in the real world are subject
to similar attacks. For example, if I put my credit card in a fake ATM
or a fake PIN Entry Device, then that device can steal my credit card
details. So one might hope that users of this kind of abstraction are
aware of that class of attacks, and do not automatically assume that an
arbitrary alleged-Lockbox cannot steal the token.

[...]
> 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)?

No, because Lockbox is not a final class. If it were a final class, and
if its code had been security reviewed, then a client of an object of
type Lockbox (in the correct package) could depend on the properties
established by that review.

-- 
David-Sarah Hopwood