Microkernels Really Do Improve Security

We are thrilled to re-post this microkerneldude blog post –Random rants and pontifications by Gernot Heiser

Many of us operating systems researchers, going back at least to the US DoD’s famous 1983 Orange Book, have been saying that a secure/safe system needs to keep its trusted computing base (TCB) as small as possible. For system of significant complexity, this argues for a design where components are protected in their own address spaces by an underlying operating system (OS). This OS is inherently part of the TCB, and such should itself be kept as small as possible, i.e. based on a microkernel, which comprises only some 10,000 lines of code. Which is why I have spent about a quarter century on improving microkernels, culminating in seL4, and getting them into real-world use.


Monolithic vs microkernel-based OS structure.

It is intuitive (although not universally accepted) that a microkernel-based system has security and safety advantages over a large, monolithic OS, such as Linux, Windows or macOS, with their million-lines-of-code kernels. Surprisingly, we lacked quantitative evidence backing this intuition, beyond extrapolating defect density statistics to the huge TCBs of monolithic OSes.

Finally, the evidence is here, and it is compelling

Together with two undergraduate students, I performed an analysis of Linux vulnerabilities listed as critical in the Common Vulnerabilities and Exposures (CVE) database. A vulnerability is tagged critical if it I easy to exploit and leads to full system compromise, including full access to sensitive data and full control over the system.

For each of those documented vulnerabilities we analysed how it would be affected if the attack were performed against a feature-compatible, componentised OS, based on the seL4 microkernel, that minimised the TCB. In other words, an application running on this OS should only be dependent on a minimum of services required to do its job, and no others.

We assume that the application requires network services (and thus depend on the network stack and a NIC driver), persistent storage (file system and a storage device driver) and console I/O. Any OS services not needed by the app should not be able to impact its confidentiality (C), integrity (I) and availability (A). For example, an attack on a USB device should not impact our app. Such a minimal TCB architecture is exactly what microkernels are designed to support.

The facts

The complete results are in a peer-reviewed paper, I’m summarising them here. We find that of all of the 115 critical Linux CVEs, we could analyse 112, the remaining 3 did not have enough information to understand how they could be mitigated. Of those 112:

  • 33 (29%) were eliminated simply by implementing the OS as a componentised system on top of a microkernel! These are attacks against functionality Linux implements in the kernel, while a microkernel-based OS implements them as separate processes. Examples are file systems and device drivers. If a Linux USB device driver is compromised, the attacker gains control over the whole system, because the driver runs with kernel privileges. In a well-designed microkernel-based system, only the driver process is compromised, but since our application does not require USB, it remains completely unaffected.
  • A further 12 exploits (11%) are eliminated if the underlying microkernel is formally verified (proved correct), as we did with seL4. These are exploits against functionality, such as page-table management, that must be in the kernel, even if it’s a microkernel. A microkernel could be affected by such an attack, but in a verified kernel, such as seL4, the flaws which these attacks target are ruled out by the mathematical proofs.
    Taken together, we see that 45 (40%) of the exploits would be completely eliminated by an OS designed based on seL4!
  • Another 19 (17%) of exploits are strongly mitigated, i.e. reduced to a relatively harmless level, only affecting the availability of the system, i.e. the ability of the application to make progress. These are attacks where a required component, such as NIC driver or network stack, is compromised, and as a result compromising the whole Linux system, while on the microkernel it might lead to the network service crashing (and becoming unavailable) without being able to compromise any data. So, in total, 57% of attacks are either completely eliminated or reduced to low severity!
  • 43 exploits (38%) are weakly mitigated with a microkernel design, still posing a serious security threat but no longer qualifying as “critical”. Most of these were attacks that manage to control the GPU, implying the ability to manipulate the frame buffer. This could be used to trick the human user into entering sensitive information that could be captured by the attacker.

Only 5 compromises (4%) were not affected by OS structure. These are attacks that can compromise the system even before the OS assumes control, eg. by compromising the boot loader or re-flashing the firmware, even seL4 cannot defend against attacks that happen before it is running.


Effect of (verified) microkernel-based design on critical Linux exploits.


What can we learn from this?

So you might ask, if verification prevents compromise (as in seL4), why don’t we verify all operating systems, in particular Linux? The answer is that this is not feasible. The original verification of seL4 cost about 12 person years, with many further person years invested since. While this tiny compared to the tens of billions of dollars worth of developer time that were invested in Linux, it is about a factor 2–3 more than it would cost to develop a similar system using traditional quality assurance (as done for Linux). Furthermore, verification effort grows quadratically with the size of the code base. Verifying Linux is completely out of the question.

The conclusion seems inevitable: The monolithic OS design model, used by Linux, Windows, macOS, is fundamentally and irreparably broken from the security standpoint. Security is only achievable with a (verified) microkernel design. Furthermore, using systems like Linux in security- or safety-critical applications is at best grossly negligent and must be considered professional malpractice. It must stop.

This article was originally posted at https://microkerneldude.wordpress.com/2018/08/23/microkernels-really-do-improve-security/

Three Takeaways from SINET Melbourne

I recently had the honor of being a panelist at SINET Melbourne.

SINET is dedicated to building a cohesive, worldwide Cybersecurity community with the goal of accelerating innovation through collaboration. The organization’s global series of events act as a catalyst that connects senior level private and government security professionals with solution providers, buyers, researchers and investors.

