Trying to pick up the discussion from #1322 (comment):

That discussion suggested register_t could be considered for holding register values with seL4_Register potentially being added to the libsel4 types for the public variant. What are the reasons for selecting rword_t now beyond register_t already being used for register IDs?

The reason is trying to make this PR minimum (as register_t is already used by seL4 and needed more changes), but I'd very much like it to be register_t. This is based on our discussion at the seL4 summit that we want to only include the necessary parts for CHERI, so I made it an optional commit and separated this renaming part in a separate commit here: CTSRD-CHERI@1e4608f

I am more than happy to integrate that back if we all agree that's fine.

If there was consensus in using register_t for an actual register value type, then we would want to separately take that separate commit to apply in advance of this PR.

vptr_t is currently used by the kernel as an offset into a virtual address space and at this stage I don't agree that vptr_t variables should hold CHERI values. I'm interested in having the discussion about this.

For example: create_it_frame_cap() calls -> cap_frame_cap_new() and vptr is passed through as the mapping address that's written into the hardware page tables which has no use for CHERI permissions.

vptr_t is currently used as both user pointers (ipcbuf_vptr, v_entry, bi_frame_vptr, all Arm's cache operations, etc) and offsets/integers as you mentioned. When we need a type to be able to hold both pointers and integers, we just a CHERI type, hence I changed vptr_t.

We could split that up into two types if you'd like, one that's always a pointer, and another that's just an integer (though, I wouldn't include the ptr_t part in it because it's not really a pointer). However, that will require changes to existing function definitions, calls, and structures that might be more disruptive than my current changes.

Ok your right that sometimes the kernel uses vptr_t as offset into its own address space. I'm not sure whether this goes beyond the cache maintenance instructions though.

Do the cache maintenance operations that operate by VA change on Arm with CHERI to take a capability as the virtual address argument or is it just the address?

There is a place where the kernel does use a vptr_t value to initialize the initial thread's R0 for the address to the bootinfo struct. But it casts the vptr_t to a pointer first. This seems like a valid point to need to explicitly construct a new CHERI capability for launching this thread.

Ok your right that sometimes the kernel uses vptr_t as offset into its own address space. I'm not sure whether this goes beyond the cache maintenance instructions though.

Do the cache maintenance operations that operate by VA change on Arm with CHERI to take a capability as the virtual address argument or is it just the address?

Yes, they need a valid tagged capability in C64 mode. But in hybrid kernel it's not required.

There is a place where the kernel does use a vptr_t value to initialize the initial thread's R0 for the address to the bootinfo struct. But it casts the vptr_t to a pointer first. This seems like a valid point to need to explicitly construct a new CHERI capability for launching this thread.

Yeah, bootinfo passed to user, IPC buffer pointer (inside bootinfo struct), and user v_entry (written in the root thread's PC register). So 3 places at least where vptr_t is used as a pointer and needs to be a valid CHERI capability in a hybrid kernel.

But because it's the kernel managing CHERI pointers for a remote address space doesn't it make sense to pass around the raw address space offset and only construct the CHERI pointer right at the end when writing it into the user state?

[cheri][ipc] Make IPC's msg[] seL4_Register type

Hence, it is a deliberate decision to have msg[] the same as
rword_t/seL4_Register.

This decision is something that should have more discussion and I think the design choice here likely needs to be presented at the level of the RFC.

Currently the IPC buffer is defined in terms of 120 words for all architectures where a word is the same size for a pointer and for data. A benefit of this choice is the direct mapping of msg registers onto hardware registers for fast IPC transfer.

I argue that seL4_Word msg[seL4_MsgMaxLength]; should be preserved on CHERI configurations to continue supporting programs and interfaces that make use the IPC buffer to transfer messages. When transferring values that aren't CHERI pointers (The common case), halving the number of message registers and doubling their size would add a bunch of porting effort and make it harder to write programs that target both CHERI and non-CHERI hardware. We should consider it's possible to avoid this.

There are other options we could consider such as defining an alternate seL4_IPCBuffer type that can be used for invocations that transfer hardware caps values. Or inserting a union into the storage occupied by the msg field that allows it to be used through a seL4_Word interface or instead through a seL4_HWCap interface. (I think it would be worth considering aligning up the msg field to 128bits in this scenario).

[cheri][ipc] Make IPC's msg[] seL4_Register type

Hence, it is a deliberate decision to have msg[] the same as
rword_t/seL4_Register.

This decision is something that should have more discussion and I think the design choice here likely needs to be presented at the level of the RFC.

I am happy to discuss that, I'll just quote my reasons in the commit message here again:

Enable seL4's IPC buffer to seemingly hold CHERI-sized words.
Message registers in the IPC buffer intuitively correspond to the
underlying HW register/word's size/format, not an integer or a pointer.
It is used during IPC for various use cases such as:

1. Transferring HW registers (eg read/write/copy TCBRegisterContext)
2. Transferring register context to a fault handler
3. Transferring HW-register-sized data between user threads
4. System call arguments (eg TLSBase, VCPU reg)

Currently the IPC buffer is defined in terms of 120 words for all architectures where a word is the same size for a pointer and for data. A benefit of this choice is the direct mapping of msg registers onto hardware registers for fast IPC transfer.

I argue that seL4_Word msg[seL4_MsgMaxLength]; should be preserved on CHERI configurations to continue supporting programs and interfaces that make use the IPC buffer to transfer messages. When transferring values that aren't CHERI pointers (The common case), halving the number of message registers and doubling their size would add a bunch of porting effort and make it harder to write programs that target both CHERI and non-CHERI hardware. We should consider it's possible to avoid this.

The common case is transferring untagged data "words" or messages, not 64-bit integers. seL4_Word is no longer representing a HW word here, it's just an integer. The name is just left as it is (probably misleadingly) to avoid more disruptive changes, but it's documented in the commit message and it should only be used to hold integers.

I believe that this change has no effect at all on continuing supporting programs and interfaces, on the contrary, it's necessary to:

1. naturally respect, align with, and intentionally support the purecap ABI (where your words are really no longer seL4_Word integers), and,
2. avoid extra porting and maintenance headache (e.g., casting, unions, ifdefs, etc). This claim is based on my experimentations with sel4test and sel4bench that worked just fine with that change whether it was 120 words, or 59 words, with no changes at all this part, whether for CHERI or non-CHERI builds.
3. Perform 2x faster IPC (e.g., doing 128-bit untagged data copies, instead of 64-bit), when transferring fixed message sizes.

I don't mind preserving the seL4_MsgMaxLength to be 120 as it is (and I actually kept it that way in the previous PR), but that will require increasing the IPC buffer size, and I got the impression you don't want that from the discussion on the previous PR, so I changed it here.

There are other options we could consider such as defining an alternate seL4_IPCBuffer type that can be used for invocations that transfer hardware caps values. Or inserting a union into the storage occupied by the msg field that allows it to be used through a seL4_Word interface or instead through a seL4_HWCap interface. (I think it would be worth considering aligning up the msg field to 128bits in this scenario).

Like I said before, I would prohibit any tagged pointer transfer via memory across tasks and address spaces.

I would limit tagged pointer passing only via the register arguments of a select few syscalls, and add new single register read/write ones to avoid any need for tagged pointer passing via the IPC buffer.

seL4 can disallow multiple mappings of tagged pointer pages, as enabled with the new CHERI PTE flag set by:

• Only allowing a tagged pointer memory mapping if the page cap used is the only copy of that cap. This can be done by checking whether the parent object is an UT and whether there are no siblings.
• Prohibit cap copying of a page cap which is mapped with the CHERI PTE flag.
  You need the flag, you really don't want to enable tagged pointers for shared memory.

The above may result in a slightly bigger diff, but the actual behavioural and semantic change would be much smaller.

Hi Indan,

Like I said before, I would prohibit any tagged pointer transfer via memory across tasks and address spaces.

Yeah we agree on the across address spaces part.

I would limit tagged pointer passing only via the register arguments of a select few syscalls, and add new single register read/write ones to avoid any need for tagged pointer passing via the IPC buffer.

I have been thinking about this approach as well; do you think if the user maps the IPC buffer page without CHERI PTE capability load/store permissions, this will yield to that limiting behaviour? This way, only the fast message registers will be able to contain tagged pointers, and those get saved/restored from the TCB's archRegisters, not the IPC buffer.

seL4 can disallow multiple mappings of tagged pointer pages, as enabled with the new CHERI PTE flag set by:

• Only allowing a tagged pointer memory mapping if the page cap used is the only copy of that cap. This can be done by checking whether the parent object is an UT and whether there are no siblings.
• Prohibit cap copying of a page cap which is mapped with the CHERI PTE flag.
  You need the flag, you really don't want to enable tagged pointers for shared memory.

Exactly, we generally disallow tagged pointers for shared memory in CheriBSD (eg mmap with MAP_SHARED).

The above may result in a slightly bigger diff, but the actual behavioural and semantic change would be much smaller.
I will think about this further.

Like I said before, I would prohibit any tagged pointer transfer via memory across tasks and address spaces.

I made a separate thread for having that discussion: #1344 (comment)

I'd like for this thread to be about whether the IPC buffer storage should change it's type.

seL4_Word is no longer representing a HW word here, it's just an integer. The name is just left as it is (probably misleadingly) to avoid more disruptive changes, but it's documented in the commit message and it should only be used to hold integers.

I don't think we agree on what a HW word is. Usually 1, it's the natural unit of data used by the processor which is still 64 bits in an ARM C64 architecture because the natural size of data used by instructions is still 64bits. I can see how a disagreement in this definition leads to downstream disagreements about what the natural size of base types should be things like the IPC buffer.

3. Follow 2), while trying to be more intentional and use seL4_Register in shared code (non-CHERI and CHERI) to differentiate between using integers, pointers, messages registers, HW registers, etc.

I think option 3 should be considered:

• Specializing the seL4_Word to seL4_Register as a typedef is a pattern used elsewhere in libsel4 already,
• It does distinguish that the type of the field is "register" based and does map to register transfers by the kernel,
• The type change doesn't create any ABI break in non-CHERI architectures,
• It shouldn't break existing C client code because all supported architectures have the same original type.
• It gives a way for existing C code to be ported to CHERI aware while still being able to work with non-CHERI arch targets.

One possible downside is that non-C languages that generate language bindings via parsing the existing C headers may experience a breakage (eg a Rust bindgen approach), but we could ask about this when proposing the seL4_Register addition (it would need a small RFC).

@kent-mcleod Any preference on that change? I am happy to do either

I think my preference would need to be informed by trying to apply user level code to the changes. I know there's code that exists that uses a single 4k page for IPC buffer and some other thread specific data such as static TLS, and maybe it'd be better to keep the total IPC buffer size the same between C64 and A64.

No, we don't agree on that. Maybe Kent does, but I don't. I think it would increase the attack surface too much in practice if we would allow user space to do that. You don't for CHERI-BSD either, why open this gaping hole for seL4?

I think to merge something back upstream there should be acceptance of at least the design approach/goals and an acceptable implementation. I agree that transferring CHERI pointers across different virtual address spaces breaks a bunch of the monotonicity and confinement properties that CHERI enables. There's no way to use a mark and sweep approach for revoking capabilities if they can move across an address space for example.

@kent-mcleod Any preference on that change? I am happy to do either

I think my preference would need to be informed by trying to apply user level code to the changes. I know there's code that exists that uses a single 4k page for IPC buffer and some other thread specific data such as static TLS, and maybe it'd be better to keep the total IPC buffer size the same between C64 and A64.

Even when we increase the IPC buffer for CHERI, it'd still fit under 4k page. That is, it's only the structure size itself that got changed, but whenever you allocate an IPC buffer, it's still a 4k page as usual. No TLS or API changes were further required for that in sel4test/sel4bench.

I think to merge something back upstream there should be acceptance of at least the design approach/goals and an acceptable implementation. I agree that transferring CHERI pointers across different virtual address spaces breaks a bunch of the monotonicity and confinement properties that CHERI enables.

Yeah I am not disagreeing with that. I thought for this RFC:

1. We concluded that we globally, by default, forbid passing tagged pointers inter-AS.
2. We give the config option to the user to allow that for different threat models, given that they know what they're doing.
3. Even if the user allows 2, it still has the option to have strict CHERI security and avoid pointer aliasing by having non-overlapping address spaces for mutually distrusting (and untrustworthy compartments).

That way, we're making sure both seL4 and CHERI communities make the best use of this core CHERI-seL4 PR. We give the user the option to implement the most strict and/or informed flexible security policy based on their threat models. Where's the security gap here or the disagreement? What are the blockers?

There's no way to use a mark and sweep approach for revoking capabilities if they can move across an address space for example.

There are CHERI approaches to do so and to revoke propagated capabilities, however, this is a temporal safety issue that's beyond the scope of this project and isn't required to still have spatial memory safety. I listed it as future work, and this PR does allow it to be implemented by exporting the relative CHERI PTE bits. CheriBSD didn't have that for quite sometime, so it's totally fine for CHERI-seL4 to offer some spatial memory security and not address all CHERI issues we can think of immediately before this RFC/PR gets accepted; given that we know there are solutions for them and we don't forbid them. As I mentioned, this is just an incremental step to allow sensible CHERI use-cases on top with flexible security policies based on user's threat model.

3. Follow 2), while trying to be more intentional and use seL4_Register in shared code (non-CHERI and CHERI) to differentiate between using integers, pointers, messages registers, HW registers, etc.

