Please respond with agenda items and +1s for tomorrow's core call
My proposed item:
- Do we want to support device passthrough to trusted processes? If so, how? For context, see https://github.com/tock/tock/pull/4044
Meeting Link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b
Agenda
- Updates
- Outstanding, assigned, PRs
- libtock-rs PR 551: Raw 802.15.4 support
- Brad's suggested PRs if there can be a discussion question raised for them
On June 26th, co-located with the TockWorld conference, a group of Tock
developers (about 30 of us) met in person to discuss the state of Tock
development and share future goals for the ecosystem.
We heard summaries of the year's work from the core, networking,
OpenTitan, documentation, libtock-c and tools working groups. Those
slides are all available from the conference agenda page
(<https://world.tockos.org/tockworld7#day1>).
In addition, we had a number of very productive breakout sessions
focused on future development directions and a preview of
Treadmill---the in-development testing and remote development system.
## Breakouts
### Non execute-in-place (XIP) platforms
In integrated settings---for example where a root-of-trust
microcontroller is on the same SoC as a more powerful application
core---there is often no persistent storage from which to execute code
directly. This may be, for example, because the SoC is too thin to fit
any flash storage.
In such cases, Tock must be adapted to load code (the kernel, processes)
from persistent storage into RAM and execute from their, raising several
challenges and opportunities. If persistent storage is not part of the
TCB, there may need to be some mechanism to validate code and
permissions before executing them. Loading code into RAM puts more
pressure on memory and, in turn, requires more careful consideration of
code size. Conversely, loading code into RAM means code and data can be
predictably located near each other, thus making relocation much simpler.
Action items from this breakout are to put together documentation
describing the use cases and goals for non-XIP settings (already begun
in <https://github.com/tock/tock/pull/4081>) as well as upstream a
specific implementation (probably virtualized) of a non-XIP "board."
### Tock registers
This breakout focused on the ongoing effort (lead by @jrvanwhy to revise
Tock registers to be both more sound and more ergonomic
(<https://github.com/tock/tock/pull/4001/files>).
Downstream users raised a number of edge cases that would be good to
support in the library.
### Formal methods with Tock
This breakout gathered a number of developers either interested in or
engaged in formally verifying parts of Tock. In particular, one group at
Google had tried to do some verification using Kani with limited
success, primarily due to issues with Kani. UCSD is doing work with Flux
and Verus to verify portions of the Tock system call API and memory.
Action items include setting up a communication channel for folks
interested in verification, reaching out to Verus to propose Tock as a
real-world verification target, and plugging other stakeholders
in---Google downstream users, Rust verification groups.
### Automated driver implementations
An idea raised in one of the discussions related to userspace
maintenance got its breakout to discuss the potential for automatically
generating userland bindings from specifications of a system call ABI in
the kernel.
Several ideas were raised for how to accomplish this. The outcome is a
plan to move Markdown documentation of system call interfaces to Rust
source files and build tooling to parse that documentation and generate
boilerplate C and/or Rust userland bindings.
### Panic-free kernel
This breakout discussed options towards a kernel with no `panic`. While
Tock generally tries to avoid explicit panics in the kernel, sometimes
that sneak in anyway, and sometimes they are hidden behind core language
features (e.g. slice operations).
Action items proposed were to open an RFC to solicit feedback, focus
first on kernel board files, followed by capsules.
### Multi-core
This breakout discussed adapting Tock to multi-MCU settings. A number of
use cases were raised:
- Separate security domains on different MCUs (e.g. cc26x2-style
application and communication cores)
- Applications that require enough performance to use two cores, and
platforms like the RPi have them. Different cores would handle
distinct set of peripherals.
- Chips with asymmetric cores (e.g. an M4 and M7, or a Cortex-M and
Cortex-R)
- Platforms with multiple cores and _no shared memory_ (e.g. Signpost or
two nrf52840DKs)
- SoCs where Tock runs on some co-processor, but another core which runs
some different OS.
Action items from this breakout include fixing IPC (potentially revising
completely), finishing work on CoreLocal, and a timeline for upstreaming
current downstream muti-core implementations.
### CHERI
A small group of developers discussed using Tock in CHERI-enabled
hardware---CHERI is a hardware-based capability system that can provide
extremely fine grained and expressive memory protection. At least one
port currently exists, but a major blocker for significant upstream
support is support for CHERI in Rust itself (currently people using Rust
on CHERI have forked toolchains).
The main action item is to propose to the Rust project to upstream
support for CHERI and, in particular, support a stabilized version of
pointer provenance.
## Takeaways
This was an extremely productive TockWorld! Thanks to everyone who
participated and sorry for those who couldn't make it.
Stay tuned for upcoming call-to-actions following up on each of the
action items from the breakouts.
-Amit
