Timothy C. May writes:
SCRUFFIES AND NEATS IN SECURITY
The "security neat" believes in applying rigor to security. Machines and languages should be "provably secure." (Better yet, machines should be "provably correct," a la Viper, and operating systems and languages should produce provably correct code.)
Don't take this the wrong way, Tim, but you have totally misinterpreted the position many of us who dislike Java take. You completely mischaracterize our attitude. There are two philosophies in opposition here, the optimistic model versus the realistic model. 1) "We are smart, so we simply build something that feels good and provided we can't find a way to break it we declare it secure." This is the Java model. Java isn't "scruffy". Its a very elegant and cleanly built system, far more elegant than most. I contend that it is flawed, but not because it is "scruffy". I contend that the flaw is that its security depends on all its parts working flawlessly, and that we can't build flawless systems. Such systems are made on the liberal assumption that humans can design something perfect in all its parts. To trust a system built on such an assumption, you ultimately need a proof of its security from top to bottom. The very reason I think such a system is impractical is that I agree with the notion that such proofs are not possible or if they are made are often as buggy as the code was, proofs merely being a formalism in a different language. This is the wrong paradigm, from the start. 2) "We are ignorant, so we build something that does as little as we can get away with, makes the assumption at every stage that every component of the system might be broken, and put seventeen layers of armor around it on the assumption that we still have probably made a mistake or two in designing the system." This is the model that modern firewalls built by the likes of me take -- systems that are designed to be tolerant of multiple engineering failures. Such systems are built on the assumption that humans are fallible. Such systems, unlike Java, do not depend on flawless operation of all their components for their security. Such systems are built on the conservative assumption that humans are going to make mistakes and that you have to take account of your own fallibility when designing secure systems. In such a system, one can have breeches of the security of four major subsystems and the fifth still keeps you alive. The "belt and suspenders" model doesn't require mathematical proofs of security because it was engineered, from the start, to be robust. Tim misunderstands, thinking this is a case of some foolish perfectionists getting mad at the guys who throw things together and hope that they work. Not at all. Our problem with Java is the security model, which inherently requires perfect design and operation. We build our own systems to be robust enough to survive our own mistakes. Java is built such that any mistake is fatal. Essentially, this is the optimists versus the realists. Perry PS BTW, Tim, Java is great for the theorem prover fetishizers -- look no further than Java's bytecode verifier. I have never built a system that required an "active defense" like that. They fill me with the same sort of dread I would get from a skyscraper design that required a constant flow of electricity to the building lest it collapse. Sure, its cool. Maybe it even saves some money. However, can you sleep at night inside it?