- Devel - lists.tockos.org

Tock Meeting Agenda 2024-12-06

by Branden Ghena

Meeting link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b Agenda - Updates - PR check-in - #4250 MachineRegister type <https://github.com/tock/tock/pull/4250> - #4256 ARMv7m EXC_RETURN <https://github.com/tock/tock/pull/4256> - #4259 ARMv6 CONTROL register <https://github.com/tock/tock/pull/4259> - Any others people want to bring up - Release Plan Thanks, Branden Ghena Northwestern University

Dec. 6, 2024

Call for Tock Meeting agenda items 2024-12-05

by Branden Ghena

Please respond with any agenda items for tomorrow's call. -Branden

Dec. 5, 2024

No Tock core meeting today

by Amit Levy

In lieu of proposed agenda items and due to a few absences anyway, let's cancel this week. Instead, please review the recent type-safe system call ABI proposal: https://github.com/tock/design-explorations/pull/4 We will likely also skip next week due to the Thanksgiving holiday.

Nov. 22, 2024

Call for Tock meeting agenda items 2024-11-22

by Amit Levy

Please respond with any agenda items for tomorrow's call.

Nov. 22, 2024

Re: Type-safe syscall exploration

by Johnathan Van Why

On Tue, Nov 19, 2024 at 1:20 PM Amit Levy <amit(a)amitlevy.com> wrote: > Johnathan, > > Thanks for this very detailed writeup! > > My general take is that this is probably the right direction for the > next version of the ABI. > > A few high level comments, partially based on one-on-one discussion with > you: > > First, good to separate the high level approach from the specific > details of each system call. High level, this is basically defining a > set of possible types that can be passed across the ABI, how those types > are laid out in registers/memory when passed in various configurations > and orders, and a way of communicating those which types are being > passed. > > To that extent, one question is whether this covers all the right types > and not more. My intuition is yes, it includes all of the typical > primitive types we care about. There are two more types I came up with that could fit into this design; I omitted them because: 1. They are more complex to explain, and I didn't feel the extra paragraphs would contribute to the goals of the document. 2. They are a greater deviation from the design of Tock 2.0, and I wanted to keep this design Tock-2.0-ish to keep it easily digestable and limit the number of ideas we're discussing concurrently. 3. I ran out of 4-bit type IDs (!). For completeness, the extra types I came up with are "read-only slice" and "read-write slice". These types are effectively &[u8] and &mut [u8] from Rust, and would provide access to the buffer they point to for the duration of the system call. They would enable you to avoid an Allow and un-Allow pair when you're calling a system call that only needs synchronous access to the buffer (e.g. if we add a blocking Command syscall). > It also includes "CHERI" capabilities as > a "special" type, which is problematic on non-CHERI platforms, but I > think this is easily captured by some general name like "descriptors" or > something, that fit in a register, and refer to structure the kernel > keeps track of (e.g. file descriptors---these are not meant to be CHERI > pointers). > We could do that, but that does give up the main benefit of using CHERI capabilities for handles: userspace cannot forge CHERI capabilities. I don't see much advantage in having a separate "descriptor" type rather than just using u32. If we remove the "fit in a register" part though, then we could still have an unforgeable handle type. On CHERI systems handles would be a capability, and on non-CHERI systems handles would be (128-bit?) cryptographically secure random numbers. Second, it's not totally obvious we need or want this first register > that communicates the types across the ABI. In particular, for each call > and response there _has_ to be a specific contract between the driver > and process, as neither will deal with _all_ possible variants > reasonable. We need a way to "communicate" or check that contract, but > probably doing so at load time or installation time is better than > dynamically. E.g., perhaps a TBF header that describes the expected > interface from drivers and a loader (either on the host, at > compile/composition-time, or in the kernel at dynamic installation time) > ensures the kernel current drivers actually expose that interface. > There is a large spectrum of designs between "types are checked only at runtime" (the design I proposed) and "types are not checked but breaking changes are disallowed by CI" (mentioned in possible improvement <https://github.com/tock/design-explorations/blob/a1466b31cfc8dbd24a6f0eadc0…> #4). Personally, I'm a fan of moving checks to build time (and where possible automating backwards-compatibility checks). Here's another idea that's between the two extremes: Create a deterministic way to map a system call signature into a string. For example, button driver command 3 <https://github.com/tock/tock/blob/a25d927a32c7c77c45be9aecd0cd680dc3522bd5/…> might become: class: Command, driver: 3, command number: 3, name: "Read button", Args: (u32), Success: (bool), Failure: (ErrorCode) We then run this string through a deterministic fingerprint function <https://en.wikipedia.org/wiki/Fingerprint_(computing)> to "convert" it into a 64-bit value. To make a system call, userspace writes that value into one or two registers, and the kernel uses a lookup table to identify the correct system call to invoke. Except for the slight risk of fingerprint collision, this gives us strong type safety (and would catch a type mismatch if an app and kernel are compiled against incompatible versions of a syscall API), and unlike using type descriptors it allows for more than 15 types. It also avoids the cost and build system complexity of using a TBF header. However, debug information for an "unknown syscall" would be very limited as the kernel would only know the fingerprint of the unknown syscall. > Conversely, what, if any, are the cases for dynamically checking the > type of the arguments/returns across the ABI boundary? (this is a > question for everyone, not just Johnathan) > Having the type descriptors at runtime seems useful for debugging output. For example, a failed syscall could output something like: Syscall type mismatch: moisturemonitor invoked driver 3 command 3 with argument type (i32) but argument type (u32) is required. Of course, this would have a code size impact and I would expect it to be turned off by more demanding Tock users. If we remove the "Each specific Command [...] must specify its argument type [...]" rule, we could have dynamically-typed commands. For example, an RPC driver could enable a userspace process to pass a message of dynamic type to another process via a single Command call (and the message would be delivered as an upcall with a dynamic argument type). > -Amit > > Johnathan Van Why via Devel <devel(a)lists.tockos.org> writes: > > > Inspired by the ongoing discussions about porting Tock to CHERI, I wrote > > down some ideas on how to make Tock's syscall ABI more type-safe. The > > writeup is in the design-explorations repository at Add an exploration of > > type-safe system calls < > https://github.com/tock/design-explorations/pull/4>. > > While I'm not suggesting that we should start on Tock 3.0 now, I do think > > we should incorporate some of the design ideas into Tock 3.0 when it > > happens. A secondary goal of the document is to spread knowledge about > > CHERI. > > > > Feel free to take a look, and either reply with feedback here or comment > on > > the PR. > > > > -Johnathan > > _______________________________________________ > > Devel mailing list -- devel(a)lists.tockos.org > > To unsubscribe send an email to devel-leave(a)lists.tockos.org >

