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.
Gernot Heiser wrote:
For an outsiders' view see this article:
http://www.computerworld.com.au/article/314817/nicta_wins_race_secure_l4