CSIRO logo

Game-Changing Innovation Tackles the CyberSecurity Conundrum

Once worthy of headlines, cybersecurity breaches have become so routine that only the most egregious are reported by the media. Cybersecurity is not restricted to criminal groups engaged in for-profit attacks but also nation states engaged in cyberwarfare1. Yet, even those barely register with the public.

We have become numb to the continuous threat partly out of frustration with current cybersecurity approaches and partly from the sheer magnitude of the problem. At the core it is a race between the attacker and the defender, where the attacker has the advantage and, in the long term, will always win.

We got to this point not by lack of diligence or innovation but from the break-neck evolutionary speed of technology, globalization and business models. Data and systems are increasingly interconnected and interdependent which will only increase with IoT (Internet of Things) and AI (Artificial Intelligence)2. Yet we do not look at systems holistically. Most established software systems were never architected to address the cyber risks that are commonplace today. Add to that, we have approached cyber security reactively and targeted symptoms with code patches, intrusion detection, firewalls, etc. The result is much like the game of Whac-a-Mole3.

Decades ago Tony Hoare4 had a different vision. He believed and dedicated his career to developing formal verification, in essence mathematical proof, that “solves the problems of reliability that arise when programs get large and more safety-critical5 .” Great idea but one the industry felt was unattainable.

Today, CSIRO’s Data61 made Hoare’s vision a reality and shows it is a more effective solution for cybersecurity. In essence, the approach is to provide formal, mathematical proof, in a cost effective and scalable manner, that software code does what it is supposed to do and nothing more.

This is achieved with seL4, the secure embedded L4 microkernel, a game-changing approach that enables software engineers to design-in resiliency and a verified foundation while building code. What differentiates seL4 is that it enforces security by “ensuring isolation between trusted and untrusted system components and by carefully controlling software access to hardware devices6” and supporting memory protection for stronger component isolation. Most systems are hacked by attacking non-critical components through interconnections with critical components. This enables bad actors to gain access to the whole system; isolation is key. What makes seL4 truly unique is the formal proof of its correctness and isolation enforcement. seL4 is open source and available on GitHub .

The Data61 Trustworthy Systems team developed the microkernel and its formal proof, and demonstrated that it is deployable in enterprise and commercial systems. The team partnered with Rockwell Collins, Galois Inc., Boeing and the University of Minnesota7 to demonstrate that formally verified software is effective at preventing cyberattacks on embedded computer software in autonomous air vehicles. Beyond the military domain, where it has been demonstrated, the technology is ready for use in civilian contexts, including self-driving cars, commercial aerospace, critical infrastructure, IoT, and commercial space satellites.

seL4 demonstrates the power of open innovation to solve a global problem and disrupt an entire industry. The game-changing impact of seL4 is that organizations no longer have the ‘excuse’ that they could not prevent the breach. This technological innovation will ultimately change how regulatory bodies monitor and hold accountable organizations that do not secure their systems. As June Andronick , Principal Research Scientist and Research Group Leader at CSIRO Data61 said, “Cybersecurity is a key risk that needs a true attitude shift and a change of the state-of-the-art, towards software with built-in security and strong, mathematical evidence that security is enforced.

CSIRO US facilitates relationships with US companies, government agencies and academic institutions to connect Australian researchers with USA projects to expedite mutually beneficial opportunities for scientific advancements in food agriculture, space, water conservation, wildfire and smart cities. Partnering in open innovation not only brings deep scientific research competencies to the table but also deep experience with a wide range of real world problems.


Once worthy of headlines, cybersecurity breaches have become so routine that only the most egregious are reported by the media.