riscv / riscv-cheri

This repository contains the CHERI extension specification, adding hardware capabilities to RISC-V ISA to enable fine-grained memory protection and scalable compartmentalization.
https://jira.riscv.org/browse/RVG-148
Creative Commons Attribution 4.0 International
47 stars 28 forks source link

Unclear wording of ACPERM rule #415

Open tomaird opened 3 days ago

tomaird commented 3 days ago

The rules for ACPERM includes this for RV32:

Clear X-permission if X-permission and R-permission are set, but C-permission and W-permission are not set.

This is a bit ambiguously worded. It could either mean:

  1. if (X && R && !(C || W) then clear X
  2. if (X && R && !(C && W) then clear X

If it's option 2 (which I think is the most logical reading of it) then there's several encodings which are impossible - encodings 2-3 or 6-7 for quadrant 1:

image

Which is quite a large area of redundant encoding.

However if it's option 1 it's possible to create an a set of permissions that has no encoding. If we have R+C+X+LM permissions (quadrant 1, encoding 2-3) in a capability that we load from memory without LM permission in the authorising cap, then we're supposed to clear the LM permission, which would leave us with R+C+X permissions. If we interpret the above rule as option 1 then we shouldn't clear X, but there is no encoding that exists for R+C+X permissions.

jamie-melling commented 3 days ago

I think the rule needs to look like this: (X && R && ((LM ^ C) || !(C || W))) then clear X Not sure how you'd sensibly express that in a sentence though (other than adding new rules and having ordering dependency on implementing the rules?)

tariqkurd-repo commented 3 days ago

without worrying about the exact rules for a minute - let's see which transitions are affected and what a sensible outcome would be for them:

Quadrant 1:

R,W,C,LM,X,ASR -> R,W,C,X,ASR doesn't exist so will need to map to R,W,X or R,C R,C,LM,X -> R,C,X doesn't exist so will so need to map to R,C R,W,C,LM,X -> R,W,C,X doesn't exist so will need to map to R,W,X or R,C

Quadrant 3:

R,C,LM -> R,C - this one is ok! R,W,C,LM -> R,W,C doesn't exist so will need to map to R,C

so we have 4 cases where only a single mapping possible (R,C), and two where there is a choice between R,W,X and R,C.

From a hardware perspective, always selecting R,C is preferable.

@arichardson @LawrenceEsswood @davidchisnall what makes more sense in these cases?

arichardson commented 2 days ago

The intent of Clear X-permission if X-permission and R-permission are set, but C-permission and W-permission are not set. was that clearing C on from Execute + Cap RO would go to RO in q0 and clearing X on Execute + Data RW goes to Data RW in q0.

@LawrenceEsswood does that match your understanding?

Quadrant 1:

R,W,C,LM,X,ASR -> R,W,C,X,ASR doesn't exist so will need to map to R,W,X or R,C

When clearing LM here, there are no other encodings with ASR, so we have to look at R,W,C,X (almost exists, but that encoding option also has LM), so we have to either clear C to get R,W,X or R,C. We don't have R,W,C (the potential encoding here has an implicit LM due to being in the "elevate" quadrant that implies LM for W).

R,C,LM,X -> R,C,X doesn't exist so will so need to map to R,C R,W,C,LM,X -> R,W,C,X doesn't exist so will need to map to R,W,X or R,C Quadrant 3:

R,C,LM -> R,C - this one is ok! R,W,C,LM -> R,W,C doesn't exist so will need to map to R,C

so we have 4 cases where only a single mapping possible (R,C), and two where there is a choice between R,W,X and R,C.

Also agree with all of these.