NCipher Takes Hardware Security To Network Level

[bear]

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 majordomo at metzdowd.com