Introduce capability levels

[arichardson]

This adds the local/global mechanism of CHERIv9, augmented with the LoadGlobal feature of CHERIoT. The specification is written in such a way that a future extension could extend the bits used for local/global to more than one.

[arichardson]

CC: @nwf @davidchisnall

[davidchisnall]

I think this is sufficiently expressive for what we need. We currently have orthogonal global and store local, and we use the following combinations:

• Global, not StoreLocal: heap, globals.
• Local, not StoreLocal: heap and globals that are temporarily delegated.
• Local and StoreLocal: Stacks / register save areas.

We don’t use StoreLocal + Global because that would violate stack isolation. This means that, in our encoding, Global is an orthogonal permission but StoreLocal is a dependent permission that can exist only if you have both W and c permissions and so we can squeeze it into a corner of the encoding space.

I believe that his scheme could be represented in this proposal.

That said, I don’t think that this belongs in the core specification. We have shown that our use of local/global works well in the context of an RTOS but there is, as yet, very little demonstration that either this or the generalised multi-level variant is the right thing on larger systems. For example, when we worked through the levels we’d want in CheriBSD, we came up with a bunch of different concepts that would be nice to express:

• Kernel vs userspace.
• Compartment-local vs shared.
• Thread-local (including stack) vs shared.
• Hypervisor-owned vs guest-owned.
• Stack, TLS, heap, global, with ordering between them.

A few people have used local-global in different ways in Morello, but this still feels like something that’s too close to research to be in the base spec. Putting it in a separate optional extension and aligning the permissions with CHERIoT so that we can appear as a two-level instantiation of that extension would be fine.

[andresag01]

Thanks for the proposal! A few questions after an initial read through.

[tariqkurd-repo]

I really don't follow the details of how this feature works, I guess it doesn't help that I'm not familiar with the feature in either CHERI v9 or CHERIoT.

I think we need a better description.

[nwf]

There are several intertwined mechanisms here; let me try to go through each in turn, specifically in the context of CHERIoT.

At its most basic, CHERIoT uses two of the permission bits discussed here to differentiate stack memory from globals and heap, and from that builds a few useful properties. Specifically, the RTOS bootstrap ensures that...

• All pointers to globals and the heap arena are "global" (bear a set GL bit) and not store-local (bear a clear SL bit).
• All thread initial stack pointers are marked "local" (bear a clear GL bit) and store-local (bear a set SL bit).

First and foremost, this architectural feature propagates up to software as the property that pointers derived from stack pointers are confined to the stack (cannot be stored into globals or onto the heap). The policy asymmetric and the reverse is permitted: pointers to globals or into the heap can be stored to the stacks.

Beyond that static partitioning, it is possible for software to clear the GL bit, changing a "global" capability to a "local" one, such that storing it to memory now requires a SL-bearing authorizing capability. This provides software with a "shallow no-capture" mechanism: compartment A can take a "global" capability to a heap object and down-convert it to "local" before handing it to compartment B (as part of a cross-compartment call); by the time compartment B returns, the only locations that may have come to hold copies of that passed capability are pointed to by SL-bearing authorities, usually just the stack. Zeroizing the stack between the caller's high water mark (lowest used address) and the callee's high water mark is sufficient to eliminate most of these automatically. [0]

The addition of the "load global" (LG) permission can transmute "shallow no-capture" to "deep no-capture". By clearing both GL and LG on a passed pointer, compartment A can ensure that no part of the graph structure transitively referenced by that pointer can be captured by compartment B. [0] [1]

[0]: One does need to be a little careful about passing SL-bearing pointers as arguments in cross-compartment calls; it is possible for the callee to "capture" local capabilities into such spaces, so the caller must take defensive countermeasures. Usually, though, the stack (automatically managed by the runtime) is the only SL-bearing capability passed across compartment boundaries. See https://github.com/CHERIoT-Platform/cheriot-rtos/blob/5763f0fe7d08e8799af97722c0169db3789e62fc/sdk/core/switcher/entry.S#L780-L832 for the gory details of cross-compartment return handling.

[1]: There is some subtlety around the interaction of sealed capabilities and LG. When a non-LG-bearing authority is used to load an unsealed capability, the result will have both GL and LG cleared. However, if the load is of a sealed capability, GL will be cleared but LG will be preserved; that is, GL is "outside" the seal while LG is "inside". Tangentially, both SD (what the draft calls W) and LM are "inside" the seal and so will not be cleared when loaded through a non-LM-bearing authority. See CHERIoT-Platform/cheriot-sail#14 and CHERIoT-Platform/cheriot-sail#44 for the full details.

