SeL4 gets the Boeing test
On 24 July 2015, Boeing tested Data61’s (formerly known as NICTA) seL4 – the “world’s most highly assured operating system” – on its autonomous Unmanned Little Bird (ULB) helicopter.
Running its own mission board software on top of the seL4, Boeing tested to see if could be hacked into while in flight, with it not succeeding an attack.
seL4 is a formal mathematical proof that guarantees isolation between components of a system.
NICTA demonstrated how a hacker can remotely connect and get root access to a virtualised Linux instance of the ULB mission board, which sits on top of the seL4 operating system. The hacker can then try to crash Linux by using up all the CPU available to the Linux instance.
Because of the isolation properties of the seL4, the helicopter could continue to function despite the Linux instance being affected.
NICTA is also working with Defence Science and Technology Organisation to support secure access to multiple classification data and networks using one portable device, instead of many different devices.
In the above video, Ihor Kuz, senior researcher at Data61, explains how seL4 passed the test of an attack on a Boeing autonomous helicopter.