detection of out of range top #521
Conversation
src/cap-description.adoc
Outdated
|
|
||
| These cases are computationally expensive to detect without expanding the bounds, therefore | ||
| all instructions such as <<CBLD>> which expand bounds and output a capability will clear | ||
| the output tag if the top bound is out of range. |
There was a problem hiding this comment.
I don't understand this point. No such capability is given to you in the initial system state, so of course CBLD must ensure that it doesn't give you back one of these, but that's by virtue of it never being a subset of an existing capability?
There was a problem hiding this comment.
this is like the malformed bounds case, and so I'd like (at least the option of) detagging if such a thing is observed on either input of CBLD, just like we do for malformed bounds, reserved bits set etc...
There was a problem hiding this comment.
@tariqkurd-repo : Could you provide an example situation you are thinking that CBLD would produce a capability that has this property? (i.e. its top > 2^MXLEN and is tagged).
As @jrtc27 explained, CBLD will only ever output capabilities that have equal or smaller bounds than the input capability to maintain the property that software cannot gain permissions it did not have. So, if at reset the most permissive/powerful capability provided to software is the infinite capability, then CBLD should never return a capability that is tagged and has top > infinite_cap.top.
There was a problem hiding this comment.
These are currently (mostly) undocumented malformed bounds cases, and there are many of them.
They can only be caused by fault injection or bugs e.g. the tag cache attaching the wrong tag, and so should be filtered out.
They are too expensive to detect directly from the bounds, but trivial if the bounds are expanded.
Strictly speaking nothing needs to change in the hardware as they are impossible cases, just like reserved bits set or bad permissions.
The objective is to get formal verification to work allowing any bit pattern against the design, and this is one of the awkard cases, so we need to choose an approach.
src/insns/cadd_32bit.adoc
Outdated
| @@ -48,7 +48,8 @@ For <<CADD>>, the address is incremented by the value in | |||
| For <<CADDI>>, the address is incremented by the immediate value | |||
| `imm`. | |||
|
|
|||
| include::malformed_clear_tag.adoc[] | |||
| NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <<section_cap_malformed,malformed>>, | |||
There was a problem hiding this comment.
Why is ADD singled out? (Well, and SHxADD too, by virtue of their special fragment file not being updated)
There was a problem hiding this comment.
because they don't expand the bounds, so for cheaper implementation we're only including instructions which do expand the bounds
There was a problem hiding this comment.
They still need to perform a representability check
There was a problem hiding this comment.
this is true, but don't expand the bounds. A functional unit which does CADD/CADDI doesn't need to do anything with the bounds, and the expansion is expensive just for this check.
If the expansion has already been done then the check is cheap.
Signed-off-by: Tariq Kurd <[email protected]>
if element zero is masked then don't take a cheri fault
Some minor revisions that I found when scrolling through the document.
they need to be updated on all exceptions, not just CHERI ones --------- Signed-off-by: Tariq Kurd <[email protected]>
Move the note after the two sub-items to ensure asciidoc renders the document correctly. Fixes: riscv#523
Replace the ascii art with the bounds decoding diagram to make it clear
how they are computed and what the resulting width of top and base.
This PR replaces this:
```
top: t = { {1'b0, a[MXLEN - 1:E + MW]} + ct, T[MW - 1:0], {E{1'b0}} }
base: b = { a[MXLEN - 1:E + MW] + cb, B[MW - 1:0], {E{1'b0}} }
```
With the bytefield figures in the attached image.
<img width="694" alt="Screenshot 2025-02-06 at 19 21 42" src="https://github.com/user-attachments/assets/521e4239-f23d-4bd2-b9a0-e242cf35cc41" />
Add a note indicating that capability stores may trap in future extensions when the authorizing capability does not grant capability write permissions. Also remove outdated TODO. Fixes riscv#476
Suggestions about how to handle the malformed caps which have an out of range top, which are difficult to detect without expanding the bounds
@PeterRugg
fixes #522