There was once a time when improving your system security meant throwing everything out in favor of a new model. Virtualization has since given system integrators a loophole to work with.
Virtualization makes it easier to run simultaneous platform-specific operating systems (Linux, RTOS, VxWorks, RTEMS, other) in virtual machines that emulate, virtualize, or use virtualization hardware extensions to provide the necessary hardware they require. These VMs are supported by a hypervisor running on a single device.
Now that virtualization support for 64-bit x86 architecture is available for the seL4 hypervisor, the loophole has gotten bigger.
“By expanding the CAmkES-VM to run 64-bit guests, this increases the feasibility of porting legacy systems,” says DornerWorks seL4 engineer Chris Guikema, one of the engineers responsible for the 64-bit x86 port. “This gives people the ability to run 64-bit builds of centOS or Ubuntu while gaining the security benefits of virtualization and seL4.”
Guikema says the development process started with a 64-bit kernel image. He tried to boot it up and investigated where it inevitably faulted.
“The first challenge was starting the virtual machine (VM) in 64-bit mode,” Guikema says. “Specific bits in the x86 registers needed to be set and there was very little documentation overviewing what those bits were.”
The team used a Dell OptiPlex 980 with an Intel Core i7 860 CPU to test the image. A Continuous Integration server allowed all the engineers working on the project to queue up their own tests on the same machine.
“This allowed all of us to test out our features without interfering with each other or having to move the hardware between desks,” says seL4 engineer Alex Pavey.
Once Guikema and the team recognized the 64-bit addresses they knew they were making greater progress. Their next challenge was allocating an address for the Linux OS memory requirements.
“32-bit and 64-bit software have different address translations, so I needed to research the 4-level translation scheme and implement the initial address space,” Guikema says. “Once those issues were taken care of, I started seeing Linux boot.”
The x86 entry trampoline code instructions must also be emulated to enable virtualization. Guikema accomplished this by referencing the assembly code at the addresses where the 64-bit mode boot faulted.
The final challenge involved sharing the CPU’s memory registers with the seL4 kernel.
“Previously, guests only ran in 32-bit mode, leaving 64-bit specific registers to be handled solely by seL4,” Guikema says. “However, a 64-bit OS needs to be able to modify these registers that are shared with the kernel. The solution ending up being saving seL4 and any VM’s version of these registers and restoring the proper version on a context switch.”
This milestone also brings improved performance to virtualization on seL4-based systems, and enables a few new features:
The CAmkES-VM for x86 previously only supported 32-bit VMs. This does not take full advantage of the hardware resources. DornerWorks added support in the seL4 kernel and VMM libraries to boot 64-bit VMs, which has been tested with a basic buildroot and centOS.
While there is not a limit to the number of VMs the CAmkES-VM can support, each VM is only given a single core. This does not take full advantage of modern processors, which have numerous cores and built-in support for multicore. DornerWorks added support in the VMM to boot VMs with multiple cores.
When running the CAmkES-VM, the filesystem has previously been mounted on RAM. While pass-through of a SATA device is possible, many processors may not have access to more than 1 SATA device. This forces secondary VMs to run in volatile memory, losing any information on a reboot. By partitioning access to a SATA device, multiple VMs can share the hardware resource, allowing for the file system to mount on non-volatile storage and persist between boots. Storage partitions on a SATA drive are virtualized out to the VMs, and each VM is given access to those partition through configuration.
“This way one VM cannot overwrite or inspect the storage space for another VM,” says seL4 engineer Robert VanVossen.
Public repos for the release can be found here:
Support for 64-bit x86 virtual machines on seL4 has not yet been rebased onto the master or merged into the Data61 mainline repositories yet. This port is also not backed by seL4’s proof. Running 64-bit VMs requires kernel changes and hypervisor extensions that are not yet backed by the proof.
If you would like help in accelerating your software development on the trusted base of the seL4 microkernel, schedule a meeting with our seL4 engineering group and we will collaborate with you on a plan to turn your ideas into reality.