I think option 3 should be considered:

• Specializing the seL4_Word to seL4_Register as a typedef is a pattern used elsewhere in libsel4 already,
• It does distinguish that the type of the field is "register" based and does map to register transfers by the kernel,
• The type change doesn't create any ABI break in non-CHERI architectures,
• It shouldn't break existing C client code because all supported architectures have the same original type.
• It gives a way for existing C code to be ported to CHERI aware while still being able to work with non-CHERI arch targets.

This PR does all of that.

One possible downside is that non-C languages that generate language bindings via parsing the existing C headers may experience a breakage (eg a Rust bindgen approach), but we could ask about this when proposing the seL4_Register addition (it would need a small RFC).

Can we maintain a list of all the invocation and syscalls that are having their interfaces changed to transfer hardware caps?
My understanding so far is that the following change:

• TCBSetTLSBase,
• All invocations that take or return a seL4_UserContext
• seL4_SetTLSBase

And what isn't expected to change:

• VSpace operations that use a virtual address for mapping or cache operations.
• seL4_TCB_SetIPCBuffer

(I assume that the seL4_ARM_SMC cap is out of scope at this stage too).

Good idea. I tried to separate such changes into separate "ABI" commits. seL4_ARM_SMC and seL4_ARM_VCPU_WriteRegs, seL4_ARM_VCPU_ReadRegs and future RISC-V hypervisor syscalls, etc are out of scope of this PR, but will need to change when we support hypervisors. Otherwise, what you mentioned are the minimum ones that were required to support passing purecap sel4test with the default configs.

