If security is your most important concern for your computation, seL4 kernel will solve all future problems. This is the first time that an operating system has passed rugged security tests. The research also found that many kinds of common attacks will not work on the seL4 kernel. For example, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code. Products based on seL4 are expected to be available in the market in 2011.
Trustworthiness of a system has a lot to do with its size. Even well-engineered code has of the order of several defects per thousand lines of code. Hence, a bigger system has inherently more bugs than a small system. L4 is one of the smallest general purpose kernels in existence and is known for its excellent performance, making it an ideal original starting for our work. The seL4 project has extended L4’s applicability to application domains requiring strong security guarantees, and also made it more amenable to formal verification of correctness. Strong security is a fundamental requirement for some existing and emerging embedded application domains and devices, such as personal digital assistants, mobile phones, and set-top boxes. Source: NICTA