Security Bug in Example Fixed

[Mark S. Miller]

At a recent party I couldn't resist temptation, and asked the host to bring 
up a web browser so I could show off the smart contract for a 
covered-call-option.  Fortunately, Michael Butler was one of the people I 
was showing it off to.  By asking some astute questions, he uncovered a 
security bug in the call-option that is exactly along the lines of E's 
rationale for having entry guards.

Indeed, most instances of the bug were addressed simply by adding 
SlotGuards to serve effectively as entry guards.  Notice the three
": integer" declarations absent in our original submission 
http://www.erights.org/elib/capability/ode/ode-submission.html , but now 
present in the current draft 
http://www.erights.org/elib/capability/ode/ode-bearer.html .  In the 
original code, the call-writer could cause the call-option to behave 
erratically, and in violation of the contractual terms we intended to write, 
by providing, for example, an exercise price that acts like an integer, but 
that acts like different integers at different times.  By constraining such 
incoming data via ": integer", we know the variable can only hold bona-fide 
integers, and we know that the call-writer's argument coerced to whatever
integer we have, but we don't know or care, and don't need to worry about, 
further properties of what the call-writer passed in.

Another instance of the same problem is the original moneyDest passed in by 
the call-writer.  Since the broker doesn't check that this is a valid 
implementation of the money-purse abstraction, the call-writer could pass in 
one that responds to "deposit" by performing the deposit to a real purse, 
and then throwing an exception, thereby getting the money the call-holder 
payed to exercise the option, but without giving up the stock the 
call-holder paid for.  Our solution to this makes the code more symmetrical: 
the broker passes in an empty escrowedMoney purse from an issuer the broker 
trusts, just as the broken has always passed in an escrowedStock purse.  
Since this code explicitly leaves aside issues of concurrency & 
distribution, it therefore leaves aside issues of partition or other forms 
of partial failure.  Therefore, our final change, the try/finally at the 
end, is sufficient to ensure that the money is transferred to the 
options-writer and the stock is transferred to the options holder.

I looked at all the other code in the paper, and none of the rest seems to 
have this problem.  In particular, the purse-money code already performs 
adequate input validation everywhere it might have been an issue.

Thanks Mike!


         Cheers,
         --MarkM