Welcome

Welcome to the tutorial for the seL4 Microkit.

To complete this tutorial, you will need:

• A laptop or computer with access to the internet.
• Some familiarity with operating systems concepts and the C programming language.

Getting started

In this tutorial, you will be completing multiple exercises to end up with a system that implements the Wordle game. If you are not familiar with Wordle, it is a simple word guessing game. Through implementing the game, you will see how systems are constructed on seL4 using Microkit. This Wordle system, while largely a toy, does represent a realistic architecture as there is:

• a device driver (to allow the user to input a word)
• a trusted server (which has the secret word)
• an untrusted client (which guesses what the word is based on user input)

All of these are isolated components that then communicate via seL4 and Microkit.

But, before we can start the actual tutorial, you will have to go to part 0 to set up your machine.

License

This work is created by Ivan Velickovic and licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

Part 0 - Setting up your environment

This page covers two things:

1. Acquiring the Microkit SDK and the other dependencies needed for the tutorial.
2. Acquiring the tutorial code, so you can complete the exercises.

If you have any issues, feel free to open an issue on the GitHub repository.

Acquiring the dependencies

We have two options for working on the tutorial:

1. Install dependencies and do the tutorial natively, however this option is only available if you are doing the tutorial on Linux or macOS.

2. If you prefer to use Docker or are not on Linux/macOS, you can follow the instructions for Docker.

Option 1 - Native (Linux and macOS)

You'll need the following dependencies:

• Make
• AAarch64 cross compiler
• QEMU simulator for running the tutorials
• The Microkit SDK

Linux setup

On Ubuntu/Debian with apt you can use the following command:

sudo apt-get update && sudo apt-get install -y make gcc-aarch64-linux-gnu qemu-system-arm

On Arch Linux or other distributions that use pacman:

sudo pacman -Sy make aarch64-linux-gnu-gcc qemu-system-aarch64

On Fedora with dnf use the following command:

sudo dnf install -y make qemu gcc-aarch64-linux-gnu

You can get the SDK with:

# First make a directory for the tutorial
mkdir microkit_tutorial
cd microkit_tutorial
# Then download and extract the SDK
curl -L https://github.com/seL4/microkit/releases/download/1.4.0/microkit-sdk-1.4.0-linux-x86-64.tar.gz -o sdk.tar.gz
tar xf sdk.tar.gz

macOS setup

You can install the dependencies using Homebrew:

brew tap messense/macos-cross-toolchains
brew install make qemu aarch64-unknown-linux-gnu

For Apple Silicon (ARM64) Macs to get the SDK you can do the following:

# First make a directory for the tutorial
mkdir microkit_tutorial
cd microkit_tutorial
# Then download and extract the SDK
curl -L https://github.com/seL4/microkit/releases/download/1.4.0/microkit-sdk-1.4.0-macos-aarch64.tar.gz -o sdk.tar.gz
tar xf sdk.tar.gz

For Intel (x86) Macs to get the SDK you can do the following:

# First make a directory for the tutorial
mkdir microkit_tutorial
cd microkit_tutorial
# Then download and extract the SDK
curl -L https://github.com/seL4/microkit/releases/download/1.4.0/microkit-sdk-1.4.0-macos-x86-64.tar.gz -o sdk.tar.gz
tar xf sdk.tar.gz

Option 2 - Docker

seL4 provides an official Docker container which has the necessary dependencies for this tutorial. You can find instructions for acquring it here.

After setting up the Docker container, run the following commands outside Docker:

# First make a directory for the tutorial
mkdir microkit_tutorial
cd microkit_tutorial
# Then start the Docker container
container
# Then download and extract the SDK
curl -L https://github.com/seL4/microkit/releases/download/1.4.0/microkit-sdk-1.4.0-linux-x86-64.tar.gz -o sdk.tar.gz
tar xf sdk.tar.gz

This Docker image is mounted on your host file system. What that means is that the microkit_tutorial directory is accessible from both Docker and from your normal environment.

Run all the commands for downloading the tutorial code and building/running the tutorial in the container. You can then open the microkit_tutorial directory in your code editor for viewing/editing the tutorial code.

Getting the tutorial code

# Download and extract the tutorial code (in the microkit_tutorial directory)
curl -L trustworthy.systems/Downloads/microkit_tutorial/tutorial.tar.gz -o tutorial.tar.gz
tar xf tutorial.tar.gz

