Enable the Security Potential and Versatility of seL4 in Medical Device Development

Posted on April 23, 2020 by Matthew Russell

Between a qualified medical professional and a hacker with devious intentions, who is more qualified to operate the equipment keeping someone alive?

The answer may seem obvious. Still, cyberthreats are yet enough to keep medical product manufacturers worried.

Doctors, nurses and the healthcare systems they work for all have an obligation to protect their patients and their data. The same is true for the technology employed to make that happen, but as more devices are networked together and connected to the internet, maintaining security and marketability has become a greater challenge. Bad actors may attempt to hijack the firmware updates needed to keep devices functioning as intended, and lengthy certification processes follow any changes in software, bumping development cycles out of an important market window.

Pacemakers, insulin pumps and MRI systems are just three of the examples we’ve seen this century. Along with covering the cost of product recalls and a tarnished reputation, the manufacturers of these products might even be saddled with class-action lawsuits.

A robust security solution can protect medical device manufacturers from costly product recalls.
A robust security solution can protect medical device manufacturers from costly product recalls.

Overcoming security challenges with connected devices

Wirelessly networked medical devices can help medical practitioners deliver a higher quality of care to their patients by saving them time and delivering accurate data when it’s needed most. They provide product developers an accelerated path to improvement through usage data. With a reliable security solution, they can change countless lives for the better.

One way connected medical devices can be made more secure while maintaining market momentum is by separating critical software processes from non-critical ones and isolating communication channels between higher privileged domains. The seL4 microkernel can help accomplish this by providing a trusted software foundation for medical devices. In turn, this makes life easier on both developers and users by providing a secure environment for:

  • Remote equipment monitoring
  • Maintenance and update scheduling
  • Patches that fix problems before equipment breaks down
Wirelessly connected medical devices can enhance the capability of healthcare workers, and the quality of care.
Wirelessly connected medical devices can enhance the capability of healthcare workers, and the quality of care.

A medical product manufacturer developing a convenient new solution to administering anesthetic wanted to make sure the patient’s dosage data would be safe from tampering. DornerWorks guided the company to a hardware accelerated solution that lowered SWAP-C and made room for future flexibility and augmentation with an FPGA-based design.

seL4 could have taken this design a step further. The seL4 microkernel is backed by a formal proof that provides assurance of correctness; such a proof provides additional guarantees against unintentional security vulnerabilities. Furthermore, the open source nature of the kernel means that the latest source code is always available, providing updates for the entire device’s lifecycle.

With the isolation provided by seL4, products built using it can maintain HIPAA compliance through reduced the risk of vulnerability exploitation and software interference, which benefits both developers and practitioners. This isolation also provides the means to update the system and add new components without adversely affecting previously developed functionality; for example, an isolated camera link streaming on the platform could further allow a doctor to monitor a patient remotely, with full control over drug delivery during surgery.

The seL4 microkernel could provide a trusted software foundation for medical devices
The seL4 microkernel could provide a trusted software foundation for medical devices.

In his blog, “seL4 is finally free! Can you afford not to use it?” Scientia Professor Gernot Heiser from UNSW Sydney and CSIRO’s Data61 suggests other potential uses for the seL4 microkernel, including medical implants:

“Medical implants could kill a patient or fail to keep them alive if they fail. Such systems may fail because their critical functionality (that keeps the patient alive) is compromised by a “non-critical” part that misbehaves (either by a bug triggered during normal operation, or a vulnerability exploited by an attacker) Most implants have such “non-critical” code, in fact, it tends to be the vast majority of the software on the device. Most devices these days have some wireless communication capability, used for monitoring the patient, the state of the device, and maybe even to allow the physician to adjust its operation. On systems not built on seL4, there can be no guarantee that this “non-critical” software is free from dangerous faults, nor can there be a guarantee that its failure cannot cause the critical bits to fail.

According to the Linux Foundation, which officially backed the founding of the seL4 Foundation in April 2020, “The trustworthiness of embedded computing systems is vital to improving the security of critical systems around the world to safeguard them from cyber threats. This is particularly paramount in industries including avionics, autonomous vehicles, medical devices, critical infrastructure and defense. The seL4 microkernel is the world’s first operating system with a proof of implementation correctness and presents an unparalleled combination of assurance, generality and performance, making it an ideal base for building security- and safety-critical systems.”

DornerWorks, a member of the seL4 Foundation, has been working to accelerate the adoption of the seL4 microkernel as a trusted software foundation for system security. During multiple SBIR contracts with DARPA, our engineers have ported seL4 to the Xilinx Zynq UltraScale+ MPSoC and open source RISC-V architecture. We can help you enhance the security of your medical 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