Welcome to the 2023 Tock Tutorial! This one-day, in-person workshop will teach how to use the Tock operating system for secure and reliable embedded systems.
Tock is a new operating system for embedded microcontrollers with a focus on safety and security. The kernel is written entirely in Rust, and the OS supports multiple independent applications which execute isolated from the rest of the system. Tock is being used for security key fobs, root of trust silicon, wireless sensor nodes, automotive ECUs, and other security-focused devices.
Tutorial Overview
The tutorial will provide hands-on experience with three aspects of Tock: the kernel, mutually distrustful applications, and secure systems. Each participant will have their own embedded development board to use and prototype with.
The final session will have participants develop a security-focused application: either a HTOP security key fob or a physical security wireless sensor.
Tock is an open-source project led by a consortium of developers from academia and industry. Tock extensively uses Rust to increase system robustness and minimize the amount of untrusted code in the kernel. If you are interested in Rust this tutorial will introduce you to a mature Rust project focused on embedded programming. If you are not interested in Rust, the tutorial will also include application-level development in C.
Details
- Date: Wednesday, July 26, 2023
- Location: Rice Hall, University of Virginia
- Room: Rice 130 (Lecture hall on main floor)
- Time: 10 am - 4 pm
Registration
Registration is available here!
Schedule
Note, schedule is subject to change.
| Time | Topic |
|---|---|
| 9:30 | Arrival and Check-in |
| 10:00 | Welcome and Overview of Tutorial |
| 10:15 | Introduction to Tock - (pptx) |
| 10:45 | Tutorial Lesson 1 |
| 12:00 | Lunch Break |
| 1:00 | Tutorial Lesson 2 |
| 2:15 | Break |
| 2:30 | Tutorial Lesson 3 |
| 3:45 | Wrap Up |
The tutorial itself can be found at: https://book.tockos.org/key-overview.html
Hardware
The tutorial is a hands-on experience where we will develop on real hardware.
Tock supports numerous hardware platforms, but for the tutorial we will use
platforms based on the Nordic nRF52840 microcontroller. Specifically, we will
use the nRF52840
DK board
(mouser,
digikey).
We encourage you to bring your own nRF52840-DK board so you can continue using Tock after the tutorial. Otherwise, we will have hardware boards available at the tutorial you can borrow.
Tutorial Sessions
The tutorial will be organized around three steps in one overarching theme: the creation of a USB security key.
Overview
For those new to Tock, we will give a brief primer on key aspects of the OS.
Session 1: HOTP Application
We will start by using and improving a userspace application that implements an HOTP security token. Consistent with other operating systems, Tock considers applications interdependently of the kernel, and as such applications can be written in any programming language (although we’ll use C for this tutorial). Importantly, the Tock kernel guarantees (as part of the thread model) that applications cannot maliciously affect other applications or the kernel.
Session 2: Encryption Oracle Capsule
In this session we will improve our security key by developing our own kernel capsule which is capable of encrypting and decrypting HOTP secrets. This will introduce the Tock threat model and how Tock’s architecture helps minimize potentially buggy code in the Tock kernel. As Tock is written in Rust, this session will introduce the subset of Rust (i.e. no dynamic memory allocation) used in the kernel, as well as some Rust programming concepts.
Session 3: Access Control
Building on the first two sessions, in the third session we will implement access control in Tock to limit which applications can run on our USB security key and ensure that only allowed apps have access to the encryption oracle capsule we developed.