Now you can move on to part 1 of the tutorial.

Part 1 - Serial server

Since seL4 is a micro-kernel, a lot of functionality you would typically expect from a kernel is deliberately not implemented. One example of this is something as simple as outputting and inputting characters via a terminal. There are no write or read system calls like on Linux or macOS. While there is a way to output characters to the terminal via seL4, it is strictly for when debugging/developing.

This means that if we want to build a system like Wordle, which takes user-input and displays the game results via the serial connection, we first need a driver for the serial connection.

In this first part, you will learn all the pieces that go to make a driver on top of seL4. This driver will act as a "server" that clients (in this case the Wordle client) will send data to. The serial server then is the one actually talking to the serial device. The serial device that we will be using is called a Universal Asynchronous Receiver-Transmitter (UART).

Below is a diagram of what we will end up with by the end of this part¹:

Creating a serial server

System description example

In Microkit, you describe the architecture of the system you are building in a file we refer to as the "system description". This file is written in the XML format. Below is an example of a very simple "hello world!" system you could create. It contains a single protection domain that will print out "hello, world!" when it executes. You can see here we define a <protection_domain>, with the program image being some code that we have compiled to hello_world.elf.

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <protection_domain name="hello_world">
        <program_image path="hello_world.elf" />
    </protection_domain>
</system>

Before making our own system description, let's first understand what a protection domain actually is.

Protection Domains (PDs)

A protection domain is similar to a "process" on typical UNIX systems. However, by default a protection domain cannot do much except execute its code.

A protection domain is an abstraction created by Microkit and is made up of various seL4 primitives. The main ones are:

• A thread-control-block (TCB), because in order to actually have a thread of execution, seL4 needs to create a thread.
• A virtual address-space, known as a VSpace. This is what memory the kernel allows the PD to access. By default all that is in the VSpace is the ELF² of the PD, so it can execute its own code, and nothing else.
• A capability space, known as a CSpace. Each protection domain has its own CSpace which is a data structure that holds all the capabilities that a PD has access to.

As you can see, there is not lot a PD can actually do by default. And this is intentional. We do not want PDs to be able to access anything unless we explicitly allow it. This is allowed by the capability system, as all resources in seL4 are modelled by capabilities. If a PD does not have the capability to some resource, seL4 does not allow it to use it!

Entry points

Although a protection domain is somewhat analogous to a process, it has a considerably different program structure and life-cycle. A process on a typical operating system will have a main function which is invoked by the system when the process is created. When the main function returns the process is destroyed. By comparison a protection domain has three entry points: init, notified and, optionally, protected.

When a Microkit system is booted, all PDs in the system execute the init entry point, and then the Microkit library (libmicrokit) that each PD is linked with waits for events to come in. This diagram shows the control flow of a PD:

Here is a description of the protection_domain element:

• name: a unique name for the protection domain.
• pp: (optional) indicates that the protection domain has a protected procedure; defaults to false.
• priority: (optional) the priority of the protection domain (integer 0 to 254), defaults to 0 which is the lowest possible priority. The priority dictates which order PDs will run in. For example if there are two PDs that are both schedulable (i.e. are ready to run) then seL4 will run the higher priority one first.
• budget: (optional) the PD's budget in microseconds; defaults to 1,000.
• period: (optional) the PD's period in microseconds; must not be smaller than the budget; defaults to the budget.

Serial server protection domain

Now that you have some understanding of how protection domains work and are specified, your task is to:

• Edit the system description (wordle.system) to specify a protection domain for the serial server.
  • The name of the program image produced by the Makefile is serial_server.elf.
  • All values in the XML description are surrounded by quotes, for example, <protection_domain name="pd" priority="254" />.
• Since this PD is a server rather than a client, it should have a higher priority than the client.

Building

If we build part 1 and then look inside the build directory:

# Run these commands inside the "microkit_tutorial" directory
$ cd tutorial
# If you are working on native macOS, `make` may be installed as `gmake` instead.
$ make part1
$ ls build
serial_server.elf serial_server.o loader.img report.txt

We can see that when we run make part1, the file serial_server.c gets compiled into serial_server.elf. That is why the name of the program image in the system description file is serial_server.elf.

After compiling all the code, the microkit tool takes our ELFs and system description file and produces loader.img, a binary containing everything that we then give to QEMU to load.

