Eric Drexler blogging
At Metamodern.com. [link no longer works] Way cool. I look forward to what he has to say.
Unfortunately, one of his early posts falls into the trap of believing that “Computation and Mathematical Proof” [link to http://metamodern.com/2008/11/10/26/ no longer works] will dramatically improve computer security:
Because proof methods can be applied to digital systems, and in particular, will be able to verify the correctness (with respect to a formal specification) of compilers [pdf], microprocessor designs [pdf] (at the digital-abstraction level), and operating system microkernels (the link points to a very important work in progress). Software tools for computer-assisted proof are becoming more usable and powerful, and they already have important industrial-strength applications [pdf]. In a world which increasingly relies on computers for everything from medical devices to national governance, it will be be important to get these foundations right, and to do so in a way that we can trust. If this doesn’t seem important, it may be because we’re so accustomed to living with systems that have built on foundations made of mud, and thinking about a future likewise based on mud. All of us have difficulty imagining what could be developed in a world where computers didn’t crash, were guaranteed to be immune from virus attack, and could safely download code written by the devil himself, and where crucial pieces of software could be guaranteed to not leak data.
The trouble with this approach is that you demonstrably can’t make a useful computer which is immune from virus attack. The proof: a useful computer is one on which I can install software. The user of the computer will have to make a decision about a piece of software. Con men and frausters will continue to convince people to do things which are obviously not in their best interests.
Therefore, however well proven the operating system is, you can’t usefully guarantee them to be free of viruses, because computers are useful when they are generative and social.
That’s implied by his parenthetical “with respect to a formal specification.”
Similarly, the data may be guaranteed not to leak, but can also be guaranteed to be shown to people. (Otherwise, it’s not useful.) Those people can and will leak it. (Ross Anderson’s work on medical systems demonstrates this with a higher level of formality.)
This is not to say that formal methods won’t provide useful results on which we can build. They have, and will continue to in those areas where the problems don’t involve humans, our decisions, or our societies. But human beings are not rational result maximizers who adhere to computer security policies, and all the math in the world won’t change that.