IceCap

IceCap is a virtualization platform from Arm Research with a minimal trusted computing base that aims to provide guests with confidentiality and integrity guarentees. IceCap serves as a research vehicle for virtualization-based confidential computing. At the foundation of IceCap is seL4, the formally verified microkernel.

This seL4 Summit 2020 talk provides a high-level overview of IceCap's design.

The IceCap project is logically partitioned into the IceCap Hypervisor, which names the firmware and supporting components which together form the virtualization platform mentioned above, and the more general IceCap Framework, which is a collection of libraries and tools for constructing seL4-based systems. The IceCap Hypervisor is the original purpose of the IceCap Framework, and remains the reference application of the IceCap Framework. This repository contains both the IceCap Hypervisor and the IceCap Framework.

Highlights

• IceCap Framework replaces the C-based seL4 userspace of the seL4 software ecosystem with Rust. With the exception of libsel4 and the CapDL loader, the IceCap Hypervisor's seL4 userspace contains less than 400 lines of C.
• The IceCap project includes a port of the MirageOS unikernel to seL4.
• The build system of the IceCap project is based on Nix for the sake of hermeticity, configurability, and maintainability.

We are eager to share and discuss any aspect of IceCap's design and implementation with you directly. Please feel free to reach out to project lead Nick Spinale <[email protected]>.

Demo

See ./demos/hypervisor/README.md for instructions on how to build and run a demo of the IceCap Hypervisor.

Tutorial

See ./examples/README.md for a tutorial-style introduction to the IceCap Framework.

Supported platforms

IceCap supports Armv8.

Note that we intentionally use different platform names than the seL4 kernel. seL4 has the notion of a KernelPlatform (e.g. bcm2711 for the Raspberry Pi 4). Our platforms may eventually become more specific than those named by seL4.

• virt: A minimal, made-up platform emulated by QEMU with qemu-system-aarch64 -machine virt

• rpi4: Raspberry Pi 4 Model B (with at least 4GiB of RAM)