The report.txt file contains details about the system that can be useful when debugging, but for this tutorial, you do not need to look at it.

Running

In order to actually run the system, we will be using the QEMU emulator which allows us to essentially create virtual hardware that we then run seL4 on.

You can emulate the system using the provided Makefile with:

make run

To exit QEMU, press CTRL + a then x.

qemu-system-aarch64 -machine virt,virtualization=on \
    -cpu cortex-a53 \
    -serial mon:stdio \
    -device loader,file=build/loader.img,addr=0x70000000,cpu-num=0 \
    -m size=1G \
    -nographic \
    -netdev user,id=mynet0 \
    -device virtio-net-device,netdev=mynet0,mac=52:55:00:d1:55:01

If you've done everything correctly, you should see the following output:

MON|ERROR: received message 0x00000006  badge: 0x0000000000000001  tcb cap: 0x8000000000000006
MON|ERROR: faulting PD: serial_server
MON|ERROR: Registers:
MON|ERROR: pc : 0x00000000002000e8
MON|ERROR: spsr : 0x0000000000000040
MON|ERROR: x0 : 0x0000000000000050
MON|ERROR: x1 : 0x0000000000000038
MON|ERROR: x2 : 0x0000000000000000
MON|ERROR: x3 : 0x0000000000000000
MON|ERROR: x4 : 0x0000000000000000
MON|ERROR: x5 : 0x0000000000000000
MON|ERROR: x6 : 0x0000000000000000
MON|ERROR: x7 : 0x0000000000000000
MON|ERROR: VMFault: ip=0x00000000002000e8  fault_addr=0x0000000000000038  fsr=0x0000000092000046  (data fault)
MON|ERROR:    ec: 0x00000024  Data Abort from a lower Exception level   il: 1   iss: 0x00000046
MON|ERROR:    dfsc = translation fault, level 2 (0x00000006) -- write not read

When we start the system we get a bunch of error printing, what has happened?

Remember that by default a protection domain does not have access to any memory other than its own code (as well as any global data and the stack region).

If we look at serial_server.c:

void init(void) {
    // First we initialise the UART device, which will write to the
    // device's hardware registers. Which means we need access to
    // the UART device.
    uart_init();
    // After initialising the UART, print a message to the terminal
    // saying that the serial server has started.
    uart_put_str("SERIAL SERVER: starting\n");
}

You will see that it tries to access the UART hardware when it calls uart_init(), which it doesn't have access to! What happens is that seL4 gets a "virtual memory fault" and delivers this to something called the monitor which then prints out the errors you are seeing with MON|ERROR. The monitor acts as the initial task and default fault-handler for Microkit.

So how do we prevent the virtual memory fault from happening? We need to give the serial server access to the UART.

Accessing the UART

Our serial driver will be useless unless it can actually access the UART device registers. We cannot just access the physical address of the UART device since the driver is a user-space program (Protection Domain) and so has its own virtual address space. This means we will need to map in the physical address into our PD's virtual address space. Microkit provides an abstraction for this, it is called "Memory Regions".

Memory Regions (MRs)

We can create memory regions at a specific physical address, or somewhere in RAM, that we can then map into the address space of whichever PD we want to have access to it. Here is a full description of the memory_region element which you would use to create a memory region:

• name: a unique name for the memory region.
• size: size of the memory region in bytes (must be a multiple of the page size).
• page_size: (optional) size of the pages used in the memory region; must be a supported page size if provided (4KiB or 2MiB on AArch64). By default it is 4KiB.
• phys_addr: (optional) the physical address for the start of the memory region.

In order to access the memory region from a PD, it needs to be mapped using the map element:

• mr: Identifies the memory region to map.
• vaddr: Identifies the virtual address at which to map the memory region to.
• perms: Identifies the permissions with which to map the memory region with. Can be any combination of r (read), w (write), and x (eXecute).
• cached: Determines if region is mapped with caching enabled or disabled. Defaults to true.
• setvar_vaddr: Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region.

Example