Whether transferring HWCaps in an IPC buffer to a thread of a different VSpace is allowed is also something that probably needs to be specified in the RFC. I think that if the restriction is added, it would also require adding more invocations that allow transferring HWCapabilities across an address space.

My opinion is that conceptually, if transferring HWCaps across an address space is prohibited, then it follows that performing TCBWriteRegisters when the target TCB is in a different address space should also be prohibited unless the caller can present sufficient authority - control of the target VSpace via a Vspace capability, which would introduce new invocation variations.

Whether transferring HWCaps in an IPC buffer to a thread of a different VSpace is allowed is also something that probably needs to be specified in the RFC. I think that if the restriction is added, it would also require adding more invocations that allow transferring HWCapabilities across an address space.

I touched a bit on that in the previous reply.

My opinion is that conceptually, if transferring HWCaps across an address space is prohibited, then it follows that performing TCBWriteRegisters when the target TCB is in a different address space should also be prohibited unless the caller can present sufficient authority - control of the target VSpace via a Vspace capability, which would introduce new invocation variations.

Yeah I agree. This is also discussed in the other PR, and I suggested using the CHERI sealing mechanism for that, which might get us away with not having to introduce new seL4 invocations. This PR is an incremental effort, however. It's not aiming to have the most secure/restrictive CHERI solution yet, but should allow this to happen. I am happy to explore and trial with sealing if you think this (i.e., prohibit TCBWriteRegisters and friends from de-referencing inter-AS CHERI caps) is a blocker and needs to be addressed now. But IMO, it's not too bad for this PR to say, "if you build with CHERI and want secure CHERI behaviour, don't overlap your user processes address spaces, until/unless you/we provide better fine-grained solution, otherwise you should know what you're doing at your own risk"

