Unmanned aerial vehicles (UAVs) using NICTA’s secure seL4 kernel have survived penetration testing.
The tests are part of a DARPA High-Assurance Cyber Military Systems (HACMS) program.
Secure Mathematically Assure Composition of Control Models (SMACCM) is a joint US$18 million project running for four-and-a-half years. The team consists of formal verification and synthesis groups in NICTA, Rockwell Collins Galois, Boeing and the University of Minnesota.
NICTA has completed phase two of the project and held end-of-phase demos recently. A Boeing video showing an optionally piloted autonomous helicopter called the Unmanned Little Bird running seL4 is expected to be released later this year.
NICTA professor and software systems group research leader Gernot Heiser said the ULB underwent testing by professional penetration testers.
“We basically stopped them [testers] from compromising the copter. The operating system has properties which means parts of it can be compromised but the essential controls remain intact.”
The aim of the project is to detect and deter cyber-attacks across a wide range of automated systems, he added. This includes smartphones, military systems, medical devices as well as UAVs.
The system is able isolate different flight controls or components, so if one is compromised the attack does not spread to other controls.
A microkernel is a compact kernel that performs only minimal functions such as inter-process communication (IPC) with core functions such as file systems running in userland.
Not having all functions run in privilege mode means that if one process breaks down, the others can still run efficiently.
Heiser said that phase three of the project will take 18 months to complete. Data from the tests in the last stage will be keenly examined by researchers.
While the project is US-lead, there have been some very early discussions with the Australian Defence Force, federal and state police about the seL4-protected UAVs.