When should bit patterns of the cap meta data be preserved for untagged caps?

[vmurali]

TL;DR: Can I change the bit patterns of an untagged cap whenever I use any cap-modifying-instruction on that cap?

Detailed question:

It is unclear what bit patterns should be kept intact when storing a cap back into the memory, especially if one keeps the expanded caps for PC (see CHERIoT-Platform/cheriot-sail@0185917; this necessarily needs expanded caps for PC; otherwise, one has to store previous PC and make sure that a new Jump address is in the same representable region as the previous PC's cap) and registers.

The need for preserving the bit pattern arises because multiple combinations of T, B and E represent the same cap (for instance, when T = 1, B = 0, E = 1 is the same bounds as T = 2, B = 0, E = 0).

CLC and CSC are forced to keep the bit patterns for untagged caps because they are used in memcpy (since we don't have a language level distinction between caps and data). This leads to corner cases which are troublesome:

For instance, if one does a CAndPerm and the permissions remain intact, and if it were an untagged cap, should a later CSC maintain the original bit pattern for T, B and E?

In general, if an instruction is supposed to change some fields of the cap, but the specific values keep the value of those fields unchanged, can the bit pattern of T, B and E change?

What if the values of the other fields change, but CSetBounds was not used? What if CIncOffset is used on an untagged cap?

[davidchisnall]

That’s an interesting question. I don’t believe anything in software requires untagged capabilities if you modify them. The memcpy requirement is specifically for things that are only loaded and stored but not modified in registers. The other requirement is that, after a tag-clearing operation, the cget* instructions should hopefully give something useful for debugging.

I believe cincoffset on an untagged capability modifies only the lower bits (so that it can be used for add on an intptr_t). I also believe csetbounds on an untagged thing does not change the top fields. Candperm should not modify anything except for the permissions field.

I presume that you have in mind a microarchitecture that keeps registers in a [partially] expanded state for faster operations and decompresses later? We did have an earlier CHERI prototype that did this and hit a number of corner cases, which is part of the reason that so much later work went into ensuring that the capability manipulation instructions can be done on the compressed representation. I would expect that such an implementation would keep the original bounds encoding around until it did a bounds-manipulation instruction and then recompress into some canonical form. I believe the specification permits this and requires that the bounds remain in a canonical form. @rmn30?

[davidchisnall]

Can an implementation store only compressed caps (and not the expanded caps) for PCC?

I believe that we should permit this.

"Exceptionally difficult" because one is forced to store the previous compressed PCC, in addition to current compressed PCC, and representability check (or similar) has to be performed w.r.t. previous compressed PCC in the fetch stage.

I am not sure that I quite follow this. If you are storing only compressed capabilities then you need to forward the old PCC to wherever you do the PCC update that isn't a jump-register. If you store the expanded bounds then you will see the bounds check fail and then will reconstruct bounds that may not be the same bit pattern as the original and insert them into the (untagged) capability in MEPCC, but that seems to be the same as the next point:

The issues related to preserving bit-patterns in cap arises because one is forced to store expanded caps. They will go away if the spec is changed to make it easy to work with compressed caps.

I believe any operation that changes the address is intended to permit canonicalise the bounds, but is not required to. We can't easily express that in Sail, but (assuming @rmn30 has no objections) I don't see a problem with permitting both modes in Sail with a configuration switch and clarifying the prose description to state that either is permitted.

If Sail were a better ISA description language, then we'd specify this as a symbolic value that must match the bounds of the original PCC.

I definitely don't wish to preclude implementations that store the bounds of PCC expanded (or partially expanded) because, to date, that's all CHERI implementations (MIPS, RISC-V and Arm) that have used a compressed encoding. Permitting implementations to not expand PCC may be cleaner for verification and so we need to ensure that the expansion is as unobservable as possible at the architectural level.

[rmn30]

On a branch / j[al] the Sail leaves PCC unmodified, including its address, and only updates a separate PC register (an integer). The subsequent instruction fetch uses the address in PCC to compute PCC base and top and checks that the instruction fetch from PC is in bounds. There's no representability problem because the we have the original PCC address, which is only set when installing a new PCC (on jalr / mret / exception). We might face a representability problem when combining PCC and PC to put in MEPCC, which is why we now always clear the tag of MEPCC on instruction fetch bounds exceptions (even if the result would have been representable, a choice I made to avoid having to do a representability check -- we could reverse if @kliuMsft says it's OK). I don't think we want to do a representability check in jumps or branches as the whole point of CHERIoT-Platform/cheriot-sail#23 was to be able to delay the check until instruction fetch. Maybe a representability check on just the new PC would be slightly cheaper than a bounds check on newPC..newPC+2 as it doesn't require an add, but that is one for @kliuMsft .

[vmurali]

I am not sure that I quite follow this. If you are storing only compressed capabilities then you need to forward the old PCC to wherever you do the PCC update that isn't a jump-register.

Consider the snippet (not real assembly instructions, but explicit addresses; all instructions are 32 bits):

# Current PCC: B = 0, T = 511, E = 0, addr = 504, tag = 1
504: cjump PCC+12 # next PCC.addr = 516, which is not representable
508: add x7 = x8 + x9
512: add x4 = x5 + x6
516: add x1 = x2 + x3

The time sequence of the trace is as follows:

• Time 0: Fetch instruction in address 504. Check for in-bounds w.r.t. B=0, T=511, E=0, addr = 504, length = 4 bytes. It passes in-bounds check for addresses 504 and 507 w.r.t. B=0, T=511, E=0 because base = 0 and top = 511.
• Time 1: Execute cjump PCC+12. Change PCC.addr to 516 without checking if 516 is representable w.r.t. B=0, T=511, E=0, addr=504. Old PCC which had addr = 504 is lost.
• Time 2: Fetch intruction in address 516. Check for in-bounds w.r.t. B=0, T=511, E=0, addr = 516, length = 4 bytes. It passes in-bounds check for addresses 516 and 519 w.r.t. B=0, T=511, E=0 because now base = 512 and top = 1023 as addr = 516. This is wrong. To fix this, one needs to recalculate the previous PC's bounds, namely, when B=0, T=511, E=0, addr=504 to calculate oldBase = 0 and oldTop = 512. Only then will it fail the in-bounds check.

EDIT: Changed the starting address to make sure we don't hit top.

[nwf]

Ah, I see; my confusion was around "next", and jal has two "next" PCCs to consider: the jump target and the address-adjacent instruction. Sorry for misunderstanding.

I think I'm not going to say anything very novel in the below wad of text, which is mostly an attempt to check my understanding and, if so present, offer perhaps a slightly different perspective. In any case...

I believe the fundamental issue has little to do with compressedness of representation and is in

Time 1: Execute cjump PCC+12. Change PCC.addr to 516 without checking if 516 is representable

I would argue that it is almost never correct to blindly assign into any of a capability's fields, compressed or not. Looking at the other setters afforded to users of capabilities,

• Tag updates are always AND,
• CSeal is a function of the old, new, and permitted otypes,
• CAndPerm is a logical AND on the expanded form (== the literal form in Big CHERI) (and depends on the old otype),
• CSetAddr/CIncOffset need T, B, E, and a_{mid} as well as the old otype

PCC is only special because we make multiple consecutive requests under its authority, those requests need to be fast, we have the invariant that its otype is "unsealed", and we need its permissions only with AUIPCC because we also enforce that its permissions included Execute. I think integer-offset jumps must induce a bounds check somewhen between the jump committing and the target instruction beginning execution.

Speaking as emphatically not a hardware person, there are several ways to do that, and these have different implications for the value reported into MEPCC, but I think the salient point there is that the exact value does not matter very much from a security perspective, subject to the constraint that if its tag is set then the capability must be as if it were derived from the PCC holding the jump instruction. I believe this ambivalence of security concerns extends as far as whether it is the jump instruction's address or the jump target's that is reported in MEPCC.

Compressed representation enters only in that operating with expanded PCC bounds allows for that bounds check to happen as late as fetching the jump target, while operating with compressed PCC bounds requires at least a representability check as part of the update. Deferring that representability check and conflating it with the bounds check in fetch would require at least keeping the old PCC's a_mid value, because that's what the CIncOffset operation needs.

[vmurali]

I think integer-offset jumps must induce a bounds check somewhen between the jump committing and the target instruction beginning execution.

I think that's exactly what I am arguing for.. A representability check, rather than a bounds check because that will just satisfy the invariant that at the time of fetch, PC is always representable, and we always need to check if PC, and PC+3 (or PC+1) are in bounds.

• CSetAddr/CIncOffset need T, B, E, and a_{mid} as well as the old otype

We also need $a_{top}$

Compressed representation enters only in that operating with expanded PCC bounds allows for that bounds check to happen as late as fetching the jump target, while operating with compressed PCC bounds requires at least a representability check as part of the update. Deferring that representability check and conflating it with the bounds check in fetch would require at least keeping the old PCC's a_mid value, because that's what the CIncOffset operation needs.

Agreed. (We need both $a_{mid}$ and $a_{top}$.)

[kliuMsft]

I think really the point is more about whether the "current" pcc bounds are expanded or compressed. To me the former makes sense as otherwise we may have to do a representability check on every PC movement (including incrementing), which is error-prone and wastes power/gates. In this case, we only update/expand the pcc bounds on "installing" new PCC (CJALR/exceptions/mret). And to me it makes sense to clear pcc tag on bound violations instead of doing a representability check (as we need to do bound check anyway, and if bound checking passes then we know it's representable).

@vmurali in this context, line 4 (PC=516) of your example will result in a fetch violation since we are still runing on the "current" pcc.

[davidchisnall]

Irrespective, as I have mentioned before, you need to clarify this in the spec.

Agreed.

The fact that either you require expanded PCC or you are not raising exception on the instruction that actually generates the exception but on the next instruction requires some commentary in the spec

I believe that, as written, the spec says that a relative branch must generate a new value to be installed in PCC that is equivalent to doing the add on the PCC, and clear the tag if it's not representable. We then fail either the tag or bounds check when we try to fetch that instruction. We can certainly add some more prose here. I don't think that this mandates either a compressed or expanded PCC, it just changes where you need forwarding paths.

@rmn30, is that what the spec actually says, or am I talking nonsense?

[vmurali]

I believe that, as written, the spec says that a relative branch must generate a new value to be installed in PCC that is equivalent to doing the add on the PCC, and clear the tag if it's not representable. We then fail either the tag or bounds check when we try to fetch that instruction.

This is sufficient (EDIT: but I don't think the spec reads that way currently).

[davidchisnall]

I don't think the spec reads that way currently

The Sail model, the prose or both? We should definitely fix either / both.

From an orthogonality perspective, I would like it if:

auipcc $tmp, 0
cincoffset $tmp, $tmp, n-6 # Or whatever the displacement is with compressed instructions
cjr $tmp

And:

j n

Were equivalent in terms of the exception that is raised. This suggests that we should get the tag exception, not the bounds exception, if we jump out of representable bounds, but I don't have a very strong feeling either way.

[vmurali]

The Sail model, the prose or both? We should definitely fix either / both.

Prose. Sail has a different implementation which is consistent with what you wrote.

Were equivalent in terms of the exception that is raised.

Note that CJR raises the exception at CJR, while CJ will be raising it in the next instruction. (I am arguing for identical treatment :) ). But at least with your clarification in the spec prose, the semantics of CJ will be clear, even if it is different from CJR's semantics.

[vmurali]

Here's the latest version of the spec for CJAL and CJALR. I was wrong about CJALR: representability/bounds violation doesn't raise exceptions on CJALR either. But the spec doesn't specify the PCC tag being cleared on representability violations.

[rmn30]

It would have to check for newPC < base and either newPC > top or newPC > representable limit, whichever is either for hardware.

Actually it just has to check newPC is in representable limit for JAL and Branch instructions w.r.t. prevPCC, and for JALR, you need to check if newPC is in the representable limit for the cap in cs1. One doesn't have to worry about newPC+1, newPC+2, etc. For straight line code, it is already representable as I mentioned earlier.

That's exactly what I meant. I'm also giving Kunyan the option of either a check against top (preferable for sw) or against the representable limit depending on which is easier in hw. We definitely need to check against base as it is the lower representable limit.

[vmurali]

Okay, I parsed it as ((newPC < base) and either ((newPC > top) or (newPC > representable limit))

[vmurali]

We definitely need to check against base as it is the lower representable limit.

Oh Okay, you are just expanding the check. Got it.

[rmn30]

My typo didn't help understanding, sorry!