Connect with us

Hi, what are you looking for?

SecurityWeekSecurityWeek

Data Protection

Highly Secure Operating System seL4 Released as Open Source

Secure embedded L4 (seL4), said to be the world’s most highly-assured operating system, has been released as open source, Australia’s Information and Communications Technology Research Centre of Excellence (NICTA) and U.S. aerospace and defense company General Dynamics C4 Systems announced on Tuesday.

Secure embedded L4 (seL4), said to be the world’s most highly-assured operating system, has been released as open source, Australia’s Information and Communications Technology Research Centre of Excellence (NICTA) and U.S. aerospace and defense company General Dynamics C4 Systems announced on Tuesday.

The organizations are making available not only the source code for the seL4 microkernel, but also formal mathematical proofs, libraries, tools and programs that can be used as an example by those who want to develop secure systems.

“What is being released today is not only the breakthrough proofs NICTA achieved in 2009, but a whole host of advanced work built on top of that in the last five years,” said Dr. Gerwin Klein, senior principal researcher and leader of formal verification at NICTA. “This includes new, stronger security proofs, verification of not only the C code, but the binary of the kernel, and a large amount of support and example code that will enable developers to get started quickly. With the proof released, you don’t have to trust that the kernel was developed correctly – you can check the evidence yourself.”

seL4, the most advanced member of the L4 microkernel family, is not susceptible to stack smashing, code injection or return-oriented programming (ROP) attacks because it’s designed not to operate in unspecified ways. According to NICTA, the operating system is bug free and it’s secure in the interpretation of classic operating system security.

The microkernel supports ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) and all modern x86 processor architectures, the organization noted in an FAQ. 

At the beginning of July, NICTA published a video to demonstrate how seL4 could protect an aerial drone against cyberattacks. However, the organization points out that this is a general-purpose microkernel that’s ideal for embedded systems with security or reliability requirements, particularly on “platforms that provide virtual memory protection and for application areas that need isolation between different parts of the software.”

“seL4 takes software dependability to a new level, and will support the development of truly trustworthy systems,” explained Gernot Heiser, Software Systems Research Group Leader at NICTA. “There is ample evidence of the fundamental shortcomings of today’s critical software. By open-sourcing seL4 we hope to create a world-wide community of developers of dependable systems, in application areas ranging from national security to automotive, avionics, medical implants, industrial automation and BYOD in corporate environments.”

seL4 code and proofs are available on GitHub under GNU General Public License, version 2.

Advertisement. Scroll to continue reading.

A video demonstration from NICTA is embedded below:

Written By

Eduard Kovacs (@EduardKovacs) is a managing editor at SecurityWeek. He worked as a high school IT teacher for two years before starting a career in journalism as Softpedia’s security news reporter. Eduard holds a bachelor’s degree in industrial informatics and a master’s degree in computer techniques applied in electrical engineering.

Click to comment

Trending

Daily Briefing Newsletter

Subscribe to the SecurityWeek Email Briefing to stay informed on the latest threats, trends, and technology, along with insightful columns from industry experts.

Understand how to go beyond effectively communicating new security strategies and recommendations.

Register

Join us for an in depth exploration of the critical nature of software and vendor supply chain security issues with a focus on understanding how attacks against identity infrastructure come with major cascading effects.

Register

Expert Insights

Related Content

Application Security

Cycode, a startup that provides solutions for protecting software source code, emerged from stealth mode on Tuesday with $4.6 million in seed funding.

Vulnerabilities

Less than a week after announcing that it would suspended service indefinitely due to a conflict with an (at the time) unnamed security researcher...

Data Protection

The cryptopocalypse is the point at which quantum computing becomes powerful enough to use Shor’s algorithm to crack PKI encryption.

Data Breaches

OpenAI has confirmed a ChatGPT data breach on the same day a security firm reported seeing the use of a component affected by an...

Artificial Intelligence

The CRYSTALS-Kyber public-key encryption and key encapsulation mechanism recommended by NIST for post-quantum cryptography has been broken using AI combined with side channel attacks.

IoT Security

A group of seven security researchers have discovered numerous vulnerabilities in vehicles from 16 car makers, including bugs that allowed them to control car...

Vulnerabilities

A researcher at IOActive discovered that home security systems from SimpliSafe are plagued by a vulnerability that allows tech savvy burglars to remotely disable...

Risk Management

The supply chain threat is directly linked to attack surface management, but the supply chain must be known and understood before it can be...