Nov. 19, 2024

Re: Type-safe syscall exploration

by Amit Levy

Johnathan, Thanks for this very detailed writeup! My general take is that this is probably the right direction for the next version of the ABI. A few high level comments, partially based on one-on-one discussion with you: First, good to separate the high level approach from the specific details of each system call. High level, this is basically defining a set of possible types that can be passed across the ABI, how those types are laid out in registers/memory when passed in various configurations and orders, and a way of communicating those which types are being passed. To that extent, one question is whether this covers all the right types and not more. My intuition is yes, it includes all of the typical primitive types we care about. It also includes "CHERI" capabilities as a "special" type, which is problematic on non-CHERI platforms, but I think this is easily captured by some general name like "descriptors" or something, that fit in a register, and refer to structure the kernel keeps track of (e.g. file descriptors---these are not meant to be CHERI pointers). Second, it's not totally obvious we need or want this first register that communicates the types across the ABI. In particular, for each call and response there _has_ to be a specific contract between the driver and process, as neither will deal with _all_ possible variants reasonable. We need a way to "communicate" or check that contract, but probably doing so at load time or installation time is better than dynamically. E.g., perhaps a TBF header that describes the expected interface from drivers and a loader (either on the host, at compile/composition-time, or in the kernel at dynamic installation time) ensures the kernel current drivers actually expose that interface. Conversely, what, if any, are the cases for dynamically checking the type of the arguments/returns across the ABI boundary? (this is a question for everyone, not just Johnathan) -Amit Johnathan Van Why via Devel <devel(a)lists.tockos.org> writes: > Inspired by the ongoing discussions about porting Tock to CHERI, I wrote > down some ideas on how to make Tock's syscall ABI more type-safe. The > writeup is in the design-explorations repository at Add an exploration of > type-safe system calls <https://github.com/tock/design-explorations/pull/4>. > While I'm not suggesting that we should start on Tock 3.0 now, I do think > we should incorporate some of the design ideas into Tock 3.0 when it > happens. A secondary goal of the document is to spread knowledge about > CHERI. > > Feel free to take a look, and either reply with feedback here or comment on > the PR. > > -Johnathan > _______________________________________________ > Devel mailing list -- devel(a)lists.tockos.org > To unsubscribe send an email to devel-leave(a)lists.tockos.org

Nov. 19, 2024

Type-safe syscall exploration

by Johnathan Van Why

Inspired by the ongoing discussions about porting Tock to CHERI, I wrote down some ideas on how to make Tock's syscall ABI more type-safe. The writeup is in the design-explorations repository at Add an exploration of type-safe system calls <https://github.com/tock/design-explorations/pull/4>. While I'm not suggesting that we should start on Tock 3.0 now, I do think we should incorporate some of the design ideas into Tock 3.0 when it happens. A secondary goal of the document is to spread knowledge about CHERI. Feel free to take a look, and either reply with feedback here or comment on the PR. -Johnathan

Nov. 19, 2024

Tock meeting agenda 2024-11-15

by Amit Levy

Meeting link: https://meetings.dialpad.com/room/tock/1vnk9r3e1b Agenda - Updates - TockWorld format and timing - x86 upstreaming: fresh rewrite or vendored crate - `usize` in ABI -comments PRs #4228 and #4229 - Crypto WG proposal

Nov. 15, 2024

Re: Call for Tock meeting agenda items 2024-11-15

by Amit Levy

- TockWorld planning, specifically same format as last year? Or different? - x86 upstreaming: fresh rewrite or vendored crate - Crypto WG proposal - Significant downstream differences in crypto HILs, should we empower a group to redesign the upstream ones? - What's in a `usize`? (comments PRs #4228 and #4229, and discussions around non-32-bit ABIs)

Nov. 14, 2024

Call for Tock meeting agenda items 2024-11-15

by Amit Levy

Please respond with any agenda items for tomorrow's call.

Nov. 14, 2024