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.
What you miss is the distinction between different kinds of programs and their protection implications. Networking programs with unintended flaws may allow outsiders to gain access to your internal network and do harm. Non-networking programs with unintended flaws may fail to operate properly or act as a vector for the spread of corruption, but they don't give outsiders unlimited insider access without insiders somehow facilitating the process. That's why we are far more concerned about networking programs that about word processors. In terms of word processors with Trojan horses, we don't want them either, but there's a big difference between a Trojan horse and the ability to spread a virus. Viruses can spread whenever there is sharing and general purpose programming. Hence, most modern spreadsheets, word processors, Postscript interpreters, etc. allow viruses to spread. A big problem with remote auto-execution is that it allows someone not authorized to use your computer decide to run a program on it. This may make you the unwhitting vector for a virus, cause your system to crash, etc. With auto-execution, the web turns from a networked read-only database with limited searching capabilities into a giant distributed processor in which the users have little or no control over what their computers are used for. The battle is for control over your own computer and what it does.
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.
I don't see any huge benefits to postscript. In fact, postscript files are essentially impossible to search for items of interest, to display on a normal video screen, to quote from without reentering the data, etc. The point is, do we want to turn the Web into a distributed computing environment in which anyone can eecute any code on anyone else's computers? Don't assume I am against it - after all, I was the only vocal proponent of viral computing for almost 5 years and got villafied for it plenty of times. I am in favor of making the decision conciously, not by accident or ignorance, and providing proper protection mechanisms. If the question of Hot Java is asked in terms of permitting all computers using the Web to become part of a global viral computing environment, I am ready to hear the answer. -- -> See: Info-Sec Heaven at URL http://all.net Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236