ZeroRISC and Tock OS Team Present Tutorial at ACM MobiSys 2025
On July 4th, ZeroRISC and the Tock secure embedded OS development team jointly presented a full-day tutorial on secure firmware design for hardware roots of trust (HWRoTs) using Tock.
This tutorial spotlighted Tock's memory protection, process management, and compiler-derived kernel isolation guarantees, providing a comprehensive view of how Tock can uphold HWRoT security requirements from userspace down to the metal.
As the primary author of the HWRoT-specific section of the tutorial, I deeply enjoyed the process of preparing and delivering the relevant materials. To make it useful as an onramp for others to learn more about Tock and general hardware security, I’ve put this post together.
We will review what Tock is and why its design is powerful for trusted hardware development, concluding with the highlights of the tutorial we shared. Please review the tutorial available here as part of the Tock Book for a more advanced overview. Following along at home only requires a development board and OLED screen breakout; see the Hardware Setup page in the Tock Book for details.
What is Tock?
Tock OS is a Rust-based embedded operating system designed for securely running multiple untrusted applications at once with strong isolation guarantees. By carefully leveraging embedded memory protection hardware and guarantees provided by Rust’s type system, Tock manages to offer both runtime isolation guarantees for applications, and compile-time isolation guarantees between different parts of the kernel, all while allowing applications to be both loaded on demand and completely untrusted.
Delving into runtime isolation, nearly all embedded devices have some support for hardware memory protection. Two common examples of such mechanisms are ARM’s Memory Protection Unit (MPU) specifications and RISC-V’s Physical Memory Protection (PMP).
Such mechanisms work by providing a hardware block in the processor with a fixed number of “slots” representing spans of physical memory. Each slot generally has associated permissions, such as:
RW (read-write) for a region of SRAM
RX (read-execute) for a flash region holding application code
RWX (read-write-execute) for a RISC-V Debug Module debug region
These can all be modified via memory-mapped registers. Memory addresses not in any provided region are generally treated as inaccessible. To enforce such a set of permissioned regions, these mechanisms monitor all processor memory accesses and fault the processor whenever the access policy given by these regions is violated.
Diagram illustrating a RISC-V PMP configuration. Each PMP region is a contiguous range of memory addresses which can be configured as readable, writable, and/or executable. If a memory access by the processor falls outside of the policy set by these regions, the processor will fault.
Tock’s context switching code carefully makes use of the memory protection mechanisms in several different processor architectures, limiting applications to exactly the memory they should access without assuming anything about how the application binary was constructed.
Diagram illustrating how the RISC-V PMP configuration is reconfigured on context switch. Since a different process's .text section and allowed SRAM regions will be used, PMP regions need to be shifted and even added/removed correspondingly.
In contrast, Tock’s kernel is designed such that isolation between components of the kernel, called capsules, is given at compile-time. In particular, Tock capsules can only be written using safe Rust, a subset of the Rust language that provides strong type-safety and memory-safety guarantees. In particular, safe Rust disallows constructing references to arbitrary memory, preventing capsules from accessing each other’s data except when explicitly permitted.
Moreover, Tock leverages this fact in several completely novel measures to prevent capsules from faulting the kernel as a whole. One key example is memory grants: rather than use a kernel heap that one capsule could exhaust, applications instead grant access to small portions of their memory via the syscall interface to provide heap space for capsules.
Diagram illustrating Tock's core architecture. Rather than maintain a global heap, Tock allocates an associated "grant" region for each application. This is memory which can be delegated piecemeal by the application to parts of the kernel as heap space, preventing a single kernel component from exhausting the heap for the whole system. (https://tockos.org/assets/img/architecture.png with permission)
In this manner, the portion of a Tock-based SoC that needs to be fully trusted remains quite minimal relative to other embedded OSes. For more details, the Tock website’s Design page is an excellent overview.
What makes a Hardware Platform Secure?
A secure hardware platform is often a subsystem of a larger device that provides some level of cryptographically-enforced trust to a larger system. For instance, a hardware root of trust (HWRoT) is a secure hardware platform responsible for the following:
Securely store cryptographic keys on behalf of the system it belongs to
Allow other subsystems to delegate cryptographic operations
Perform secure boot for the full system
Attest to the present firmware and configuration of the system
Encrypt and decrypting secure storage mediums
Coordinate device firmware updates for the full system
While a general-purpose processor could feasibly perform all of these operations; the key with a secure hardware platform is that these operations are performed in a dedicated, extensively-tested, and hardened subsystem, which can withstand attacks that a general-purpose processor will not.
Depending on the security and standardization requirements of a device, a secure hardware platform might be required to complete the following:
Prevent side-channel attacks by making use of constant-time, masked hardware implementations of cryptographic operations
Resist fault-injection attacks with a hardened processor design and fault detection logic
Detect active tampering using dedicated analog sensors and zeroize data in response
Leverage hardware-backed key stores to prevent direct key exfiltration by firmware
Undergo extensive third-party security review and even formal analysis to provide strong security guarantees
The aim is for other subsystems to be able to confidently rely on the platform’s integrity and confidentiality guarantees, delegating management of sensitive data and operations instead of undergoing the same degree of hardening.
Some notable secure hardware platforms in the wild include:
The general-purpose, open-access OpenTitan Silicon RoT, which comes in both discrete and integrated flavors
Apple's Secure Enclave, the integrated root of trust in iPhone mobile processors
Hewlett Packard Enterprise's Silicon Root of Trust, the integrated root of trust in their out-of-band management chip
Infineon's SLE78 Secure Element, which is used in YubiKey 5 series USB security keys
While these platforms are physical hardware systems, they all rely on firmware in order to make precise, careful use of the secure hardware. Two critical points to note are:
Secure firmware without secure hardware leaves the system open to a variety of hardware attacks, like side-channel analysis and fault injection attacks.
Secure hardware without secure firmware is vulnerable to the same set of firmware-level attacks that a general-purpose processor might be.
As such, a secure hardware platform must be realized as a joint, even co-designed system carefully assembled with the complementary security guarantees of hardware and software in mind. Firmware can make or break the security guarantees of a hardware platform; as such, careful consideration of what embedded OS the system leverages is due.
Why Tock as an OS for Secure Hardware?
As previously illustrated, Tock provides excellent security and isolation guarantees by design while allowing untrusted multi-tenancy, critical for delivering the various complex services a secure hardware platform must provide to its surrounding system.
Moreover, its careful design around the Rust language allows for the elimination of broad classes of memory and type safety violations at compile-time, critical for the delivery of truly secure systems in timeframes appropriate to a fast-moving market.
Yet, Tock serves as an excellent secure hardware platform OS for a more innate reason. Secure hardware isn’t designed as a monolith; typically, a well-designed secure hardware platform will be split into several stages which boot in sequence. In a secure hardware platform like a HWRoT, these form a chain of trust, inductively ensuring the security of the whole system. For example, when performing secure boot:
Boot stage 0 will be immutable (usually as mask ROM)
Boot stage n + 1 will be verified to match a manufacturer-signed hash by boot stage n before handing over control flow
Similarly, for attestation:
Boot stage 0 will be immutable (usually as mask ROM)
Boot stage n will generate a signature of boot stage n + 1’s hash, then lock write access to the certificate for later boot layers
The hierarchical nature of these dual processes allows for reasoning about a small part of the system at a time, allowing for both modularity and a granular permissioning structure. For instance, in a secure microprocessor the boot stages might take the form of
This is where each stage verifies and attests to the state of the next, and
ROM (the mask ROM) is baked into mask ROM
ROM_EXT (ROM extension) lies in flash, and is signed by the chip’s creator for security updates
BL (the bootloader) lies in flash, and is signed by the chip’s owner for everyday firmware updates
Tock’s design and trust model allows for seamlessly extending this chain of trust, instantiating the bootloader with Tock’s boot code and using applications as later boot stages. Because Tock has built-in support for application code signing and can be securely extended to provide application attestation, we can make our chain of trust become
As Tock provides strong compile-time isolation between kernel components, the application verification and attestation components of Tock can be carefully verified and isolated. Similarly, Tock’s design allowing for untrusted, hot-loadable, code-signed applications means that application code signing permissions can be trivially delegated to and revoked from a third-party by the device owner on demand.
Moreover, the kernel components that each application relies on–for instance, a secure signing service might rely on a hardware ECDSA driver–can be easily isolated and verified individually, providing defense in depth within the kernel even when a singular driver might be compromised.
In summary, this makes Tock a viable option for providing a reliable, secure, extensible OS for secure system design.
New Tock Book Section: Tock as a Root of Trust OS
As part of delivering our demo at MobiSys, zeroRISC and Tock OS developers contributed a chapter to the Tock OS Book, Tock as a Hardware Root of Trust Operating System.
This chapter, available here, focuses on building a toy encryption service as a Tock application to mimic the behavior of a small HWRoT like a secure element. From there, the reader is guided through a set of increasingly invasive attacks on the system, highlighting Tock's ability to provide defense in depth in practical applications as highlighted above.
I recommend reviewing this tutorial, and encourage readers to share feedback with us. If you’re interested in learning more, please take a look at our early-access program or contact us at info@zerorisc.com.
Conclusion
Secure hardware platforms are modern examples of where careful simultaneous consideration of hardware and software together is critical to success.
Tock, a modern Rust-based embedded OS, is an excellent example of how an operating system can complement the security guarantees of the hardware it runs on in a seamless fashion. At zeroRISC, we care about delivering strong security guarantees that extend up to the application software our customers rely on, and leveraging modern, secure embedded OS design is a critical part of being able to deliver that in practice.