OSWebSec: Exokernels

From Soma-notes
Jump to navigation Jump to search


Key idea of Engler et al. in Exokernel: an operating system architecture for application-level resource managementp


Portability is a major concern with exokernels: In addition to the work required to port the exokernel to different hardware, you also have to port all programs to it since the exokernel provides a different API depending on what hardware it is running on.

The goal of exokernels was to make the system minimal, but at the end of the day you end up adding onto it and providing things like POSIX semantics anyway, and therefore introducing vulnerabilities into your system.

Extensibility is mentioned as a key advantage of exokernels, but modern OSs are quite extensible anyway: You can write kernel modules/device drivers, file systems, etc.

Exokernels for what?

The authors mention that many of the hardware abstractions offered by the kernel end up slowing down some specialized applications. But for a monolithic kernel this is no problem: You can just add APIs for specialized tasks to reduce overhead. So who exactly will go through all the pain of using an exokernel, when they can just take an open source OS like Linux and modify it to suit their needs?

Formal proof

The authors made some big compromises in order to make a formal proof for their exokernel possible:

  • They restricted themselves to a subset of the C language (e.g., no function pointers)
  • Gimped concurrency
  • Interrupt handling
  • Memory allocation (none)

They designed their kernel for uniprocessor systems. How do you verify a multi-threaded kernel? Even without verification, modern kernels took a lot of work to reach a state where they work correctly.


Microkernel subsystems depend on each other to get things done. There are too many tightly coupled services passing around too much data. Compromising one component can allow you to compromise others. Where's the win?

All optimizations that are done to improve microkernels can also be done to monolithic kernels. In class we discussed binder, an IPC system originally designed for microkernels, which has now been implemented for Linux and is used in Android.

Microkernels vs. Exokernels

Exokernels appear as hardware to the applications running on it, whereas microkernels provide abstractions.

Some barriers (e.g., user/kernel space) are natural, others aren't. If you try to create barriers where it doesn't make sense to do so, you simply end up breaking too many holes through them make things work correctly. From a security perspective, this brings you back to the same situation you started with because of all the holes that you've created.