Re: java security concerns

[Ray Cromwell <rjc@clark.net>]

  I think to require formally proven implementation for something
like Java is simply unreasonable. Even if it were possible. The
whole computer market, and for that matter, most of the market as a
whole, relies on "unproven" products. Most of what you buy and use is
based on a notion of "quality" which is merely an inductive argument
that the product had no problems in the past. Everytime you buy a piece
of software and use it, you risk your security. Everytime you ftp
something off the net and run it, you are taking that risk. How do you know 
MS Word doesn't have security holes or trojan horses built in, have you 
seen the source? Software always has bugs, holes, and security flaws. It 
always will. If we were to require each new generation of software to be
"formally correct", software would never evolve. There is an important
feedback process between customers, software companies, and even
hackers, that drives software towards higher quality. Perfect software
implementations proven correct by mathematics is a pipe dream. Maybe
you can have higher confidence in small, simple software -- I've heard
Negroponte expressing that nostalgia for the days of word processors
that ran in 32k of ram, but frankly, I'm glad those days are gone.

   Will the IPv6 and IPSEC stack implementations be formally proven 
correct?   

  Yes, it may be possible that exploiting holes in Java will be easier
than those in sendmail, just as it is easier to exploit a hole in 
software on a networked machine rather than a non-networked one. But this
can not be an argument against Java or its utility. The same arguments
were raised when Postscript first came out, yet the huge benefits
of postscript are obvious, while the amount of security damage
done by it is minimal. Java will have lots of holes. It will go through
the same evolutionary progress that all software does. Sendmail was
given a chance to evolve, I think Java deserves the same
chance, given its potential.

-Ray