l4-hurd
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Challenge: Find potential use cases for non-trivial confinement


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-----




reply via email to

[Prev in Thread] Current Thread [Next in Thread]