Walsh: Secure Virtualization Using SELinux (sVirt) [LWN.net]

Walsh: Secure Virtualization Using SELinux (sVirt)

Posted Aug 26, 2009 9:36 UTC (Wed) by renox (guest, #23785)
In reply to: Walsh: Secure Virtualization Using SELinux (sVirt) by mheily
Parent article: Walsh: Secure Virtualization Using SELinux (sVirt)

> seL4 sounded great until I read this part:
>
>> The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary. We are endeavouring to release seL4 in the future, but the time-line and exact nature of the release is yet to be decided.

> Thanks, but no thanks. There are already plenty of other free microkernels out there (L4, Mach, Coyotos, HURD, Minix, etc.)

Sure, but those don't have the 'proof of correctness' feature so you shouldn't say that they're plenty of free alternative: if you really need this feature then AFAIK only proprietary OS provide it currently, otherwise sure there are plenty of free alternative.

to post comments

Walsh: Secure Virtualization Using SELinux (sVirt)

Posted Aug 26, 2009 16:40 UTC (Wed) by Wol (subscriber, #4433) [Link] (2 responses)

Unfortunately, a "proof of correctness" isn't worth the paper it's written on.

It's maths, therefor, as per Godel, it's either trivial, wrongly spec'd, or wrongly proved. At least ONE (and probably two) of those conditions MUST be true.

Poof! there's your proof gone up in smoke...

Cheers,
Wol

Walsh: Secure Virtualization Using SELinux (sVirt)

Posted Aug 26, 2009 20:34 UTC (Wed) by jordanb (guest, #45668) [Link]

Godel says no such thing.

Walsh: Secure Virtualization Using SELinux (sVirt)

Posted Aug 27, 2009 3:12 UTC (Thu) by njs (subscriber, #40338) [Link]

> It's maths, therefor, as per Godel, it's either trivial, wrongly spec'd, or wrongly proved.

Out of curiosity, which of those categories do you think Goedel's proof falls into?

Open Proofs

Posted Aug 27, 2009 14:05 UTC (Thu) by dwheeler (guest, #1216) [Link]

There's a big need for software that is proven correct and for which the implementation, proofs, and required tools are all open source software. I call such software "open proofs". If you're interested in helping, please visit the Open proofs web site; we need people who can package existing OSS tools, as well as people who can develop and prove programs.