Here is an example of how the system description would look for a driver for a real time clock (RTC) device.

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <!-- Define a page sized region for accessing the "real-time clock" -->
    <memory_region name="rtc" size="0x1000" phys_addr="0x9010000" />

    <protection_domain name="timer_driver">
        <program_image path="timer_driver.elf" />
        <!--
            Map in the "rtc" region that corresponds to the physical address
            of the real time clock. The Microkit tool will set the value of
            the variable "rtc_base_vaddr" to the virtual address of the mapping
            when compiling the final `loader.img` image
         -->
        <map mr="rtc" vaddr="0x2000000" perms="rw" cached="false"
            setvar_vaddr="rtc_base_vaddr" />
    </protection_domain>
</system>

Mapping in the UART device

From reading the above example and referring to the description of the map and memory_region elements, you should be able to create the mapping to the UART for the serial server.

Note that:

• With QEMU, we'll be using a PL011 UART which has a physical address of 0x9000000.
• You only need to map in a single 4KiB page.
• Microkit places the code of a PD starting at 0x200000 in it's virtual address space. This means that the address to place the mapping for the UART should be below this, or significantly higher to avoid overlapping (e.g. 0x4000000) with the code of the PD.
• You can use setvar_vaddr to initialise a symbol in the code to the specified virtual address. The UART driver provided expects a uintptr_t uart_base_vaddr variable to be set to the virtual address of the UART mapping.
• Since we are doing memory mapped I/O, we do not want to enable caching on the mapping.

Your task now is to:

• Map in the UART to the serial server PD with both read and write permissions.
• Run the system and check to see if the SERIAL SERVER: starting appears.

Interrupt handling

An interrupt request (IRQ) is a signal from a hardware device (e.g. the UART serial device) that tells software that some event has happened. In the case of the UART device, every time we input a character, the device will deliver an interrupt to seL4. In seL4, it decodes the signal and then sends the interrupt as a notification to user-space. In our system we want this interrupt to go to the serial server so that it can handle the interrupt.

In the serial server code (serial_server.c) you will see the notified(microkit_channel ch) entry point. What we want to happen is that whenever we get an interrupt form the UART the notified entry point is executed. Then we can handle the interrupt and once notified finishes, the PD will go back to waiting to receive more events (such as more interrupts).

In the Microkit system description, we need to register these interrupts and associate them with a certain PD. This is because like with memory, IRQs are also modelled by capabilities meaning that we need to have the capability to a certain interrupt, before it can be delivered to a PD by seL4.

The irq element is a child element of protection_domain (just like program_image), and has the following attributes:

• irq: The interrupt number.
• id: The channel identifier, an integer from 0 to 62³.

The channel identifier is what's used by a PD to distinguish a particular interrupt from other interrupts or other notification sources. For example, if you had <irq id="0" irq="20" /> this would mean that whenever we get the interrupt number 20 from the hardware, the notified(microkit_channel ch) function will be entered, where the value of the ch parameter is 0.

Your task now is to:

• Specify the interrupt for serial input in the system description.
  • For the QEMU platform, the IRQ number is 33⁴.
• Inspect the serial server code (serial_server.c) and complete the notified entry point. When receiving the UART interrupt, do the following:
  1. Get the character that has been inputted via the keyboard with the int uart_get_char() function.
  2. Print out the character using the void uart_put_char(int ch) function.
  3. Call the function void uart_handle_irq() for the driver to handle the IRQ.
  4. The Microkit library function void microkit_irq_ack(microkit_channel ch), in order to acknowledge the IRQ.
     • Why do we need to acknowledge the IRQ? What this does is tell seL4 that we have finished handling the IRQ and are ready to receive another one. If we do not acknowledge it, we will never receive another UART IRQ again!

Now we can check to see that we are actually receiving interrupts. When you input a character, it should be printing as well. If that is working, you can move on to the next exercise.

Part 2 - Client

Now that we have a serial server working, our next goal will be to have a client PD that serves a command-line interface to play Wordle. For this we want to have a way for the client to retrieve characters from the serial server. A relatively simple way to do this is to share a buffer and have the serial server notify the client that there's a new character to read. We also want the client to be able to send characters for the serial server to output to the terminal. By the end of this part, we will have something like the following:

Your first task is to:

• Add a PD for the client to the system description. The name of the client's program image is client.elf.
  • Note that, as mentioned in part 1, the client should have a lower priority than the serial server.

Building

For building part 2, run the command:

make part2

Running

The same command from part 1 works:

make run

You should get the following output, indicating that the client has been successfully started:

SERIAL SERVER: starting
CLIENT: starting