In Melbourne, I had a front row seat, and here were my three most important takeaways.

Cybersecurity awareness has gone mainstream.

As someone who has kept a keen eye on the evolution of cybersecurity in the last decade, I’m very encouraged to see that we no longer have to convince organizations to care about security. The conference presented in-depth information on how we deal with cyberthreats, as well as how we can remediate and manage attacks. That being said …

We’re missing a big piece of the puzzle.

An area where I’d obviously love to see more of a focus is on the move toward modular device design. The modular approach starts with the fundamentals of good security, including redundancy and defense-in-depth system implementation. Systems must move from an old-school monolithic approach to a modular approach. And this isn’t just a security play. …

That piece of the puzzle will change everything.

Modular device design is like constructing a solid building foundation – no one wants to talk about it. Everyone notices the sweeping architecture of a building or the latest technology that allows for a virtualized concierge, but no one stands around oohing and ahhing at the foundation. But a foundation created on the fundamentals of good security enables you to build something innovative on top. That is how I view the importance of modular design. Yes, it’s a security play, but it goes so much further than that.

I’m excited to see the awareness that cybersecurity now has, but my hope is that as we move forward, we can engage stakeholders – particularly the younger generation of cyber professionals – to embrace modularity and enable the next wave of innovation.


Need Acceleration? Hit the Gas, Aussie Style

For the past 30+ years, it has been a pleasure to contribute to the wireless ecosystem through the ongoing evolution in this space. From AMPs, to CDMA, to GSM, to 3G/4G and now 5G it has been a period of exponential change, though none of it included discussions about security.  You would have thought that I had seen it all…until now. Recently I had the privilege to be a part of the Australian Trade Mission’s Landing Pad program in San Francisco. I can honestly say that I, my company, and my world view have been positively transformed as a result of the 90-day residency.

The transformation began when AustCyber suggested we apply for the San Francisco Landing Pad project through Austrade. We were one of five Australian cybersecurity companies that were selected to participate. These five companies now became, affectionately known as the AustCyber Cohort.

What is it like to participate in one of Australia’s Landing Pads? The best way to describe it is intense, demanding and surprisingly collaborative. I was locked in a room everyday with other Australians whose sole focus aligned with that of our company, Cog. With feet on the street in Silicon Valley (the global hub of innovation), we got down to business (and a bit of fun, as well). Yes, it was difficult at times, but the work environment led to less day-to-day distractions, kept me highly focused and ultimately led to significant results for Cog.

Our company went into the Landing Pad project with three goals:

  • Raise the company profile among influencers and decision makers in Silicon Valley
  • Obtain new customers
  • Expand relationships in the VC community

My days were filled with prospecting and meetings across the Bay area with potential customers and VC’s. The goal was five meetings each week, which allowed us to compress outreach into three months versus what would have normally taken a year as you fly back and forth to try and accommodate schedules.

Talking to so many folks helped me validate and hone the message for Cog with both our customers and potential investors. While I took the opportunity to experiment with unique angles at times, I quickly figured out what message hit the right notes for the right audience. Soon, the message (Monolithic to Modular) became the offer (We Secure IoT) and the offer became the solution (D4 Secure). It was messy at times and I floundered a bit, but I could always count on my fellow cohort members to lift me up to keep at it. Ultimately the process was illuminating and gratifying as we expanded our relationships in Silicon Valley and began to build awareness around our solution.

Comradery among my fellow mates was also a big part of the experience. Austrade loaded up the landing pad with other cybersecurity companies from Australia, plus six other non cyber-security companies.  The AustCyber Cohort was a great group, which was nice as we all spoke the same language. As the cohort had so much time together, we began to form a sense of community more out of necessity than choice. Though to do it again – I would tell you it was a choice all day long. Nothing was sacred among the cohort and no one was better than the other. These factors created a think tank-like atmosphere where we could share ideas, collaborate, learn, relate, all while stitching in comic relief.

Our partnership with SIEMonster was born as a result of this work environment. Together, we launched the Redback appliance utilizing Cog’s D4 Secure platform. This partnership provided the perfect foundation to set up both companies for success at RSA 2018 in April where we were named one of the “hottest cybersecurity products” by Peter Sayer, IDG News Service.

There were several key takeaways after this experience:

  1. We held 100+ meetings in 90 days as a result of being immersed in Silicon Valley.
  2. As an Australian company, we benefited from walking/living in someone else’s shoes. We now have a better understanding and can more effectively extend our company into this new market.
  3. The VC’s in Silicon Valley are very much focused on a ‘pay it forward’ approach. Even if they can’t help, they will ask how they can help. Call it karma – or as I like to say – it is just how they do business in the Valley.

As you know, Cog is an Australian company.  Everyone in the cohort was from an Australian company, as well.  Uniquely, I was the only Yank among all my Aussie mates in the cohort. This did require a pretty thick skin as one is not always sure when your mates are actually picking at all things American.  And, the U.S. and San Francisco bring plenty of fodder for commentary. However, I think it is important that we all note that only Australia has fought side by side with the Americans in every conflict going back 100 years.  We are true partner, allies, and friends. If there was nothing else to take from this experience, I will be forever grateful to be offered the chance to be an honorary Aussie for those 90 days.

Thank you to Austrade and AustCyber.