DornerWorks

Defend Your Devices Against a Common and Insidious Hack with seL4

Posted on March 31, 2021 by Matthew Russell

How secure is your software?

It’s a simple question with — perhaps all too often — a complex answer.

A more telling question may be, just how quickly can your software be breached?

Hosting providers facilitate the movement of massive amounts of customer data and in some cases provide internet routers to those customers. Trivial as it may seem, even the configuration page for this service can be targeted by malicious hackers who want access to data within.

Someone could direct a DDOS attack at the configuration page and crash the IP stack. The whole system could go down because of a memory leak.

This type of attack can badly damage a company’s reputation, and it happens a lot.

Memory Leak Bugs

When the Heartbleed security bug was discovered in the OpenSSL cryptography library in 2012, an estimated 17% the Internet’s secure web servers were vulnerable to this sort of memory leak attack.

The Microsoft Security Response Centre found that the majority of vulnerabilities detected in Microsoft products since 2004 were “caused by developers inadvertently inserting memory corruption bugs into their C and C++ code.”

That’s all it takes, and as codebases grow, the potential for memory leak vulnerabilities increases, too.

DornerWorks has been helping companies develop secure systems based on the seL4 microkernel for several years. We’ve ported seL4 to the Xilinx Zynq UltraScale+ MPSoC and RISC-V architecture on Microchip’s PolarFire SOC Icicle Kit. Open source RISC-V hardware architecture has provided developers with a cost-effective platform on which to build products that can easily integrate with others in the rapidly growing RISC-V ecosystem. DornerWorks seL4 port to RISC-V hardware makes it possible to build enhanced security into those products, with the added confidence that new devices and supercharged processing platforms like Microchip’s PolarFire SOC can also harness the power of this technology.

Demonstrating seL4’s isolation capabilities

Demonstrating seL4’s isolation capabilities for a US Army SBIR, DornerWorks engineers built two simple HTTP servers running on seL4 on both the Xilinx ZU102 (ARM) and Microchip’s PolarFire SOC Icicle Kit (RISC-V).

At a specified URL, users can see instances running on each of those servers.

Two windows representing HTTP servers built on the seL4 systems running on the ZU102 and PolarFire SOC Icicle Kit.
Two windows representing HTTP servers built on the seL4 systems running on the ZU102 and PolarFire SOC Icicle Kit.
The second server can be crashed by pushing the “Halt and catch fire
The second server can be crashed by pushing the “Halt and catch fire” button.

In one window, the seL4 Web Server Status shows whether the second window is “ALIVE” or “DEAD.”

Pushing the “Halt and Catch Fire” button in the second window crashes that instance by causing a memory leak overflow.

The red “DEAD” box lights up in the seL4 Web Server Status window, indicating that the second server has crashed, while the first runs uninterrupted by the event.

The first window shows the status of the second, and can revive it with a click.
The first window shows the status of the second, and can revive it with a click.

This shows how seL4 can enable isolation and control from another higher privilege process.

Solving memory leak vulnerabilities with seL4

This demonstration shows how seL4 can 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 keeping sensitive information separate from public channels without the use of virtualization.

If you want to enhance the security of your products schedule a meeting with us. We will map out a plan to turn your ideas into reality, based on the secure foundation of seL4.


This material is based upon work supported by the U.S. Army Combat Capabilities Development Command Aviation & Missile Center, Aviation Development Directorate-Eustis under Contract No W911W6-19-C-0036.

Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the U.S. Army Combat Capabilities Development Command Aviation & Missile Center, Aviation Development Directorate-Eustis.

Matthew Russell
by Matthew Russell