seL4 Microkernel

Sarad AV jtrjtrjtr2001 at yahoo.com
Fri Jan 28 07:07:40 PST 2011


"The L4.verified project
  A Formally Correct Operating System Kernel

L4.verified The University of New South Wales
 
Function calls in the seL4 kernel [What's this?]

In current software practice it is widely accepted that software will always have problems and that we will just have to live with the fact that it may crash at the worst possible moment: You might be on a deadline. Or, much scarier, you might be on a plane and there's a problem with the board computer.

Now think what we constantly want from software: more features, better performance, cheaper prices. And we want it everywhere: in mobile phones, cars, planes, critical infrastructure, defense systems.

What do we get? Mobile phones that can be hacked by SMS. Cars that have more software problems than mechanical ones. Planes where computer problems have lead to serious incidents. Computer viruses spreading through critical infrastructure control systems and defense systems. And we think "See, it happens to everybody." "

Full text in url below
http://ertos.org/research/l4.verified/

One of their papers from wilipedia's citations
http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf

Now, can all these above mentioned problems disappear with seL4 microkernel?

Thanks.





More information about the cypherpunks-legacy mailing list