[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
http://www.erights.org/elib/capability/ode/ode-capabilities.html#simple-money
using ACLs + stack introspection without capabilities.
Cheers,
--MarkM