CAmkES VMM

camkes-vm-apps

This project is for running virtualised Linux guests on seL4 for ARM and x86 platforms. The camkes-vm implements a virtual machine monitor (VMM) server, facilitating the initialisation, booting and run-time management of a guest OS. You can view the code for the VMMs in the camkes-vm repository under VM_Arm and VM.

Currently the supported platforms include:

• Exynos5 (exynos5410, exynos5422)
• TK1
• TX1
• TX2
• QEMU ARM virt machine
• ZCU102
• x86
• x86_64

Getting and Building

Cloning the repository set and preparing a build directory

repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git
repo sync
mkdir build
cd build

Arm and x86 have slightly differing build instructions. See the sections below.

Building for Arm

The following example builds the CAmkES Arm VMM for the TK1. In the build directory, run:

../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1
ninja

Note: To buid for another platform you can substitute the value of the -DPLATFORM variable e.g. (exynos5422, tx1, tx2, zcu102, qemu-arm-virt)

An EFI application file will be left in images/capdl-loader-image-arm-tk1 We normally boot using TFTP, by first copying capdl-loader-image-arm-tk1 to a tftpserver then on the U-Boot serial console doing:

dhcp
tftpboot ${loadaddr} /capdl-loader-image-arm-tk1
bootefi ${loadaddr}

Building for x86

The following example builds the CAmkES VMM for x64. In the build directory, run:

../init-build.sh -DCAMKES_VM_APP=minimal_64
ninja

Boot images/kernel-x86_64-pc99 and images/capdl-loader-image-x86_64-pc99 with the multiboot boot loader of your choice. Use *.ia32-pc99 if built for 32-bit with ../init-build.sh -DCAMKES_VM_APP=minimal.

CAmkES ARM VMM Applications

This project contains various reference CAmkES applications that incorporate the VMM component. These applications include:

• vm_minimal: A simple VMM application, launching a single guest Linux with a buildroot RAM-based file system
• vm_cross_connector: Application demonstrating communication between a Linux guest user-level process and a native seL4 component. This leveraging cross vm communication channels established between the VMM and the seL4 component.
• vm_multi: Application demonstrating running multiple guest VM’s. This is achieved through having multiple VMM components, each managing a single Linux guest (1-1 model).
• vm_serial_server: Application demonstrating the use of Virtio Console, where a VM’s serial I/O is forwarded to/from a serial server.
• vm_virtio_net: Application demonstrating the use of Virtio Net, where a virtual network interface is presented to a VM and subsequent network traffic on the virtual network interface is sent to/from other native seL4 components.

See the apps/Arm/ subdirectory for all the supported virtual machine manager apps, their implementations and the platforms they target.

CAmkES x86 VMM Applications

• The minimal application is a simple CAmkES VM application. The application is configured with:

  • 1 Guest Linux VM: The Linux guest is a buildroot built image sourced from the the camkes-vm repo. The Linux images (rootfs and kernel) are defined in the CMakeLists.txt file of the minimal application. In the CMakeLists.txt file we are able to find that the rootfs and kernel images are added to the FileServer under the names "rootfs.cpio" and "bzimage" respectively.

• The optiplex9020 VM application is configured with:

  • 2 Guest Linux VM’s: The Linux guests are buildroot built images sourced from the the camkes-vm repo.

  • Cross VM Connectors: To demo the use of cross-vm connectors a series of shared dataports and events are established between vm0 and the StringReverse component. The StringReverse demo can be invoked from the command-line of vm0:

    Welcome to Buildroot
    buildroot login: root
    Password:
    \# string_reverse
    [   19.739028] dataport received mmap for minor 1
    [   19.743337] dataport received mmap for minor 2
    hello
    olleh
    

• The cma34cr_centos application is a more complex CAmkES VM configuration demonstrating the use of passthrough hardware. The cma34cr_centos application is configured with:

  • 1 Guest Linux VM: The Linux guest images (bzimage and roofs.cpio) are located in the applications directory (cma34cr_centos/centos_linux), originally sourced from an i386 altarch CentOS-7 installation. Additionally the CentosOS installation should be on a flash drive passed-through to the cma34cr application. Further information regarding the Linux installation can be found in the applications README.
  • Cross VM Connectors: A series of shared dataports and events are established between vm0 and the StringReverse component.
  • Ethernet Driver, UDPSever, Echo, Firewall: A passthrough ethernet configuration demo. The guest VM is configured to use the Ethernet driver component through a virtio configuration.
  • Passthrough hardware storage (SATA/USB): A hardware configuration to boot the CentOS installation.

