July 2024 - Devel - lists.tockos.org

Tock meeting agenda 2024-07-26

by Amit Levy

Meeting Link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b Agenda - Updates - Outstanding, assigned, PRs - OpenTitan working group status and trajectory - Dynamic allocation in libtock-rs - https://lists.tockos.org/hyperkitty/list/devel@lists.tockos.org/message/QYQ…

July 26, 2024

Re: Call for Tock meeting agenda items 07/26

by Hudson Ayers

I would like to discuss options for dynamic allocation in libtock-rs. There are two basic approaches: 1. The approach used in the old libtock-rs: Allow apps to specify a heap size at compile time, reserve that much space for the heap using brk() while initializing the runtime, and then use an allocator that assumes a backing store of a fixed size (such as linked_list_allocator <https://crates.io/crates/linked_list_allocator>). 2. An approach similar to that originally suggested <https://github.com/tock/libtock-rs/pull/205#pullrequestreview-436914914> by Johnathan when the old libtock-rs allocator was first implemented: a heap that only takes memory from the kernel as needed, and return memory to the kernel when no longer needed. The idea is generally an allocator that works on a backing store it was given, but will grow the size of this contiguous backing store as needed. One advantage of this approach is that if an app wants to allocate a bunch of memory, then return it before calling any syscalls that lead to grant allocation, that app can use more memory than would otherwise be possible given the size of a grant allocation. This approach can also just be useful toward maximizing the memory available to the app -- rather than having to specify a constant heap size that is known to be smaller than (app memory - allocated grant size), the app can just use everything that is not taken by grants, and then allocations will start to fail once that point is reached. The second approach is more challenging to integrate with existing open source embedded Rust allocators, because in practice I have not found any that provide APIs for returning memory given to the allocator back to the kernel, without having to add an OS port to the allocator itself. IMO this approach seems more likely to require us to write our own allocator, or to modify an existing open source allocator with a port to Tock specifically. Interested to hear what others think. On Thu, Jul 25, 2024 at 5:15 PM Amit Levy via Devel <devel(a)lists.tockos.org> wrote: > Please respond with agenda items and +1s for tomorrow's core call > _______________________________________________ > Devel mailing list -- devel(a)lists.tockos.org > To unsubscribe send an email to devel-leave(a)lists.tockos.org >

July 26, 2024

Call for Tock meeting agenda items 07/26

by Amit Levy

Please respond with agenda items and +1s for tomorrow's core call

July 26, 2024

Tock meeting agenda 2024-07-19

by Amit Levy

Meeting Link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b Agenda - Updates - Outstanding, assigned, PRs - Device passthrough to trusted processes, and how. See <https://github.com/tock/tock/pull/4044> for context

July 19, 2024

Call for Tock meeting agenda items 07/18

by Amit Levy

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

July 18, 2024

Tock meeting agenda 2024-07-12

by Amit Levy

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

July 12, 2024

Re: Call for Tock meeting agenda items 07/12

by Brad Campbell

- https://github.com/tock/tock/pull/4028 - Addresses the general problem that an AppId assigner may need information from the app verifier to correctly assign AppIds/ShortIds. - Feedback from last week was it would be better if the "feedback" was a generic type T rather than a usize. I tried this but that type gets propagated to ProcessBinary which feels not worth it. - https://github.com/tock/tock/pull/4031 - Implements the storage permissions TRD. Provides kernels with much more flexibility on how storage permissions are assigned. - Recent changes: capabilities are now required to construct a storage permission. - https://github.com/tock/tock/pull/4075 - Use .cargo/config.toml to specify required build flags so that `cargo X` commands work. - Including hidden files that are necessary to build the central piece of software is a *contentious* issue. However, I think we have a workable solution with upside that outweighs the negatives. - However, `cargo test` does not work because we build core. Anyone know what to do about that? On Thu, Jul 11, 2024 at 2:38 PM Johnathan Van Why <jrvanwhy(a)google.com> wrote: > libtock-rs PR 551: Raw 802.15.4 support > <https://github.com/tock/libtock-rs/pull/551>: It is failing in CI > because Miri is catching UB, and the author is having trouble understanding > the cause of the UB. I suspect the design is unsound and probably not easy > to fix -- and I commented that on the PR -- but I don't have the time > needed to fix it (I'm not familiar with how these buffers are supposed to > work or how they are supposed to be used). I'm anticipating an awful and > drawn-out review experience for the PR author if we don't course correct > now (especially as I leave for a 3 week vacation tomorrow afternoon), so > I'm hoping to avoid that outcome. > > On Thu, Jul 11, 2024 at 11:32 AM Amit Levy <amit(a)amitlevy.com> wrote: > >> Please respond with agenda items and +1s for tomorrow's core call >> _______________________________________________ >> Devel mailing list -- devel(a)lists.tockos.org >> To unsubscribe send an email to devel-leave(a)lists.tockos.org >> > _______________________________________________ > Devel mailing list -- devel(a)lists.tockos.org > To unsubscribe send an email to devel-leave(a)lists.tockos.org >

July 11, 2024

TockWorld Developer Day Recap

by Amit Levy

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

July 11, 2024

Re: Call for Tock meeting agenda items 07/12

by Johnathan Van Why

libtock-rs PR 551: Raw 802.15.4 support <https://github.com/tock/libtock-rs/pull/551>: It is failing in CI because Miri is catching UB, and the author is having trouble understanding the cause of the UB. I suspect the design is unsound and probably not easy to fix -- and I commented that on the PR -- but I don't have the time needed to fix it (I'm not familiar with how these buffers are supposed to work or how they are supposed to be used). I'm anticipating an awful and drawn-out review experience for the PR author if we don't course correct now (especially as I leave for a 3 week vacation tomorrow afternoon), so I'm hoping to avoid that outcome. On Thu, Jul 11, 2024 at 11:32 AM Amit Levy <amit(a)amitlevy.com> wrote: > Please respond with agenda items and +1s for tomorrow's core call > _______________________________________________ > Devel mailing list -- devel(a)lists.tockos.org > To unsubscribe send an email to devel-leave(a)lists.tockos.org >

July 11, 2024

Call for Tock meeting agenda items 07/12

by Amit Levy

Please respond with agenda items and +1s for tomorrow's core call

July 11, 2024