the cost of complexity (was: Re: [E-Lang] Java 2 "Security" (was: Re: Welcome ChrisSkalkaand ScottSmith of Johns Hopkins))

David Wagner daw@mozart.cs.berkeley.edu
25 Jan 2001 08:39:23 GMT


Jonathan S. Shapiro wrote:
>There are elements of a protection system whose architecture can be
>demonstrated to be mathematically correct.

Ahh, yes.  Proofs of correctness for your code are great, when you can
get them.  And yes, I share your preference for principled approaches,
when you can find them.  I absolutely agree.

But there seem to be two challenges which have held this promising
approach back: (1) even figuring out what the right spec should be can
be very expensive in practice (when one considers the overhead it would
add to existing programming practice); and (2) automated theorem provers
today aren't up to proving what everyday programmers would need to get
their jobs done in such a programming environment.

I'd love to see these challenges surmounted and formal methods become
workable in practice, with acceptable overhead.  But we're not there yet
for most mainstream coding tasks.  And in the meantime, we need to do
the best we can, even if our systems aren't absolutely, mathematically
perfect; that's where I see techniques like defense in depth coming
in handy.