The next step is to get the client and serial server communicating.

Channels

A channel allows two protection domains to interact with each other, either via notifications which are asynchronous and bidirectional, or, protected procedures which are synchronous and unidirectional. In this part of the tutorial, you'll be using notifications (protected procedures will be covered later).

When a channel is created between two PDs, a channel identifier is configured for each PD. The channel identifier is used by the PD to reference the channel. Each PD can refer to the channel with a different identifier. For example if PDs A and B are connected by a channel, A may refer to the channel using an identifier of 37 while B may use 42 to refer to the same channel.

The channel element has exactly two end children elements for specifying the two PDs associated with the channel.

The end element has the following attributes:

• pd: Name of the protection domain for this end.
• id: Channel identifier in the context of the named protection domain. The id is passed to the PD in the notified and protected entry points. The id should be passed to the microkit_notify function which allows you to notify the PD on the other end of the channel.

Example

Here is a basic example of two PDs using a channel to notify each other.

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <protection_domain name="sender">
        <program_image path="sender.elf" />
    </protection_domain>
    <protection_domain name="receiver">
        <program_image path="receiver.elf" />
    </protection_domain>

    <channel>
        <end pd="sender" id="1" />
        <end pd="receiver" id="2" />
    </channel>
</system>

The sender's code might look something like this:

#include <microkit.h>

#define RECEIVER_CHANNEL_ID 1

void init() {
    // Send a message to the receiver
    microkit_notify(RECEIVER_CHANNEL_ID);
}

The receiver's code might look something like this:

#include <microkit.h>

#define SENDER_CHANNEL_ID 2

void notified(microkit_channel ch) {
    // Receive a message from the sender
    switch (ch) {
        case SENDER_CHANNEL_ID:
            microkit_dbg_puts("Received message from sender!\n");
    }
}

void init() {}

Notice that the IDs of the channel are local to the PD. The sender refers to the channel with 2 but the receiver refers to the same channel with 1.

Your task now is to:

• Add the channel to the system description.
• You can make sure you have added the channel correctly by printing a message when the client gets notified from the serial server.
  • You can use either microkit_dbg_puts to print out a string or use printf for formatted strings. printf is just using microkit_dbg_puts behind the scenes anyways, but will be more convenient if you have to debug etc.

Shared buffer

Now that we can communicate between the client and serial server, the serial server has the ability to let the client know that it has received input. Since we cannot pass data via notifications, we will use a shared buffer, placing each new character in the buffer and subsequently notifying the client.

Example

If we wanted to have two PDs that share a buffer to avoid costly IPC to send data between the PDs, my system description might look something like this:

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <!--
        Define a page sized buffer to share between the "sender" and "receiver"
        protection domains.
    -->
    <memory_region name="shared_buffer" size="0x1000" />

    <protection_domain name="sender">
        <program_image path="sender.elf" />
        <!--
            Map the buffer into the address space of "sender", which only
            writes to it. The Microkit tool will do ELF symbol patching to set
            the virtual address of the mapping to a global variable called
            "buffer". The region is mapped as read-write as write-only mappings
            are not permitted by seL4 (at least on AArch64).
        -->
        <map mr="shared_buffer" vaddr="0x4000000" perms="rw" setvar_vaddr="buffer"/>
    </protection_domain>
    <protection_domain name="receiver">
        <program_image path="receiver.elf" />
        <!--
            Map the buffer into the address space of "receiver", which only
            reads from it. The Microkit tool will do ELF symbol patching to set
            the virtual address of the mapping to a global variable called
            "buffer".
        -->
        <map mr="shared_buffer" vaddr="0x4000000" perms="r" setvar_vaddr="buffer"/>
    </protection_domain>
</system>

Your task now is to:

• Create two shared buffers between the client and server. One buffer should handle user input, the other should handle output in order to display the game state.
• Be able to print out the characters received from the serial server in the client.
• Implement the serial_send function in the client to print out the game's interface.

Ultimately, you want to be able to get some output like this:

SERIAL SERVER: starting
CLIENT: starting
Welcome to the Wordle client!
[h] [e] [l] [l] [o]
[t] [h] [e] [r] [e]
[ ] [ ] [ ] [ ] [ ]
[ ] [ ] [ ] [ ] [ ]
[ ] [ ] [ ] [ ] [ ]

