“seL4” is an Unhackable Kernel for Keeping All Computers Safe From Cyberattack

Share on twitter
Share on whatsapp
Share on facebook

unhackable-kernel-sel4Short Bytes: The Australian national research agency Data61 has developed an unhackable kernel named seL4 and proved its unhackable property mathematically. The kernel does this job by separating the critical systems and data from the kernel. 

Today, the threat of cyber attacks isn’t just limited to computers and smartphones. With the ever-increasing intrusion of computers and electronics in our lives, ranging from our home automation system to cars, everything has become a hacker’s target.

This could also create problems in the battlefield where any software plays an important role in military and intelligence systems. Recently, in a DARPA drill, hackers were given the complete access to the computer of a Boeing Little Bird helicopter – but they were unable to disrupt the critical systems of the helicopter. How did this happen? Well, the computer in the helicopter was using a new operating system, based on an unhackable kernel.

Kernel is the heart of any computer’s operating system and if hackers can access it, they can do some irreparable damages to your system. Here, I’m talking about a very dangerous situation where security of power station systems, heart pacemakers, vehicles, weapons etc. could be compromised. The Australian national research agency Data61 has developed an unhackable kernel named seL4 – and proved this mathematically.

Gernot Heiser from Data61 writes, “My hope is that in 10 years’ time, anything that is security critical is running on our system or some other one built on the principles we’ve established.”

The seL4 unhackable kernel comes with some very secure characteristics. It can only do what it’s designed to do and its code is unalterable without permission. Along the similar lines, its memory and data can’t be read without permission. Another interesting fact: An earlier version of seL4, known as OKL4, could be found in millions of smartphones.

The seL4 unhackable kernel works this way by isolating the data and the kernel. This could also be used to run two operating systems simultaneously to stop the hacking.

The seL4 unhackable kernel could also be used in multiple situations like medical equipment, manufacturing plants, automobiles, satellites and more.

Watch the video below to know about the basics of a kernel:

With inputs from New Scientist

Stay tuned for more updates from fossBytes and share your views.

Arpit Verma

Arpit Verma

fossBytes co-founder and an entrepreneur who is in love with budding technologies. A tech enthusiast and a guy who loves to play games and have a good time with his friends!

6 thoughts on ““seL4” is an Unhackable Kernel for Keeping All Computers Safe From Cyberattack”

  1. Avatar

    It is only unhackable now because it has not been made public. In time exploits will be developed if that kernel ever becomes mainstream and runs somewhat popular processing architectures.

  2. Avatar

    Actually read the article(s). They're very clear – it is unhackable in a very specific set of cases, when all of their assumptions are met. And they've proved it mathematically. I have no problem with that statement. What one needs to look at, is are their assumptions reasonable in an actual production system. Like no DMA, and no hardware issues… so while the microkernel in a pristine state meeting all the assumptions could very well be provably unhackable – will it actually be deployed in such a pristine state? If not… might not be unhackable.

Leave a Comment

Your email address will not be published. Required fields are marked *

Scroll to Top