[E-Lang] Java 2 "Security" (was: Re: Welcome Chris
Skalkaand ScottSmith of Johns Hopkins)
Mark S. Miller
markm@caplet.com
Sat, 20 Jan 2001 16:13:28 -0800
At 11:38 AM Saturday 1/20/01, Tyler Close wrote:
>[...] It is possible that
>your stack inspection technique could be valuable in this capacity.
>Please note the distinction here though. The stack inspection should
>not be just another way of expressing a prohibition, but a way of
>checking that the prohibition has been correctly expressed.
Well put. As another example, the "rely" and "suspect" declarations we've
been discussing are also cross-checks, but they are Tyler-like cross checks
on whether we've achieved the mathematical properties we intended, not Scott
like cross-checks to stop an attacker in case he gets through our first line
of defense.
Regarding living in the real world, I want to return to my favorite analogy
-- the digital logic gate. A "digital" circuit board or IC chip may not
work as its designers intended, for one of two very different reasons -- the
logic design, which exists in the same pure mathematical universe inhabited
by Tyler's software programs, may have a bug, which is a logical error in
this same mathematical universe. Or the physical embodiment of the chip may
be such that the physical substrate does not faithfully realize the
abstraction of the digital logic gate, for example, because of insufficient
voltage, cosmic rays, a microwave attack, bad analog design, or the
happenstance of quantum uncertainty. However, we don't normally make up for
dangers at this level by redesigning our logic. We put the effort instead
into better ensuring that the physical layer does indeed faithfully realize
the abstraction.
So it is with security. Capabilities are a mathematical secure
computational primitive in the same sense that the digital logic gate is a
mathematical computational primitive. There are two kinds of attacks in
such a system -- those below the level of abstraction, which prevent the
physical embodiment from faithfully realizing the abstraction, and those
above this level, which can only utilize logical errors in the mathematical
expression of what the system is supposed to do. Regarding attacks of the
first type, including the kinds of physical theft Ben talks about, Scott's
defense in depth strategy is often appropriate. However, the systems Scott
proposes to combine -- stack introspection and capabilities -- both exist
above this line, in the mathematical universe, and so can only catch each
other's logical errors, as Tyler explains.
Btw, the "analog vs digital" thing should be taken as an analogy, not
literally. In the analogy, cryptanalysis is below the line, and crypto
primitives are modeled as perfect abstract data types that achieve perfectly
the goals we know they only approximate. Likewise, no one can build a
perfect digital logic gate out of analog material.
Cheers,
--MarkM