On Mon, 13 Oct 2003, Jerrold Leichter wrote:
>Very few real efforts were made to actually produce a "provably correct" OS. >The only serious commercial effort I know of was at DEC, which actually did >a provably-correct virtual machine monitor for VAXes. I knew some of the >guys who worked on this. It was difficult, expensive, required a level of >integration that only a company like DEC - the did both the OS and the hard- >ware, which had to be modified to make the VMM run decently - was in a position >to provide. But it was quite possible. I think this is just a question of where the target is this year. As long as systems continue to become more complex, the individual parts of those systems are going to have to become more reliable. The alternative is that the complex systems die under a mass of tiny bugs that interact in bad ways. As memory space becomes larger and systems that take advantage of it become more complex, we're going to see ever-increasing reliability requirements of the individual components. And, at some point, "proofs of correctness" will be necessary as sales points for the individual components. Right now, we're not seeing it much yet. But I saw a proof of ext3 journaling fileystem software, buried in one of the design documents. It demonstrated that there is no possible order in which the filesystem interface routines can be called that will leave the system in an undefined state. Of course, that proof assumed that the read/write operations in the hardware were error-free, which is not the case. They come close though, with the sector checksums an error correction codes. Filesystems are a nice microdomain for proofs of software correctness, partly because operations on them are fairly constrained and partly because they are subject to hardware errors; if you want to say with assurance that some crash isn't the filesystem drivers' fault you have to prove it. Crypto is another nice microdomain for proofs of software correctness, because it is also constrained, but operates under assumptions of malicious attack or efforts at subversion, and is relied upon to protect valuable information. If you want to say that a particular security breach isn't the crypto software's fault, you have to prove it. But, as systems grow more and more complex, and you have many thousands of subsystems and components interacting, you're going to see more and more of these little microdomains, because when it gets to that level you have to have some *very* stringent requirements for correctness in all those little subsystems. I see correctness proofs for many key infrastructure components of the OS as likely to be fairly common in another ten years, or half that if the OS market shows signs of actual competition. OTOH, I don't think proofs of correctness for user-level applications is likely to ever happen, because the potential loss of value tends to be less for an application crash than for a hosed OS. Bear --------------------------------------------------------------------- The Cryptography Mailing List Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]