On Tue, Nov 19, 2024 at 1:20 PM Amit Levy <amit@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/a1466b31cfc8dbd24a6f0eadc00...> #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/d...> 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@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@lists.tockos.org To unsubscribe send an email to devel-leave@lists.tockos.org