Pressing ENTER (\r) should move to the next line if they've entered enough characters. Similarly, you should be able to delete a character by pressing BACKSPACE.

Once you have that working, we can implement the Wordle server to get it to check whether we have a correct guess.

Part 3 - Wordle server

This part involves hooking up the client with a Wordle server PD. The Wordle server will accept attempted guesses of what the word is from the client, and will reply with what characters in the word were correct, incorrect, or correct but in the wrong position. At the end of this exercise, you should have a playable Wordle!

As mentioned in the previous part, there are two operations you can do using a channel, so far we have used notifications to asynchronously signal a PD that an event has occurred. With the Wordle server however, we want the semantics that the client requests the server to check the word that has been entered by the player, and returns a response with: what characters were correct, what characters were correct but in the wrong place, and what characters were incorrect.

To do this, we will use a synchronous method of communication, where the client will be blocked and waiting on the Wordle server for a response on each request.

Protected Procedure Calls (PPC)

A protection domain may provide a protected procedure (PP) which can be invoked from another protection domain. Up to 64 words of data may be passed as arguments when calling a protected procedure. The protected procedure return value may also be up to 64 words.

When a protection domain calls a protected procedure, the procedure executes within the context of the providing protection domain.

A protected procedure call is only possible if the callee has strictly higher priority than the caller. This means that if A has a priority of 1 and B has a priority of 254, A can invoke B's protected procedure, but B cannot invoke A's protected procedure. Transitive calls are possible, and as such a PD may call a protected procedure in another PD from a protected entry point. However the overall call graph between PDs forms a directed, acyclic graph. It follows that a PD can not call itself, even indirectly. For example, A calls B calls C is valid (subject to the priority constraint), while A calls B calls A is not valid.

When a protection domain is called, the protected entry point is invoked. The control returns to the caller when the protected entry point returns.

The caller is blocked until the callee returns. Protected procedures must execute in bounded time. Currently, the caller must trust the callee to conform.

To call a PP, a PD calls microkit_ppcall passing the channel identifier and a message structure, a message structure is returned from this function.

• To create a message structure, you can use microkit_msginfo microkit_msginfo_new(uint64_t label, uint16_t count). The label is typically used for distinguishing PPCs when a server has multiple services for a client to invoke. In this tutorial it will not be necessary to use the label and it can just be 0. The count will be used and it represents how many arguments (message-registers) are in the PPC.
• To set the arguments of a message (message registers), you can use void microkit_mr_set(uint8_t mr, uint64_t value) where mr is the index.
• To get arguments from the returned message, you can use uint64_t microkit_mr_get(uint8_t mr) where mr is the index.
• To get the label of a message, you can use uint64_t microkit_msginfo_get_label(microkit_msginfo msginfo);.

When a PD's protected procedure is invoked, the protected entry point is invoked with the channel identifier and message structure passed as arguments. The protected entry point must return a message structure.

Your task now is to:

• Add a Wordle server PD (using the program image wordle_server.elf).
• Add the ability to invoke the Wordle server's protected procedure from the client. This means creating a channel between the two PDs and setting pp="true" on the Wordle server's protection_domain element.
• On the client side, implement wordle_server_send to send the user-inputted word from the client to the Wordle server.
  • Do this using message registers by setting each character of the word from the client to the Wordle server.
• On the Wordle server side, implement the protected entry point microkit_msginfo protected(microkit_channel ch, microkit_msginfo msginfo).
  • Use the helper functions in wordle_server.c to put the state of each character in the same message-register that the character was delivered in.

Building

For building part 3, run the command:

make part3

Running

The same command from the previous parts works:

make run

Hopefully now you have the table printing with colour output (orange for correct letter wrong position, white for incorrect letter) and are able to guess the word! If all the letters are green, then you have won.

Part 4 - Virtual machines

Now that you have a playable Wordle, you will notice that the word to guess is always "hello" and does not change. That is a bit boring and not realistic.

The real Wordle game client works by having some server contain the word that changes every day. What if we could do something similar so that every time we start the game, we have to guess a new word? One way of doing this would be talking to some external server that picks a random word which the Wordle server receives.

This approach sounds complicated, and from part 1 you will know that in this tutorial we had to implement our own device driver just to be able to output characters to a screen. Talking to the internet would require an ethernet device driver which is non-trivial to create.

