seL4 kernel is formally verified

[Nicholas Mc Guire]

On Mon, 17 Aug 2009, Roman Beslik wrote:

> Hi.
> 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  
> performance.

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.

hofrat