Whew. I hope that's useful?

[andresag01]

@nwf : Thanks for the explanation from CHERIoT's perspective. Then do you agree with @davidchisnall that the feature described in this PR is sufficiently expressive for what CHERIoT needs?

[davidchisnall]

I am now less convinced by my own argument, because I had not thought about the PermitLoadGlobal interaction. That's orthogonal to the other states that I described, giving a total of six |

Global	StoreLocal	LoadGlobal	Use
√	X	√	Default permission for heap and globals
X	X	X	Heap / global / stack objects with deep no-capture (or stack objects that want to avoid being used to leak other stack objects
X	X	√	Heap / global / stack objects with shallow no-capture (pointers, for example an array of things to capture, such as an array of heap objects that you want the caller to be able to capture references to).
√	X	X	Heap objects that have a surprising no-capture property (you may capture the pointer, but not interior pointers). We don't currently use this, there are some hypothetical use cases such as ring buffers for one-shot invocation.
X	√	√	Default stack (and register-save area) permissions
X	√	X	Stack objects with a deep no-capture guarantee
√	√	X	Invalid, would violate thread isolation
√	√	√	Invalid, would violate thread isolation

I am not sure that all of the valid ones here can be represented. I wouldn't mind too much if we lost the Global & !StoreLocal & !LoadGlobal one, since its uses are a bit weird.

[LawrenceEsswood]

@davidchisnall The intent is that only the Global & !StoreLocal & !LoadGlobal from your "desirable" table would be lost (specifically because clearing LG in this encoding requires clearing G). The rest should be possible.

@arichardson I am happy with what is currently here, but I still think there is a missing permission that could be specified with the others here that I feel is a logical completion of these control flow bits, and by design costs no extra encoding bits here (As "E" controls all deep properties in this encoding).

LM is a deep version of W.
LL is a deep version of Level
??? is a deep version of SL

Calling it LSL (LoadStoreLocal); it is the bit to allow "Deeply non-capturING". As opposed to LL (LG as it was previously known) which makes something "Deeply non-capturable".

CHERIoT, simply by construction, does not allow any (unsealed) capabilities on their Heap/Global areas that has the SL bit (@nwf / @davidchisnall you may wish to fact check that statement). Thus, they enforce the transitive property that nothing loaded by these non-SL capabilities locations has SL. LSL would, for this use case, not make any difference because the property it enforces is true by construction.

However, I maintain the ability to quickly make a structure non-capturing (without needing assumptions about its construction) is useful. It allows delegating structures that are otherwise capturing in a way that means we don't have to search them after the delegation. The stack and register saves are very flat structures, and their life-cycles easy to reason about, but in the wider scope of all the different uses we imagine for Local/Global doing things by construction will be harder. We may not wish to mutate structures before declaring we are sure they cannot capture local things. LSL allows flipping a bit and knowing that the required property that a structure cannot be used to captured is true.

@nwf on your [0], I raised this before, but CheriOT's "Zeroizing the stack between the caller's high water mark" being sufficient. This really only works if the callee does not get pointers past that water mark that can SL. Which it does, typically via arguments. Say you wanted to guarantee that a callee does not put pointers to its own stack frame (or another to some non-capture object) within the callers frame. (without also searching the entirety of the callers frame). how do you currently do that? If you strip SL from such an argument that points to the callers stack, it may still be used to load a capability with SL, which in turn could stash a local thing. Would LSL not be a really useful knob to have here?

Like multiple levels, I don't think anything specified here prevents LSL being introduced at a later time, but I do think it is a logical completion. All the other permissions to do with movement of capabilities can have deep properties, why not SL?

And, because no review can be made without bike-shedding: L for Load and Level is getting confusing. I liked E.

[andresag01]

And, because no review can be made without bike-shedding: L for Load and Level is getting confusing. I liked E.

We also use E for Exponent in the description of the bounds encoding.

Its also interesting that we use Load for LoadMutable and Store for StoreLocal, but then we have Read and Write permissions...

[arichardson]

Split out into a separate extension and allocated RV32 encoding - still needs some cleanup but hopefully better than the previous version.

[arichardson]

Updated, hopefully this addresses the outstanding comments. I plan to create a new pull request for a "load-store-local" that can be used for a deep variant of store-local, but since this has not been validated in software yet I did not feel like including it in the base spec for now.

[andresag01]

Thanks for the changes! I just made some wording suggestions and typo/formatting fixes.