Security Experts:

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.

A video demonstration from NICTA is embedded below:

Written By

Eduard Kovacs (@EduardKovacs) is a contributing 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

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.

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.

Cloud Security

VMware vRealize Log Insight vulnerability allows an unauthenticated attacker to take full control of a target system.

IoT Security

Lexmark warns of a remote code execution (RCE) vulnerability impacting over 120 printer models, for which PoC code has been published.

Application Security

Drupal released updates that resolve four vulnerabilities in Drupal core and three plugins.

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...

Vulnerabilities

A high-severity format string vulnerability in F5 BIG-IP can be exploited to cause a DoS condition and potentially execute arbitrary code.

Email Security

Microsoft is urging customers to install the latest Exchange Server updates and harden their environments to prevent malicious attacks.

Mobile & Wireless

Apple rolled out iOS 16.3 and macOS Ventura 13.2 to cover serious security vulnerabilities.