A multi-million-dollar contract with the United States Government will see a team of computer scientists from NICTA develop a new breed of software to protect the critical systems in unmanned vehicles from cyber attack.
An international consortium, led by Rockwell Collins with NICTA as a core member, won the 4.5-year, US$18 million project with the US Defense Advanced Research Projects Agency (DARPA). The project promises to have far-reaching future applications protecting the critical systems in motor vehicles, medical devices and aircraft.
“As computers replace mechanical systems in many industries, we are increasingly dependent on the functionality implemented in software,” said Dr Jodi Steel, Director of the Security and Environment Business Team at NICTA. “This project is all about making sure that such systems function as intended, even in the case of cyber attacks.”
The work will be undertaken by the same group of NICTA scientists that developed the highly robust seL4 operating system, named by the prestigious MIT Technology Review in 2011 as one of the top ten technologies likely to change the world. The project is part of DARPA’s High-Assurance Cyber Military Systems (HACMS) program, which aims to produce highly-dependable systems that are resilient to emerging cyber threats. The successful team also includes The Boeing Company, Galois and the University of Minnesota.
As part of the program, the high assurance systems built in the project will be subjected to ‘white box’ attacks by an expert ‘red team’, to test their robustness. White box attacks are pre-arranged attempts to penetrate a system by teams with complete knowledge of their target – their purpose is to expose any security flaws so they can be addressed.
“NICTA’s involvement in this important contract is the result of groundbreaking research undertaken in NICTA’s New South Wales laboratories over more than seven years. We are proud of the innovation and world-leading expertise of the team behind this win, which is significant both for NICTA and for research and development efforts in many industries across the state. I look forward to the economic activity and knowledge exchange that this international contract promises to deliver,” said Andrew Stoner, Deputy Premier of New South Wales and Minister for Trade and Investment.
“NICTA’s selection for this project reflects our status as world leaders in the verification of operating systems,” said Scientia Professor Gernot Heiser, Leader of NICTA’s Software Systems Research Group and the University of New South Wales John Lions Chair. “Now we will have the opportunity to greatly extend the scale, aiming to ensure the safety of a complete, real-world system, something considered impossible only a few years ago.”
In this project, the NICTA team will develop new approaches to address the many challenges involved in building high-assurance systems. The aim is to develop a complete, formally proven architecture to protect the control and communication systems of an aerial vehicle from compromise by faults and targeted attacks.
“NICTA’s participation in this important international project demonstrates the power of world-class research to contribute directly to wealth creation opportunities. Congratulations to all involved,” said Hugh Durrant-Whyte, NICTA’s Chief Executive Officer.
Software that has been formally verified for functional correctness will function according to its specification and will not do anything that is not in that specification, as long as the verification assumptions are met. Such assumptions include for example the hardware working correctly. In 2009, NICTA created a sensation when its researchers proved the correctness of 7,500 lines of C code in the seL4 operating system microkernel. Formal verification has in the past been used to ensure correct operation of critical, but small and isolated pieces of software in fly-by-wire aircraft and nuclear power plants.