What if we wanted to have other more complicated systems? We would have to implement a lot of device drivers. For hardware like USB or Bluetooth, there would be hundreds of thousands of lines of code we would have to port from Linux or something else to get working on seL4.

However, there is a quicker and easier approach. We can run a virtual machine! ¹

In this part, you will be shown how to run a virtual machine running Linux using Microkit. We will make use of the ethernet driver that already exists in Linux to talk to a server trustworthy.systems/projects/microkit/tutorial/word that responds with a new five-letter word on every request.

If you do wget -qO- trustworthy.systems/projects/microkit/tutorial/word, you should see a new word each time you run the command.

Virtual machines on seL4

This diagram shows two main components involved when using virtual machines on top of seL4. Obviously there is a virtual machine (VM), but there is also a virtual machine monitor (VMM). The VMM is responsible for starting and managing the VM for its lifetime. As the VM doesn't necessarily know it is being virtualised and thinks that it is just running directly on hardware, it will try to perform operations such as memory read/write to regions of memory we do not want it to. Making these kinds of restrictions is well-suited to a capability system, as we can easily control exactly what resources the VM has power over.

In this case we want to give the VM access to the ethernet device, so we map the address of the device into the VM's virtual machine. This is typically called "pass-through" because, as you can see from the diagram, the VM bypasses both the VMM and seL4 when it accesses the device. This is ideal for performance as it means that the VMM nor seL4 consume any CPU when the VM is accessing the device.

However, interrupts are still managed through seL4 and the VMM. The reason for this is because we do not want the virtual machine to be able to mess with any other interrupts in the system, and most hardware architectures (such as ARM which we are using today) leave this problem up to software.

Integrating with the Wordle system

Our goal is to have a Linux virtual machine start that then gets the word from trustworthy.systems/projects/microkit/tutorial/word which it sends to the VMM for it to give to the Wordle server.

In Microkit it is possible to describe a VM using the virtual_machine element. It is very similar to a PD in that it has its own TCB, VSpace and CSpace.

There are a few pieces in order to create a VMM and VM in the system description, so I have given the description for you to copy-and-paste into your wordle.system. There are comments to help you understand all the pieces.

<!--
    This is what the virtual machine will use as its "RAM".
    Remember it does not know it is a VM and so it will expect a
    block of contigious memory as RAM.
-->
<memory_region name="guest_ram" size="0x10000000" page_size="0x200_000"
    phys_addr="0x40000000" />
<!-- Create a memory region for the ethernet device -->
<memory_region name="ethernet" size="0x1000" phys_addr="0xa003000" />
<!--
    Create a memory region for the GIC CPU interface. This is a device
    that is virtualised at the hardware-level, unlike other parts
    of the GIC.
-->
<memory_region name="gic_vcpu" size="0x1000" phys_addr="0x8040000" />

<!-- Create a VMM protection domain -->
<protection_domain name="vmm" priority="101">
    <program_image path="vmm.elf" />
    <!--
        Map in the virtual machine's RAM region as the VMM needs
        access to it as well for starting and setting up the VM.
    -->
    <map mr="guest_ram" vaddr="0x40000000" perms="rw"
        setvar_vaddr="guest_ram_vaddr" />
    <!--
        Create the virtual machine, the vCPU `id` is used for the
        VMM to refer to the VM. Similar to channels and IRQs.
    -->
    <virtual_machine name="linux" priority="100">
        <vcpu id="0" />
        <map mr="guest_ram" vaddr="0x40000000" perms="rwx" />
        <map mr="ethernet" vaddr="0xa003000" perms="rw" cached="false" />
        <map mr="uart" vaddr="0x9000000" perms="rw" cached="false" />
        <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" cached="false" />
    </virtual_machine>
    <!--
        We want the VMM to receive the ethernet interrupts, which it
        will then deliver to the VM.
     -->
    <irq irq="79" id="2" trigger="edge" />
</protection_domain>

Next, let's try build and run the system to see Linux booting.

Building

For building part 4, run the command:

make part4

Running

The same command from the previous parts works:

make run

When you run the system, you will see a lot more output than the previous parts, most of this is Linux's boot logs. At the bottom you should see the following (note that it may take a couple of seconds):

