seL4 and Avionics Security Discussed in IEEE Aerospace and Electronic Systems Magazine

Posted on December 3, 2019 by DornerWorks Ltd.

Aircraft safety is important, particularly to those in flight.

One way product developers in the aviation industry are bringing extreme security to their systems with with the seL4 microkernel. This platform provides the formal proof of security for mixed criticality functions running concurrently on a single piece of hardware.

The strength of the seL4 microkernel is enough to shield critical processes from malicious hacking activities that, on unprotected systems, could take over an aircraft’s controls in mid air.

DornerWorks has been working with seL4 for years, and along with being awarded a SBIR contract from U.S. DARPA for porting the seL4 Microkernel to RISC-V architecture, has been instrumental in working with other members of the seL4 Center of Excellence in expanding the seL4 ecosystem.

A paper by DornerWorks former Chief Operating Officer Steve VanderLeest, “Is Formal Proof of seL4 Sufficient for Avionics Security?,” was published by IEEE Aerospace and Electronic Systems Magazine. In the author’s own words:

“The seL4 microkernel is a minimalist operating system that has potential for use in avionics. It has been formally proven to satisfy its specifications, including classic security properties of integrity and confidentiality, making it particularly attractive for systems where safety and security are paramount. Traditional verification methods are good at testing positive requirements– whether the software does something you want, e.g., ‘when I push button X, light B turns on.’ However, those same verification methods are quite poor at testing negative requirements, when we want to ensure the software does not do something, e.g., “the software never takes longer than 10 ms to respond.” Why is that difficult? The number of circumstances we might need to test could be astronomical, making it practically infeasible to check exhaustively.”

Read more about the extreme security seL4 brings to aerospace engineering by clicking the button below.

DornerWorks Ltd.
by DornerWorks Ltd.
Technology engineering so you can focus.