Are the goals of this PR for merging or to serve as an informal checkpoint of progress? I assume that a goal of the RFC is to achieve consensus on design of CHERI support for seL4. So we eventually need to address this issue before the RFC can produce a result that has code landed in the seL4 repo. But having this PR in its current state is still useful to be able to use experimentally with user level projects.

I guess this PR should maybe be given the draft status too.

Both actually. I made the PR in a good-enough shape to be merged as an incremental core base that can, in its current state, run complete purecap sel4test/sel4bench userspace (to provide spatial memory safety as proposed, but not temporal memory-safety as it's beyond the scope of this project). It doesn't prohibit future seL4 and/or CHERI use cases or experimentations, while allowing for flexible security policies at user-level (e.g., completely disallowing tagged CHERI caps in the IPC buffer, avoid CHERI pointer aliasing by asking the user to not have overlapping AS, having intermediate trusted servers, etc). But that's just my opinion.

What I'd like to get out of this RFC PR and work with you and the community towards is identifying:

1. Any CHERI design blockers that must be addressed before this RFC/PR gets accepted.
2. Whether the verification-visible changes in non-CHERI shared code are minimal enough to be tolerated.
3. Future optional CHERI design trade-offs that aren't blockers for this PR to get merged, but important to think about.
4. anything else?

I'd put sealing and associating endpoint permissions with CHERI under 3, but happy to discuss.

How is authority for capability sealing and unsealing expected to be managed in seL4? What authority is needed to be able to seal a capability?

Capability sealing The CSeal and CUnseal instructions seal or unseal capabilities given a
suitable authorizing capability. Sealed capabilities allow software to implement encap-
sulation, such as is required for software compartmentalization.

How is authority for capability sealing and unsealing expected to be managed in seL4? What authority is needed to be able to seal a capability?

It currently isn't expected to be used in seL4 kernel itself (similar to CheriBSD). But it's just provided as CHERI helpers here in case we do in the future. The user, however, can use sealing as they wish (and there are many user-level compartmentalisation use-cases for it).

To answer your question, in order to seal/unseal a capability, you'd have to have a "sealer/unsealer" capability that:

1. Has sealing/unsealing permissions.
2. Has the same otype as the capability you're sealing/unsealing.

Capability sealing The CSeal and CUnseal instructions seal or unseal capabilities given a
suitable authorizing capability. Sealed capabilities allow software to implement encap-
sulation, such as is required for software compartmentalization.

I probably need to look more at some examples. Does a CHERI cap with sealing/unsealing permissions and no otype set represent authority to craft sealing/unsealing caps for any otype? Is that something that is controlled by the OS in cheriBSD or would it be given to the program's runtime? Thinking about how this could work on seL4. I think it's only relevant at this stage if there's suggestions of using sealing/unsealing to transfer CHERI pointers via IPC buffers.

I probably need to look more at some examples. Does a CHERI cap with sealing/unsealing permissions and no otype set represent authority to craft sealing/unsealing caps for any otype?

Yes

Is that something that is controlled by the OS in cheriBSD or would it be given to the program's runtime?

It's given to the program. CheriBSD doesn't manage or use that.

Thinking about how this could work on seL4. I think it's only relevant at this stage if there's suggestions of using sealing/unsealing to transfer CHERI pointers via IPC buffers.

Sealing and their invocations is still pretty much researchy. CheriBSD just lets the user do what they want with it, but we don't have production-ready uses for it AFAIK, and it's not used by default apart from sentries (just a special case for CFI). The sealing mechanism itself (e.g., otypes, invocations, unsealing, etc) also differs between Morello, our CHERI-RISC-V, CHERIoT, and the to-be-standardised CHERI-RISC-V draft. I wouldn't strongly bound this PR to it, but we could keep thinking about solutions using it for future use, and probably make suggestions to something like CHERI-RISC-V ISA draft to better accommodate CHERI-seL4 needs if we think of any.

Why does this need to be modified? Can't you use the compiler-provided header instead. It works for all other usecases? Adding a copy of this code seems like a bad idea.

If the compiler provided header does not work, we should fix that in the compiler and just require a new enough compiler for CHERI.

@arichardson It's because seL4 builds standalone and doesn't use or rely on any compiler headers (or standard libraries)

It uses -nostdinc -ffreestanding -fno-common -nostdlib when building the kernel and doesn't link to the compiler library. But as long as seL4 CHERI support is unverified, tweaking that a bit is preferred to duplicating compiler code.

You did add seL4 specific code to that file though, so it's not a pure copy either.

Yeah I added some helper functions along with some bootstrapping to initialise the CHERI-seL4 caps to that file. I tried to only contain such CHERI helpers in just two self-contained files (cheri.h and cheri.c). Also I added the option to do either DYNAMIC or capable relocs for Morello, which isn't there in the compiler toolchain file.

What FreeBSD does to still allow access to the compiler-provided headers is add Clang's resource dir as a explicit include directory, which is quite easy in CMake compared to the complicated makefile logic FreeBSD uses (https://github.com/freebsd/freebsd-src/blob/4b65481ac68a99122991fd73583d071c5e27c65a/share/mk/bsd.sys.mk#L285).

Something like

if (CHERI)
  execute_process(COMMAND ${CMAKE_C_COMPILER} --print-resource-directory OUTPUT_VARIABLE _clang_resource_dir)
  add_compile_options(-idirafter ${_clang_resource_dir}/include)
endif()