• The zmq_samples application demonstrates messaging between VMs using the ZeroMQ messaging library. See the README.md in its folder for more information.

See the apps/x86/ subdirectory for all the supported virtual machine manager apps, their implementations and the platforms they target.

Arm Features

See the below feature matrix for the various features the CAmkES ARM VMM implements/facilitates across the various supported platforms.

Arm Platform Configuration Notes

Exynos5422, TX1, TX2, ZCU102, QEMU ARM Virt configuration

We provide a pre-built Linux image and Buildroot image for our guest VM’s. See the images in the camkes-vm-images repository at https://github.com/sel4/camkes-vm-images. Feel free also to compile your own Linux and Rootfs images, see the README’s in each platform subdirectory (within camkes-vm-images) for information about our image build configurations.

TK1 configuration

We currently provide two linux binaries and two device tree configurations.

• linux-tk1-debian will try and load a debian userspace off of an emmc partition
• linux-tk1-initrd will load an included buildroot ramdisk
• linux-tk1-secure.dts is a device tree configuration with the devices that aren’t provided to the linux are disabled.
• linux-tk1-nonsecured.dts is a device tree configuration with all devices enabled.

In the tk1 app configuration there is a boot mode selection option that chooses between the two linux binaries, and an Insecure option which selects whether to provide all hardware devices to the linux vm or not. If Insecure is not set then the VM will only be provided a minimal amount of hardware frames and the linux-tk1-secure.dts DTS will be used. If Insecure is set then the VM will be provided all device frames apart from the Memory controller and the linux-tk1-nonsecured.dts DTS will be used.

U-Boot is required to initialise the USB devices if linux-tk1-secure.dts is used. This is done by: usb start 0.

The tk1 currently uses linux binaries constructed using Buildroot 2016.08.1 with the following configs:

• buildroot_tk1_initrd_defconfig builds linux with an included ramdisk that will be loaded at boot.
• buildroot_tk1_emmc_defconfig builds linux without a ramdisk and it will mount and run /sbin/init /dev/mmcblk0p2

To copy the files back into this project, change into the Linux directory and run make for each file as shown below. Note that you can only update one of linux-tk1-debian or linux-tk1-initrd at a time as they are built from different Buildroot configs:

cd projects/vm/linux
LINUX_FILE=linux-tk1-initrd BUILDROOT_DIR=~/workspaces/buildroot-2016.08.1/ make
LINUX_FILE=linux-tk1-dtb-secure BUILDROOT_DIR=~/workspaces/buildroot-2016.08.1/ make

Both of these configs use the tegra124-jetson-tk1-sel4vm-secure device tree file. To change to the tegra124-jetson-tk1-sel4vm.dts this will need to be changed in the buildroot make menuconfig. To change the mounted emmc partition the chosen dts file’s bootargs entry will need to be updated.

The Linux version used can be found in the seL4 branch of our linux-tegra repo.

When buildroot starts:

buildroot login: root
#

When debian starts:

Debian GNU/Linux 8 tk1 ttyS0
tk1 login: root
Password: root
root@tk1:~#

Wireless Configuration

To configure the Ralink 2780 USB wifi dongle:

ifconfig wlan0 up
iw wlan0 scan
wpa_passphrase SSID_NAME >> /etc/wpa_supplicant.conf
  ENTER_SSID_PASSPHRASE
wpa_supplicant -B -i wlan0 -c /etc/wpa_supplicant.conf
iw wlan0 link
dhclient wlan0

TK1 Build Notes

The default setup does not pass though many devices to the Linux kernel. If you make menuconfig you can set insecure mode in the Applications submenu; this is meant to pass through all devices, but not everything has been tested and confirmed to work yet. In particular, the SMMU needs to have extra entries added for any DMA-capable devices such as SATA.

Useful Links for Developing VM Applications

1. CAmkES VM: Adding a Linux Guest
2. CAmkES VM: Cross VM Connectors

Arm FAQ and Implementation Notes

How do I update camkes-vm-apps to support platform ‘X’