Starting network: OK
udhcpc: started, v1.35.0
udhcpc: broadcasting discover
udhcpc: broadcasting select for 10.0.2.15, server 10.0.2.2
udhcpc: lease of 10.0.2.15 obtained from 10.0.2.2, lease time 86400
deleting routers
adding dns 10.0.2.3
Linux user-space: Send request to trustworthy.systems/projects/microkit/tutorial/word
Linux user-space: Received word
Linux user-space: Transfer word to virtual-machine monitor
<<seL4(CPU 0) [decodeInvocation/645 T0x806000ac00 "child of: 'rootserver'" @200288]: Attempted to invoke a null cap #75.>>

What is happening here? Well after Linux boots it starts the initial task I have added a script that will automatically run and get the current Wordle word and copy it to the VMM. Surprisingly, it is a very simple script:

#!/bin/sh

# Establish internet connection
ifconfig eth0 up
udhcpc eth0

# Request the word
echo "Linux user-space: Send request to trustworthy.systems/projects/microkit/tutorial/word"
WORD=$(wget -qO- --no-check-certificate trustworthy.systems/projects/microkit/tutorial/word)
echo "Linux user-space: Received word"

# Need to go through each letter of the word
# and then write it to a location that the
# virtual machine monitor is expecting
echo "Linux user-space: Transfer word to virtual-machine monitor"
busybox devmem 0x50000000 w $(printf "%d" "'${WORD:0:1}")
busybox devmem 0x50000001 w $(printf "%d" "'${WORD:1:2}")
busybox devmem 0x50000002 w $(printf "%d" "'${WORD:2:3}")
busybox devmem 0x50000003 w $(printf "%d" "'${WORD:3:4}")
busybox devmem 0x50000004 w $(printf "%d" "'${WORD:4:5}")
echo "Linux user-space: Finished"

Once we have the word, we simply transfer it character-by-character to the VMM using a tool that lets us write to a physical address (physical address from the virtual machine's point of view). Since the characters are being written to memory that the VM does not have access to, this will cause a virtual memory fault which seL4 gives to the VMM to handle. You will notice that this is not particularly efficient, especially if we were doing this process with large amounts of data. Fortunately, other methods such as the virtIO standard exist. But for this tutorial, that is out of scope.

If we look at the last line of the system:

<<seL4(CPU 0) [decodeInvocation/645 T0x806000ac00 "child of: 'rootserver'" @200288]: Attempted to invoke a null cap #75.>>

What is happening is that the VMM is trying to perform a PPC to send the word to the Wordle server. However, as we do not have a channel, we are trying to invoke a channel (and hence a capability) that does not exist! Hence the seL4 error print.

We can easily fix this by creating a channel between the VMM and the Wordle server:

<channel>
    <!-- The VMM code expects the channel ID to be 1. -->
    <end pd="vmm" id="1" />
    <end pd="wordle_server" id="2" />
</channel>

Finally, we need to add code in wordle_server.c in order to handle the PPC from the VMM. We can look at how the VMM is transferring the word here:

microkit_msginfo msg = microkit_msginfo_new(0, WORDLE_WORD_SIZE);
for (int i = 0; i < WORDLE_WORD_SIZE; i++) {
    microkit_mr_set(i, word[i]);
}
microkit_ppcall(WORDLE_SERVER_CHANNEL, msg);

It is simply setting each character in one of the message-registers. So in the Wordle server you can read each message-register using uint64_t microkit_mr_get(uint8_t mr) to update the word array from being equal to "hello" to our new word.

After doing that and re-running the system, you should see the message Linux user-space: Transfer word to virtual-machine monitor. Hit the RETURN key then you should see the client interface printing again. You can now guess the secret word! If you do not want to guess, you can instead print out the word in the Wordle server :).

End

This is the end of the tutorial. Thank you for taking to the time to complete it, I hope you found it enjoyable and you learnt something!

If you have any questions or feedback, feel free to open an issue on the GitHub repository.

Useful links

• seL4 homepage
• Trustworthy Systems homepage
• seL4 source code
• Microkit source code
• Experimental virtual-machine-monitor used in part 4

Solutions

The solutions are available for download from here.

Alternatively you can download them via:

# Make sure to run these commands in the microkit_tutorial directory created in part 0
curl -L trustworthy.systems/Downloads/microkit_tutorial/solutions.tar.gz -o solutions.tar.gz
tar xf solutions.tar.gz

To build the solutions do:

cd solutions
make part4

To run the solutions do:

make run