[E-Lang] Java 2 "Security" (was: Re: Welcome Chris Skalka and ScottSmith of Johns Hopkins)

Mark S. Miller markm@caplet.com
Fri, 19 Jan 2001 15:02:34 -0800

At 08:41 AM Friday 1/19/01, Christian Skalka wrote:
>[...] distinction
>between policy and principle is because ACL's plus stack inspection
>is not a model that can only be used in Java.  That is, it is possible
>to design a new language from the ground up, using ACL's and
>stack inspection [...] shed skin on the road to developing a really
>sound language, 

 From my point of view, I would love to see you develop such an experimental 
pure language.  Java is such a mishmash from a security perspective that I, 
as well, am not able to separate essence from accident, and reason about 
what ACLs + stack introspection would be like in the absence of all the 
other junk.

Claims that A is better than B overall are hard to resolve, because it 
involves weighting the relative importance of the ways A is better versus 
the ways B is better.  Claims that A is strictly superior to B can be 
falsified by counterexample -- a case that B can express and enforce that A 
cannot; or can be verified by formal mean -- showing that the power of B can 
be embedded in A in a mutual-suspicion preserving fashion, but not vice versa.

The "in a mutual-suspicion preserving fashion" qualifier is needed to 
escape the trap of Turing universality which would allow anything to be 
embedded in almost anything, and for the embedding result to be meaningful 
from a security perspective.  See 
http://www.agorics.com/agoricpapers/aos/aos.4.html#section4.1 (at the end of 
section 4.1).

My intuition, as you may expect, is that capabilities are strictly superior on 
all practical counts.  However, Java is such a mess that it's hard to even 
formulate the arguments in that context, since we wish to contrast 
capabilities only against the real contender, the essence rather than the 
accident, and I can't tell which is which.

If you don't mind creating what, in my expectation, will be a sacrificial 
lamb for this debate, a 2nd generation clean pure well-designed ACL+stack 
introspection language should be a good enough contender that a definitive 
win for pure capability languages in that context may be the best way to 
settle the debate in general.

Of course, if my hypothesis is wrong, so much the better.  If capabilities 
are not strictly superior on all practical counts, your experimental 
language may be the best way to find this out.  Previous debate on e-lang 
has already (to my great surprise) uncovered a case where ACLs could, in 
principle in some contexts, express and enforce a prohibition that 
capabilities could not 
http://www.erights.org/elib/capability/conspire.html#revokability .  
Although I don't consider this case to have practical effect, since math 
doesn't care much about the boundary between practical and impractical, the 
existence of one case makes plausible the existence of others, some of which 
may have practical effects.

Let's see if we can dispense with the opposite strict practical superiority 
hypothesis quickly.  Please express, in pseudocode if you'd like, the 
MintMaker from the Ode 
using ACLs + stack introspection without capabilities.