[E-Lang] Java 2 "Security" (was: Re: Welcome Chris Skalkaand ScottSmith of Johns Hopkins)
Sat, 20 Jan 2001 19:38:27 -0000
Scott Smith wrote:
> ANY security system ultimately boils down
> to statistics
> on how many violations happen and their cost, NOT to some proof of
> correctness, because every security system lives in this
> universe with
> real people and computers, not in a mathematical universe.
I think there are subtleties of scope here that you are missing. There
are definitely parts of a security system that exist purely in a
mathematical universe. For these parts, it makes sense to think in
terms of proofs of correctness. For these parts, thinking in terms of
violation statistics does not make sense. For these parts, the
possibility of violation means that the entire part is totally broken.
The program text of a software program is something that exists purely
in a mathematical universe. Code on a piece of paper, or in a text
editor has no physical properties. It is only subject to the laws of
the language grammar in which it is written. This is what code is
defined to be. Evaluating code as if it were subject to the law of
gravity does not make sense. It exists in a different universe.
For this reason, I think your arguments for added security expressions
are mis-targeted. Since code exists in a mathematical universe, adding
protections to protections does not make sense; however, something
very similar does make sense. It makes sense to take measurements of
the space mapped out by a particular software program. When a
programmer creates a particular piece of program text, he is
attempting to map out a particular space of possible state
transitions. This space is often larger than can be tested. A
mathematical proof of the code is also often elusive. Often however,
the programmer is able to construct a list of state transitions that
he believes are not possible in the space that his code defines. If it
is possible to formally specify these anti-transitions, then it might
be possible for the computer runtime to check for these
anti-transitions while the program is executing. 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.