It has been announced today that the National Cyber Security Centre (NCSC), a part of GCHQ, has joined the seL4 Foundation an organisation which aims to expand the ecosystem around the seL4 microkernel.
Image courtesy NCSC
The seL4 software is used to create separation and controlled communication between parts of a computer system. Before seL4, establishing the required level of separation for many government use-cases required bespoke hardware. seL4 is a high-assurance software alternative which enforces this separation while maintaining high levels of trust.
The NCSC uses seL4 to enforce separation in a number of high-assurance situations. This has saved costs while reducing the need for specialised hardware, without compromising cyber security.
NCSC researchers have studied seL4 over the past few years. Its mathematically backed verification and automated proofs of correctness and security indicate a high level of resilience against software attacks.
NCSC Technical Director Dr Ian Levy said: “We’re pleased to join the seL4 Foundation, seL4 is some of the most highly assured software and its development plays an important role in the next generation of high-assurance devices.
“We support the long-term stability of the seL4 microkernel ecosystem and are looking at opportunities to develop our use-cases for it.”
To find out more about seL4, see the foundation’s website: