TockWorld 8

September 5, 2025
Seattle, WA

Register

Agenda

  1. Topic

    Time

    Speaker

  2. Welcome & State of Tock

    Amit Levy

    Better Bytes

    9:00

  3. Coffee Break

    9:45

  4. Just because you can doesn't mean you should -- Rust TypeStates for improved driver safety

    Tyler Potyondy

    UCSD

    10:15

    Hardware provides driver authors both a strict specification of the things a driver is allowed to do, and a highly permissive memory-mapped I/O interface full of things a driver can do. Using the Rust type system, procedural macros, and a novel extension to typestate programming, we present our system that exclusively uses Rust to statically enforce Tock drivers' adherence to hardware's specifications, and that drivers only "do the things they should do". We achieve this all while imposing minimal to no overheads in runtime and code size.

    In this talk, I will present our system, describe how it can help improve the robustness of drivers in Tock, and finally detail a case study of how our system can enable developers to confidently program/utilize asynchronous hardware.

  5. Enabling the usage embedded-hal-async based drivers in the Tock kernel

    Alexandru Radovici

    Wyliodrin

    10:45

    Using Rust in embedded systems becomes more and more popular. Embedded frameworks and operating systems written in Rust are emerging every day. The Rust embedded working group has stabilised a set of traits, the embedded-hal and their asynchronous version, the embedded-hal-async. Frameworks like RTIC and Embassys and operating systems like Arial OS are based on these. Due to the standard traits, drivers can easily be migrated between them.

    Tock has a different approach to writing drivers, which makes it somehow disconnected from the ecosystem. We think that connecting Tock to the rest of the ecosystem will increase Tock's usage. Synchronous drivers, those using embedded-hal, are not portable to Tock as they break the way in which Tock works. Asynchronous drivers should be portable to Tock, as Tock's driver model is asynchronous. The main difference is that Tock does not support async/.await.

    This talk will present the ways in which we have tried to implement an asynchronous executor within the Tock kernel, without breaking the Tock's rules and using a minimum number of Rust unstable features. We will present the design decisions that we have made and the limitations that it presents. We will discuss about the drawbacks that the solution has and advantages it provides.

  6. Synchronization in Tock and Pluton

    Bobby Reynolds

    Microsoft

    11:15

    In spite of its single-threaded nature, the Tock OS kernel is vulnerable to certain types of race conditions due to its highly concurrent, interrupt-driven event loop. All but the most trivial operations generally require multiple turns around this loop, and each turn presents a chance for new activity which may modify the system state and interfere with ongoing operations.

    This presentation will walk through different categories of race conditions and discuss the solution space, including the existing “Mux” pattern and a proposal for a new, general-purpose “Mutex” object. Along the way, discussion will be motivated using case studies drawn from both the upstream Tock community as well as challenges faced internally by the Pluton team at Microsoft.

  7. Lunch

    12:00

  8. Enabling LLVM PIC in Tock OS

    Beshr Islam Bouli

    zeroRISC

    12:45

    This session shares progress on enabling position-independent code (PIC) in the Tock OS, focusing on integrating ROPI/RWPI support across LLVM, Rust, and Tock userland. I’ll discuss challenges encountered in getting PIC code to compile and run on MMU-less systems, how LLVM’s ePIC model fits in, and early steps toward upstreaming required changes. The talk will also touch on how this work lays the groundwork for more dynamic embedded apps in Tock.
  9. ARMv8-M Architecture Port

    Darius-Andrei Jipa

    OxidOS Automotive

    13:15

    This talk presents the porting of the Tock operating system to the ARMv8-M architecture, targeting modern Cortex-M processors. Porting Tock to ARMv8-M required significant care to be taken with the TrustZone-M, requiring updates to the context switch mechanism, interrupt handling, and support for the ARMv8-M exception model. The port also introduces support for the Secure Attribution Unit (SAU) and the Memory Protection Unit(MPU), enabling fine-grained control over memory access permissions. Evaluation on ARMv8-M hardware demonstrates that Tock retains its minimal overhead and safety guarantees, while opening new opportunities for building secure, energy-efficient IoT systems on next-generation microcontrollers.
  10. Tick-Tock-Tock-Tock... Tock Goes Multicore

    Gongqi Huang

    Princeton

    13:45

    Multicore microcontrollers are ubiquitous in today's embedded world. Yet, Tock, in its current form, cannot fully leverage hardware parallelism as it mainly targets single-core MCUs. To this end, we adopt a multikernel approach --- running an independent Tock kernel instance per CPU core. Efficient peripheral sharing and communication are enabled by transferring ownership of Rust values between Tock instances.
  11. Coffee Break

    14:15

  12. Data Movement Patterns in Tock OS and Pluton

    Hussain Miyaziwala

    Microsoft

    14:45

    Tock’s default I/O and crypto drivers rely on statically allocated kernel buffers, which in highly constrained systems like Pluton lead to significant RAM waste and fixed transfer limits.

    This talk presents a “lazy” push/pull pattern: instead of copying into per-client buffers, drivers invoke callbacks to stream data on demand. We’ll illustrate with a redesigned UART interface and our real-world ECC capsule, quantify memory savings, surface key design choices(naming, length negotiation, chunking), and invite feedback on upstreaming this pattern as reusable traits or an I/O subsystem.

  13. The Time is Right: Retrofitting Formal Verification on Timers

    Samir Rashid

    UCSD

    15:30

    The timers in an operating system underlie everything including scheduler interrupts, radio timeouts, and user alarms. Despite its critical nature, timers are notoriously difficult to test for correctness. We present our work designing a specification for timers and then bolting formal verification onto Tock's timer subsystem. We verify the correctness of Tock's virtual alarms using the Verus Rust formal verification tool.
  14. Verified Isolation in Tock

    Evan Johnson

    NYU

    16:00

    Tock's core security guarantee is that processes remain isolated from one another---one misbehaving Tock process should not be able to read or write the sensitive data of another Tock process. To enforce this guarantee, Tock relies on a combination of hardware memory protection (the MPU) and language-level techniques (Rust), which, in practice, can be difficult to get right.

    In this talk, I'll discuss my team's efforts to formally verify process isolation in Tock. I'll highlight several subtle isolation-breaking bugs we uncovered during the verification effort, as well as opportunities for optimization that emerged from formally modeling Tock's MPU interface. I'll conclude with a discussion of our ongoing and future work.

  15. Closing Remarks

    Amit Levy

    Better Bytes

    16:30