|
From: | Tom Bachmann |
Subject: | Re: Challenge: Find potential use cases for non-trivial confinement |
Date: | Wed, 03 May 2006 20:58:39 +0200 |
User-agent: | Mail/News 1.5 (X11/20060403) |
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Pierre THIERRY wrote: > Scribit Tom Bachmann dies 02/05/2006 hora 21:57: >>> OK. Now how many of these software carry formal proof of their >>> correctness? >> This is not true for the Hurd (afaik) > > Why? > The TCB is more than just the kernel. To formally prove correctness like done with the kernel, the complete TCB would have to be written in bitc. I just didn't hear we want to do this. - -- - -ness- -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.2.2 (GNU/Linux) iD8DBQFEWP1fvD/ijq9JWhsRArWkAJ9vLM5kG44ADVAWNIy23oA1/1fM3QCfZfbK CbruuNxQZM7/kOFxXgjoWQo= =iN2f -----END PGP SIGNATURE-----
[Prev in Thread] | Current Thread | [Next in Thread] |