ACPERM and levels

[LawrenceEsswood]

The Zcherilevels section states the capability level should be modified by ACPERM. However, ACPERM currently always tag clears if values are sealed. This is somewhat contradictory with how the implicit ACPERM happens on loads and stores, where the spec says:

"The Capability Level (CL) field can be reduced even if the capability is sealed, see Table 31."

I think we should bring these two in line and have ACPERM just be aware that some bits are not protected by sealing.

Currently the description of the last step of ACPERM is:

Set cd.tag=0 if cs1 is sealed or if any reserved fields of cs1 are set.

I propose we change this to:

Set cd.tag=0 if cs1 is sealed _and any protected permissions have changed_ or if any reserved fields of cs1 are set.

Without Zcherilevels all permissions are "protected". Level is unprotected (and we can extend the definition as more fields appear).

If we do have Zcherilevels, it is now possible to make a sealed capability local without having to store/load it back. For instance "acperm out, in, ~GLOBAL".

More importantly, I think this should be in the base spec as well so that binaries can be portable between platforms that do and do not have levels ("acperm out, in, ~GLOBAL" would become a move on such platforms, rather than an untag).

[jrtc27]

I think this just comes back to what I was saying the other day with Alex, levels aren't permissions so shouldn't be shoehorned into ACPERM, just as we don't try to do the same with M.

[LawrenceEsswood]

Conceptually I agree. But we do want to both burn instruction space, and require longer programs (as we expect changing level + EL concurrently to be an expected operation) just because it seems neater philosophically? Practically, ACPERM does fit the bill with a small tweak.

[jrtc27]

The permissions bit mask is also an encoding space you're burning through, and on RV32 that's just 32 bits...

[LawrenceEsswood]

True, but not the immediate in the instruction. The space for loading constants is already spent, well before CHERI.

And, lets be honest, are we ever even going to remotely approach 32 architectural permissions for RV32? They would need to be very restricted in how they combined with existing permissions (possibly just appearing on their own) for that 32-bit architectural view to ever run out before the format limits first.

[nwf]

FWIW, CHERIoT explicitly permits clearing G on sealed caps via its candperm; see CHERIoT-Platform/cheriot-sail#83

[arichardson]

I think we should either make this change to permit ACPERM on sealed caps if only the level was changed or introduce another instruction to get and restrict levels. But that is rather invasive and would need more design work, so IMO using the CHERIoT solution would be best.

[LawrenceEsswood]

Worth noting that CheriOT took a subtly different direction than what I proposed in my original post. They went with any attempted change clears tag (i.e. based only on the mask), rather than the change actually happening (i.e. based on comparing new and old permissions)

@nwf was the choice arbitrary, or is there a good reason to go the CheriOT direction?

[rmn30]

Worth noting that CheriOT took a subtly different direction than what I proposed in my original post. They went with any attempted change clears tag (i.e. based only on the mask), rather than the change actually happening (i.e. based on comparing new and old permissions)

Not sure exactly what you mean here. We want to fail secure rather than failing open. The restricted mask is slightly easier to implement in hardware than an xor and compare on the before and after perms although that is not that significant.

[LawrenceEsswood]

@rmn30 What I meant was actually the difference between option 1 and 2 in the linked CheriOT discussion.

It seems like the committed text went for (1), you indicated a software preference for (2). I don't think either is failing safe, but I do agree that (1) is slightly simpler to implement.

I would suggest that (2) is a more forward looking choice, however.

Imagine a future permission (not yet named, call it F), that you would not expect a typical capability in the base spec to implicitly have. Further, imagine F is, like G, one of these permissions that is not meant to be covered by sealing.

If we went with Option (1), then software written to strip F on platforms that have it would not be backwards compatible to platforms that do, because the set of bits allowed to be 0 in the andperm mask are different between platforms.

Option (2) means that there is binary compatibility between the two. I can write the "strip F if it happens to exist" sequence without having to worry this will untag on some platforms but not on others.

Specifically for Zcherilevels, we could allow not having G in the mask now (even if you don't have cherilevels), but we don't know what bits like F we might add in the future. I see no security problem saying that candperms that don't change any permissions are equivalent to moves.

[nwf]

Whoop, I see I missed being tagged here. Sorry!

The choice was not completely arbitrary, though I suspect we could live with either option. Summarizing the PR discussion, we think it's reflective of a programmer error to try to clear non-GL bits on a sealed cap, and we'd rather that that induce a trap (later, when the cap is used, admittedly) every time rather than only if it happens to clear a set bit under seal.

[arichardson]

I believe we should also permit changing Global using ACPERM. Regarding the choice of only permitting a fixed mask with all-ones except for CL (Global), I prefer the more flexible definition of permitting the operation if only CL was affected by ACPERM rather than hardcoding the mask. I don't believe this adds huge HW complexity.

So in summary, I'd vote for permitting level change, but instead of following the rigid mask == -1 except for GL, we say this is permitted on sealed caps if the only bits affected are the level bits, i.e. option 2) of CHERIoT-Platform/cheriot-sail#83.

@nwf since this is a superset of the current CHERIoT behaviour, are you happy with that approach?