Whilst large parts of the ARM VMM implementation tries to be platform agnostic, there are a few things to keep in mind and implement in order to correctly run the camkes-arm-vm on your new target platform. See the below list as as a rough list of items to check off:

• Ensure the platform is already supported by seL4 (or you have developed support for the platform prior). See the following page for a list of supported platforms.
• The platform supports ARM’s hardware virtualisation features, these being found on ARMv7 (with virtualisation extensions) and ARMv8.
  • Second to this, the seL4 port to the given platform also supports running with KernelArmHypervisorSupport
• Does your platform use a GICv2 or GICv3? Note: We currently only support a virtual GICV2, with virtual GICV3 support under-development. See the listed features of libsel4vm for further information: https://github.com/sel4/seL4_projects_libs/tree/master/libsel4vm
• When porting a VMM application to your platform, say vm_minimal, ensure you provide the following:
  • A devices.camkes file for your platform. These containing platform specific definitions, see in particular the vm dtb field and the untyped_mmios field (for device passthrough). The values in the aforementioned fields corresponding with those found in the kernel device tree.
  • A vmlinux.h header for you platform. See the header file for the other supported platforms at components/VM_Arm/plat_include in camkes-vm repository.
• Provide a pre-compiled Linux kernel and initrd image for your platform. Once compiled these are usually linked in through your apps CMakeLists.txt. See apps/Arm/vm_minimal/CMakeLists.txt for examples of how other platforms link in their images.

Feel free to contact the team for further support on porting the camkes-arm-vm to your desired platform. We are also always open to contributions for new platforms.

Can a single VMM component support running multiple VM’s?

Currently, No. A VMM component only creates and manages a single VM instance. To support multiple VM’s, you can run multiple VMM components, each managing its own VM. See apps/vm_multi for an example of this configuration.

How do I enable SMP support for a VM instance?

To configure your VM with multiple VCPU’s, you can set the VM instance attribute num_vcpus in your camkes configuration. See here for an example. In addition, when initialising your build, ensure the KernelMaxNumNodes configuration option is set to your desired value. You can also initialise your build with variable -DNUM_NODES variable e.g.

../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx2 -DNUM_NODES=4

Note: ensure your platform supports SMP configurations through the above feature matrix

File included from github repo edit

CAmkES x86 VM

Prerequisites

• Get the dependencies for building CAmkES by following the instructions here
• Your host machine has to have a CPU that supports Vt-x virtualization (for Intel CPUs), or AMD-V (for AMD CPUs, but that wasn’t tested). Any newer i7 core should have Vt-x. Note that you might have to enable it first from BIOS. You can always check by lscpu and look for vmx flag.

Tutorials

Use the following tutorials to learn about the VM:

1. Camkes VM Linux using Linux as a guest in the Camkes VM.
2. Camkes Cross-VM communication walkthrough of adding communication between Linux guests in separate VMs.

Examples

• Centos
• zmq_samples

Booting from hard drive

These instructions are for ubuntu. For CentOS instructions, see CAmkESVMCentOS.

So far we’ve only run a tiny linux on a ram disk. What if we want to run Ubuntu booting off a hard drive? This section will explain the changes we need to make to our VM app to allow it to boot into a Ubuntu environment installed on the hard drive. Thus far these examples should have been compatible with most modern x86 machines. The rest of this tutorial will focus on a particular machine: the cma34cr single board computer

The first step is to install ubuntu natively on the cma34cr. It’s currently required that guests of the camkes vm run in 32-bit mode, so install 32-bit ubuntu. These examples will use ubuntu-16.04.

The plan will be to give the guest passthrough access to the hard drive, and use a ubuntu initrd as our initial root filesystem, replacing the buildroot one used thus far. We’ll use the same kernel image as before, as our vm requires that PAE be turned off, and it’s on by default in the ubuntu kernel.

Getting the initrd image

We need to generate a root filesystem image suitable for ubuntu. Ubuntu ships with a tool called mkinitramfs which generates root filesystem images. Let’s use it to generate a root filesystem image compatible with the linux kernel we’ll be using. Boot ubuntu natively on the cma34cr and run the following command:

$ mkinitramfs -o rootfs.cpio 4.8.16
WARNING: missing /lib/modules/4.8.16
Ensure all necessary drivers are built into the linux image!
depmod: ERROR: could not open directory /lib/modules/4.8.16: No such file or directory
depmod: FATAL: could not search modules: No such file or directory
depmod: WARNING: could not open /var/tmp/mkinitramfs_H9SRHb/lib/modules/4.8.16/modules.order: No such file or directory
depmod: WARNING: could not open /var/tmp/mkinitramfs_H9SRHb/lib/modules/4.8.16/modules.builtin: No such file or directory

