- Devel - lists.tockos.org

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

Re: No meeting today (June 21, 2024)

by Brad Campbell

I was hoping to discuss https://github.com/tock/tock/pull/4028. That PR enables two features for AppID: 1. Allows an AppID assignment policy to use the accepted credential when assigning IDs. This is important if the AppId is the public key used to verify a signature, for example. (This functionality used to exist and I removed it previously because of how process loading changed. Turns out we still need it.) 2. Helps developers use the accepted credential *correctly* when assigning an AppID. There are two issues/pitfalls that can arise when trying to use an accepted credential to assign an AppID. 1. The checker, while verifying the credential, has some state about the verification process that is necessary for assigning the AppID. Some examples: 1. The checker maintains a list of valid public keys that can verify signatures. The checker knows which public key was used to verify the signature. 2. The checker knows if the app was signed by the kernel developer or a third party (or both). 3. The checker has multiple public keys per organization, and knows which one signed the app. 2. TBF footers are *not* checked for integrity, and developers *must not* store any values in the footer that cannot be verified by the checker. Very little can be verified by the checker. If a public key is in the credential, the checker can validate that that public key matches the signature. But any other data cannot be verified and could be modified before the app is loaded on a board. To help with these issues, this PR also includes a `usize` that the checker can store with the accepted credential to provide information about the accepted credential that the AppID assignment policy can use. For issue #1: this would allow the process checker to keep track of some metadata about why it accepted the credential. For example it might store the index of the public key that verified the signature. Or it might store the upper 16 bits of the ShortId for the organization that signed the app. The value is opaque, and different policies/implementations can use it differently. The `Compress` trait (ie assigning ShortId) is *not* asynchronous. So from a software engineering viewpoint, whatever state the AppId assignment policy needs must be fetched in advance, and the policy can not re-run any verification steps. Therefore, the checker needs some way to communicate with the AppId assigner if the assigner is going to use any outcome of the verification process in its AppId assignment. For issue #2: this gives developers some way to attach state to an accepted credential without including that state in the credential itself. This isn't providing a correctness guarantee, but it is providing an alternative to what seems intuitively valid: just include it in the credential. Otherwise, developers that want to use different credentials to assign different AppIds can't (or have to build some sort of workaround). - Brad On Fri, Jun 21, 2024 at 11:12 AM Branden Ghena <branden(a)northwestern.edu> wrote: > The meeting today is cancelled as quite a few people are unavailable. > > Most of us will be meeting in-person this coming week for TockWorld and > we're excited to see you all there! > > -Branden > _______________________________________________ > Devel mailing list -- devel(a)lists.tockos.org > To unsubscribe send an email to devel-leave(a)lists.tockos.org >

June 21, 2024

No meeting today (June 21, 2024)

by Branden Ghena

The meeting today is cancelled as quite a few people are unavailable. Most of us will be meeting in-person this coming week for TockWorld and we're excited to see you all there! -Branden

June 21, 2024

Tock meeting agenda 2024-06-14

by Amit Levy

Meeting Link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b Agenda - Updates - Vote on "TRD: Tock Storage Permissions" (https://github.com/tock/tock/pull/4021) - Don't need - Approve - Change - Need more discussion (and if so what?) - Yield-WaitFor syscall update/plan (https://github.com/tock/tock/pull/3577) - Brad has done a bunch of updates, what's the status and what's left to do? - Kernel release planning

June 14, 2024