DornerWorks

How seL4 can Protect Against Massive Data Breaches

Posted on April 27, 2021 by Matthew Russell

It was months before anyone knew what had happened.

A major IT company’s systems had been breached by a foreign-based cyberattack that soon spread to its clients, including government agencies and crucial American businesses.

How does a supply chain attack happen?

Don't let platform vulnerabilities lead to a massive data breach.
Don’t let platform vulnerabilities lead to a massive data breach.

The attack gave intruders unmitigated access to sensitive data on millions of users. In this case, it all started with a surreptitious code injection.

After the code was added to the backend, every update or patch sent out from the company to its customers proliferated the threat. The code created a backdoor to customer’s information technology systems, which hackers then used to install even more malware that helped them spy on companies and organizations.

Before the dust settled, it was clear that US agencies including parts of the Pentagon, the Department of Homeland Security, the State Department, the Department of Energy, the National Nuclear Security Administration, and the Treasury were attacked. Private companies like Microsoft, Cisco, Intel, and Deloitte, and other organizations like the California Department of State Hospitals, and Kent State University were also affected.

US Cyber Command, the federal agency tasked with protecting American networks, was caught completely off guard. It was actually U.S.-based cybersecurity company FireEye who first discovered the intrusion which had by then already accessed its own servers.

To this day, some victims may never realize they were hacked.

“We have a serious problem. We don’t know what networks they are in, how deep they are, what access they have, what tools they left,” said Bruce Schneier, a prominent security expert and Harvard fellow.

What happens next?

DornerWorks engineers can help you apply the security features of seL4 to your system.
DornerWorks engineers can help you apply the security features of seL4 to your system.

The SolarWinds breach was one of the largest in recent history and could precipitate a number of changes within US Cyber Command itself, spurring greater collaboration with the private sector in fighting nation-state attacks and foreign bad actors in the future.

The White House is now encouraging software developers to build more security into their products. That may seem as challenging as it is ambiguous, but it is possible to build software you can trust. One way to gain that trust is by building software applications on the seL4 microkernel.

How does seL4 keep software secure?

The formal proof of seL4 provides confidence to you and your customers that core aspects of your system are actually secure. The binary code of the seL4 microkernel correctly implements the behavior described in its abstract specification and nothing more. This prevents the following in the kernel:

  • Undefined behavior
  • Memory leaks
  • Buffer overflows
  • Null pointer dereferences (pointer errors in general)
  • Arithmetic overflows and exceptions

The specification and the seL4 binary satisfy the classic security properties of integrity and confidentiality. Integrity means that data cannot be changed without permission, and confidentiality means that data cannot be read without permission. These properties are crucial in any system that requires extreme security and/or safety. They are the backbone for systems that rely on isolation. Moreover, this makes seL4 an attractive solution for systems that may not have extreme security requirements, but still want proven isolation between separate software components.

In addition, seL4’s security and core functionality is backed by mathematical proof.

What does seL4 security look like?

Build cyber-resilient products with the security features of seL4 and engineering expertise from DornerWorks.
Build cyber-resilient products with the security features of seL4 and engineering expertise from DornerWorks.

Dr. John Launchbury presented a real-life demonstration of the seL4 microkernel’s security potential as program manager of the HACMS program, funded by DARPA. After a team of government-trained penetration testers took over the controls of a commercially available drone in a matter of minutes, they gave up after hours of trying to hack into another otherwise identical drone running the seL4 OS.

Much to the disappointment of malicious hackers, seL4 can also be used to isolate an IP stack from a public-facing webpage while monitoring its health at the same time. The configuration page for a secure router, for example, is far more secure when isolation properties can be backed up by seL4’s mathematical proof than when based on a monolithic system. seL4 minimizes the attack surface while its virtualization functionality enables the separation of sensitive information from public channels.

The fallout from a data breach would have been minimized had the attackers dropped their code onto a seL4-based system with trusted boot features, which would have restricted the applications able to run on the system to only those signed with approved keys. Being isolated from other critical channels, like those which deploy updates to customer systems, a costly cascade of malicious code could have been avoided altogether.

How to get started with seL4


As an inaugural member of the seL4 Foundation, DornerWorks has been helping companies and Department of Defense organizations enable advanced security with the seL4 microkernel for years. During multiple SBIR contracts with DARPA, our engineers ported seL4 to the Xilinx Zynq UltraScale+ MPSoC and open source RISC-V architecture. More recently, we upstreamed virtualization support for 64-Bit x86 CPUs on seL4.

We can help you enhance the security of your products using seL4, better your customers’ lives and give your business a competitive edge.

Schedule a meeting with us today and get started.

Matthew Russell
by Matthew Russell