The kernel we’ll be using has all the necessary drivers built in, so feel free to ignore those warnings and errors. You should now have a file called rootfs.cpio on the cma34cr. Transfer that file to your dev machine, and put it in projects/vm/minimal. Now we need to tell the build system to take that rootfs image rather than the default buildroot one. Edit projects/vm-examples/minimal/CMakeLists.txt. Change this line:

AddToFileServer("rootfs.cpio" ${rootfs_file})

to

AddToFileServer("rootfs.cpio" <ROOTFS_FILENAME>)

where <ROOTFS_FILENAME> is replaced with the filename of the rootfs file you added in projects/vm/minimal.

Since we’ll be using a real hard drive, we need to change the boot command line we give to the guest linux. Open projects/vm-examples/minimal/minimal.camkes, and change the definition of VM_GUEST_CMDLINE to:

#define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/sda1 rdinit=/init 2"

Try building and running after this change:

BusyBox v1.22.1 (Ubuntu 1:1.22.0-15ubuntu1) built-in shell (ash)
Enter 'help' for a list of built-in commands.

(initramfs)

You should get dropped into a shell inside the root filesystem. You can run commands from here:

(initramfs) pwd
/
(initramfs) ls
dev      run      init     scripts  var      usr      sys      tmp
root     sbin     etc      bin      lib      conf     proc

If you look inside /dev, you’ll notice the lack of sda device. Linux can’t find the hard drive because we haven’t passed it through yet. Let’s do that now!

We’re going to give the guest passthrough access to the sata controller. The sata controller will be in one of two modes: AHCI or IDE. The mode can be set when configuring BIOS. By default it should be AHCI. The next part has some minor differences depending on the mode. I’ll show both. Open projects/vm-examples/minimal/minimal.camkes and add the following to the configuration section:

For AHCI:

configuration {
    ...

    vm0_config.pci_devices_iospace = 1;


    vm0_config.ioports = [
        {"start":0x4088, "end":0x4090, "pci_device":0x1f, "name":"SATA"},
        {"start":0x4094, "end":0x4098, "pci_device":0x1f, "name":"SATA"},
        {"start":0x4080, "end":0x4088, "pci_device":0x1f, "name":"SATA"},
        {"start":0x4060, "end":0x4080, "pci_device":0x1f, "name":"SATA"},
    ];
    
    vm0_config.pci_devices = [ 
        {   
            "name":"SATA",
            "bus":0,
            "dev":0x1f,
            "fun":2,
            "irq":"SATA",
            "memory":[
                {"paddr":0xc0713000, "size":0x800, "page_bits":12},
            ],
        },  
    ];

    vm0_config.irqs = [ 
        {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11},
    ];
}

For IDE:

