seL4 kernel is formally verified

Nicholas Mc Guire mcguire at
Mon Aug 17 14:39:59 CEST 2009

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.


More information about the l4-hackers mailing list