The EwoK microkernel

ewok icon

What is Ewok ?

EwoK is a microkernel targeting micro-controllers and embedded systems. It aims to bring an efficient hardening of embedded devices with a reduced impact on the device performances.

EwoK has been designed to host complex drivers in userspace. Unlike most of other microkernels, the goal is to support complex software stacks (ISO7816, …) as well as high performance (USB, SDIO, CRYP) drivers. This makes EwoK valuable for multiple use cases, including high speed and security targeted devices.

Security properties

EwoK supports the following properties:
  • Strict memory partitioning
  • Strict partitioning of physical resources (devices, etc.)
  • Fixed permissions management, set at compile time and easily verifiable
  • Stack smashing protection (at kernel level, work in progress at userspace level)
  • Heap/Stack smashing protection
  • W⊕X memory mappings
  • Strict temporal separation between declarative phase and execution phase

Ewok provides to the userspace drivers a specific interface to allow them to use the DMA engines. It permits to achieve high performance, specifically with high speed buses.

Nevertheless, DMA registers are never directly accessible to user tasks and any DMA configuration implies a validation of all the inputs by the kernel before any modification of the controller is pushed at the hardware level.

EwoK architecture

Kernel architecture

The Ewok kernel is divided into two main components: the libbsp and the kernel part.

Ework kernel architecture

The libbsp is the hardware abstraction layer, hosting all the low level and arch-specific drivers (MPU, GPIOs, timers, DMAs, etc.). The libbsp is itself separated in two blocks:

  1. SoC-specific drivers, such as DMA or GPIO support for the STM32F407 board
  2. Core-specific drivers, such as MPU support for the Cortex-M4 ARMv7m micro-architecture

The kernel part contains all specific high level content (scheduling, task management, syscalls, etc.) and uses the libbsp as a hardware abstraction for any low-level interaction.

Drivers architecture

Ework generic software architecture

The libstd is the only requested userspace library. libstd hosts the syscall user part (i.e. abstraction of the svc, aka supervisor call, assembly instruction) and some general purpose utility functions such as libstring and logging utility functions such as printf (see Technical documents).

The drivers are written as userspace libraries. They depend on the libstd, and may sometimes depend on each others. Here is the list of the existing drivers:

  • libusart, a userpace STM32 U(S)ART implementation

Libraries are various userspace features, arch-independent implementations. The current userspace libraries are:

  • libconsole, a serial console abstraction, based on libusart

Note

Other drivers and libraries will be published regulary

About the chosen programming languages

Most of microkernels have been written in C and assembly. Some use less error-prone languages such as Rust, and only a very few have been formally validated (SeL4, written in C and formally validated using Isabelle) or ProvenCore (using its own formal language).

Ewok is based on the following considerations:
  • A fully formalized microkernel is too costly for an Open-Source project
  • A C-based microkernel is clearly too error-prone and even with high level of compilation hardening and tests, C language is not that adapted to very low level safe development (no strict typing, unsafe bitfields management, too many compiler dependent behavior, etc.). Nevertheless, C is still a language highly understood by most of the developers community.

We first have implemented an EwoK prototype in full C with few Assembly. Then, to limit the risk associated with the C language, we have decided to replace all the safety critical or security critical part of the kernel by Ada and SPARK. Nevertheless, we have not deleted the corresponding C part but modified the compilation system to support file by file substitution between C and Ada reference implementations.

EwoK can then be compiled as a full C/ASM kernel or an hybrid Ada/SPARK - C/ASM kernel, reducing the C and ASM part to the most basic and easy part of the kernel. Any component requiring external inputs (like syscalls) or critical for the security (like memory management) is written in Ada or SPARK, depending on the level of formalism required.

Note

The Ada/SPARK kernel is based on about 10 Klines of Ada and about 500 lines of C and assembly.

The methodology we used to create an hybrid kernel is described in the following sections:

EwoK API

The EwoK API is tuned for embedded systems, targeting userspace drivers implementation with performance and security constraints in mind. The whole microkernel architecture and the API provided to the user tasks are specifically designed for such a purpose.

Note that despite being a microkernel, Ewok is not full-IPC driven like L4 family microkernels. Beyond this, and similarly to other kernels, EwoK interactions with the userspace are based on syscalls. In the particular case of EwoK, a main application has two execution contexts: standard thread mode and ISR thread mode. Some syscalls can be executed from any context while others cannot. This property is described in each syscall documentation, and the developer will have to refer to it and understand in which context a piece of code is executed before calling such a syscall.

Some syscalls require some specific permissions. Those permissions are statically defined (set at build time).

The EwoK API is fully described in the following:

EwoK API FAQ

General FAQ

Why applications main function is named _main?

EwoK applications entry points have the following prototype:

int function(uint32_t task_id):

There is an unsigned int argument passed to the main function, giving it the current task identifier.

When using the main symbol, the compiler requires one of the following prototypes:

