seL4 kernel is formally verified
Nicholas Mc Guire
mcguire at lzu.edu.cn
Mon Aug 17 14:39:59 CEST 2009
On Mon, 17 Aug 2009, Roman Beslik wrote:
> Are there any indications which properties of seL4 are verified?
> Heiser said one of the primary research objectives was to come up with a
> kernel that would not only be verified but whose performance would be
> suitable for use in real-life systems.
> ?My briefing was that we must not *lose more than 10 per cent
> performance through the verification process*. Right from the start,
> this was not just an academic exercise but something that was for
> real-world use.?
> I just can't understand how a verification process can undermine
simply by putting constraints on permitted code constructs and thus
potentially prevent optimization in some cases - most C verification
will require to use only a subset of C (something like C-light) putting
constraints on switch statements, goto and the use of pointers.
More information about the l4-hackers