configuration {
    ...

    vm0_config.pci_devices_iospace = 1

    vm0_config.ioports = [ 
        {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"},
        {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"},
        {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"},
        {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"},
        {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"},
        {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"},
    ];  

    vm0_config.pci_devices = [ 
        {   
            "name":"SATA",
            "bus":0,
            "dev":0x1f,
            "fun":2,
            "irq":"SATA",
            "memory":[],
        },  
    ];  

    vm0_config.irqs = [ 
        {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11},
    ];
}

Now rebuild and run:

Ubuntu 16.04.1 LTS ertos-CMA34CR ttyS0

ertos-CMA34CR login: 

You should be able to log in and use the system largely as normal.

Passthrough Ethernet

The ethernet device is not accessible to the guest:

$ ip addr
1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue state UNKNOWN group default qlen 1
    link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00
    inet 127.0.0.1/8 scope host lo
       valid_lft forever preferred_lft forever
    inet6 ::1/128 scope host 
       valid_lft forever preferred_lft forever
2: sit0@NONE: <NOARP> mtu 1480 qdisc noop state DOWN group default qlen 1
    link/sit 0.0.0.0 brd 0.0.0.0

An easy way to give the guest network access is to give it passthrough access to the ethernet controller. This is done much in the same way as enabling passthrough access to the sata controller. In the configuration section in projects/vm-examples/minimal/minimal.camkes, add to the list of io ports, pci devices and irqs to pass through:

vm0_config.ioports = [
    {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"},
    {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"},
    {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"},
    {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"},
    {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"},
    {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"},
    {"start":0x3000, "end":0x3020, "pci_device":0, "name":"Ethernet5"}, // <--- Add this entry
];

vm0_config.pci_devices = [
    {   
        "name":"SATA",
        "bus":0,
        "dev":0x1f,
        "fun":2,
        "irq":"SATA",
        "memory":[],
    },

    // Add this entry:
    {
        "name":"Ethernet5",
        "bus":5,
        "dev":0,
        "fun":0,
        "irq":"Ethernet5",
        "memory":[
            {"paddr":0xc0500000, "size":0x20000, "page_bits":12},
            {"paddr":0xc0520000, "size":0x4000, "page_bits":12},
        ],
    },
];

vm0_config.irqs = [
    {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11},
    {"name":"Ethernet5", "source":0x11, "level_trig":1, "active_low":1, "dest":10}, // <--- Add this entry
];

You should have added a new entry to each of the three lists that describe passthrough devices. Building and running:

$ ip addr
1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue state UNKNOWN group default qlen 1
    link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00
    inet 127.0.0.1/8 scope host lo
       valid_lft forever preferred_lft forever
    inet6 ::1/128 scope host 
       valid_lft forever preferred_lft forever
2: enp0s2: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc pfifo_fast state UP group default qlen 1000
    link/ether 00:d0:81:09:0c:7d brd ff:ff:ff:ff:ff:ff
    inet 10.13.1.87/23 brd 10.13.1.255 scope global dynamic enp0s2
       valid_lft 14378sec preferred_lft 14378sec
    inet6 2402:1800:4000:1:90b3:f9d:ae22:33b7/64 scope global temporary dynamic 
       valid_lft 86390sec preferred_lft 14390sec
    inet6 2402:1800:4000:1:aa67:5925:2cbc:928f/64 scope global mngtmpaddr noprefixroute dynamic 
       valid_lft 86390sec preferred_lft 14390sec
    inet6 fe80::cc47:129d:bdff:a2da/64 scope link 
       valid_lft forever preferred_lft forever
3: sit0@NONE: <NOARP> mtu 1480 qdisc noop state DOWN group default qlen 1
    link/sit 0.0.0.0 brd 0.0.0.0
$ ping google.com
PING google.com (172.217.25.142) 56(84) bytes of data.
64 bytes from syd15s03-in-f14.1e100.net (172.217.25.142): icmp_seq=1 ttl=51 time=2.17 ms
64 bytes from syd15s03-in-f14.1e100.net (172.217.25.142): icmp_seq=2 ttl=51 time=1.95 ms
64 bytes from syd15s03-in-f14.1e100.net (172.217.25.142): icmp_seq=3 ttl=51 time=1.99 ms
64 bytes from syd15s03-in-f14.1e100.net (172.217.25.142): icmp_seq=4 ttl=51 time=2.20 ms

Figuring out information about PCI devices

To add a new passthrough device, or access a pci device in general, we need to know which io ports it uses, which interrupts it’s associated with, and the physical addresses of any memory-mapped io regions it uses. The easiest way to find this information is to boot linux natively, and run the command lspci -vv.

Configuring a Linux kernel build

We provide a custom kernel image with our CAmkES VM project, found here. This kernel image is produced from building Linux 4.8.16, specifically configured with the following .config file.

However you may decide to build your own Linux kernel image (which may be a different version). When doing so, it is important to ensure the build is configured with the following Kbuild settings:

# General kernel settings
CONFIG_X86_32=y
CONFIG_X86=y
CONFIG_X86_32_SMP=n
CONFIG_SMP=n
CONFIG_NOHIGHMEM=y
CONFIG_PCI_MSI=n
CONFIG_X86_UP_APIC=n
# Power management and ACPI settings
CONFIG_SUSPEND=n
CONFIG_HIBERNATION=n
CONFIG_PM=n
CONFIG_ACPI=n
# Virtio Settings
CONFIG_VIRTIO=y
CONFIG_VIRTIO_PCI=y
CONFIG_VIRTIO_NET=y

You can configure these settings by either manually editing your kernel .config file in the root project directory or by interactively running make menuconfig.