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

[Mark S. Miller]

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