int main(void);
int main(int argc, char **argv);

As EwoK doesn’t generate such a prototype, the main symbol cannot be used, explaining why _main is used instead. The generated ldscript automatically uses it as the application entry point and the application developer has nothing to do other than to name its main function properly.

What is a typical generic task’s main() function?

A basic main function should have the following content:

  • An initialization phase
  • A call to sys_init(INIT_DONE) to finish the initialization phase
  • A nominal phase

A basic, generic main function looks like the following:

int _main(uint32_t task_id)
{
  /* Local variables declaration */
  uint8_t syscall_ret;

  /* Initialization phase */
  printf("starting initialization phase\n");

  /* any sys_init call is made here */

  /* End of initialization sequence */
  sys_init(INIT_DONE);

  /* Nominal sequence */
  printf("starting nominal phase\n");

  /*
   * If any post-init configuration is needed, do it here
   * This is the case if memory-mapped devices need to be configured
   */

  /*
   * Start the main loop or main automaton
   */
  do_main_loop();

  return 0;
}

Syscall API is complex: why?

EwoK syscalls is a fully driver-oriented API. Efforts have been put in providing various userspace abstractions to help application developers in using generic devices through a higher level API.

These abstractions are separated in:

  • userspace drivers
    These drivers supply a higher level, easier API to applications and manage a given device by using the syscall API and configuring the corresponding registers for memory-mapped devices. Drivers API abstract most of the complexity of the hardware devices (such as USARTs, CRYP, USB, SDIO, etc.)
  • userspace libraries
    These libraries implement various hardware-independent features, but may depend on a given userspace driver. They supply a functional API for a given service (serial console, AES implementation, etc.), and in case of a dependency with a userspace driver, manage the driver initialization and configuration.

Syscalls FAQ

What is the header to include to get the syscalls prototypes?

Syscalls are implemented as functions in userspace, in the libstd. The header is syscalls.h.

When I declare a device, I always get SYS_E_DENIED?

Denying may be the consequence of various causes:
  1. You are not in the initialization phase
  2. You don’t have the permission to register this type of device (see EwoK permissions)
  3. If you use EXTI for one or more GPIO, you must have the corresponding permission
  4. If you require a forced execution of the main thread for one more more ISR, you must have the corresponding permission
  5. You have left a field unconfigured with a value that means something not permitted in your case (for example EXTI access request for GPIO)

Hint

It is a good idea to memset to 0 a device_t structure before configuring it and requesting a device to the kernel.

When I configure a device, I always get SYS_E_INVAL?

Returning invalid may be the consequence of various causes:
  1. Your device_t structure contains some invalid (unset) field(s). When using the Ada kernel, be sure to memset to 0 the structure before using it, the kernel is very strict with the user entries (for obvious security reasons)
  2. You try to map a device that is not in the supported device map (see EwoK device map for information)
  3. You try to map a device with an invalid size (see EwoK device map for information)
  4. You have set more IRQ or more GPIOs than the maximum supported in the device_t structure (see EwoK kernel API for information)

Hint

It is a good idea to memset to 0 a device_t structure before configuring it and requesting a device to the kernel, and highly recommended when using the Ada kernel

Permissions FAQ

When using a library or a driver, are specific permissions required?

There is no permission needed to link to a given userspace library or driver, but they may require one ore more permission to work properly.

For example, the libconsole (managing a userspace serial console) requires the Devices/Buses permission in order to use the libusart and configure the specified U(S)ART correctly.

Each driver and library should have its required permissions specified in its documentation page.

Libstd API

Are there helper functions to manipulate registers in userspace?

Yes! A lot of helper functions and macros have been written to help interacting with registers. This API is in the libstd regutils.h header. Applications can include this header directly in order to use it.

Ewok Security

Why flash is mapped RX and not Execute only for both user and kernel?

This is a constraint due .rodata (read only data sections).

Since .rodata must be readable, executable code and such data have to live together in the same flash area. Using different MPU regions to split them would have required too much MPU regions (and the number of regions is very constrained by the hardware unit).

Another solution would be to copy .rodata content into RAM, but this suffers from the same MPU limitations issues, with the additional drawback of reducing the available task volatile memory.

Is the W⊕X principle supported?

The EwoK kernel enforces the W⊕X mapping restriction principle, which is a strong defense in depth mitigation against userland exploitable vulnerabilities.

Moreover, the Ada kernel integrates SPARK proofs that verify at that there is no region that can be mapped W and X at the same time.

EwoK build process

When I switch between C-based and Ada-based kernels, the compilation is not performed?

When changing the compilation mode of the kernel, the $(OBJS) objects files list of the kernel is modified to point to the Ada (or C) object files. As a consequence, the clean target does not do its work properly as its variables has changed. To be sure to rebuild the kernel in the other language, you can either:

  • delete the kernel/ dir from the build directory
  • execute a make distclean before calling the defconfig
  • remove the build directory manually