Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

detection of out of range top #521

Closed
wants to merge 15 commits into from
Closed

detection of out of range top #521

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
b48c50e
detection of out of range top
tariqkurd-repo Feb 5, 2025
055cc30
include cs1 in CBLD
tariqkurd-repo Feb 5, 2025
af587a1
improved xrefs
tariqkurd-repo Feb 5, 2025
d637272
Update src/cap-description.adoc
tariqkurd-repo Feb 5, 2025
45422c8
extend to JALR, load/store/atomic
tariqkurd-repo Feb 5, 2025
09fe69c
new files
tariqkurd-repo Feb 5, 2025
7418714
FoF clarification (#517)
tariqkurd-repo Feb 5, 2025
ec86701
Minor revision (#520)
marnovandermaas Feb 5, 2025
5b2714d
clarify mtval2/stval2/vstval2 handling (#518)
tariqkurd-repo Feb 6, 2025
1baa11a
Fix indentation of sub-items (#524)
arichardson Feb 7, 2025
aabff08
Replace bounds decoding ascii art with bytefield diagram (#526)
andresag01 Feb 7, 2025
d4e2ed3
Write note about traps for capability stores (#528)
andresag01 Feb 7, 2025
024e060
Remove xtdc CSRs zcherihybrid extension (#527)
andresag01 Feb 7, 2025
1ab7e6a
bump version number (#529)
tariqkurd-repo Feb 7, 2025
9d0d3cc
scale back proposal
tariqkurd-repo Feb 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions src/cap-description.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -537,6 +537,18 @@ NOTE: A capability has infinite bounds if E=CAP_MAX_E and it is not
malformed (see xref:section_cap_malformed[xrefstyle=short]); this check is
equivalent to _b_=0 and _t_≥2^MXLEN^.

[#section_cap_malformed_top_gt_inf_top]
===== The Top Bound is Out Of Range

The top bound of the <<infinite-cap>> is defined to be 2^MXLEN^.

There are cases where the decoded bounds of a capability could, in theory, exceed this value.

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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.



[#section_cap_malformed]
===== Malformed Capability Bounds

Expand All @@ -561,6 +573,7 @@ CHERI enforces the following invariants for all valid (i.e., tagged) capabilitie
. The bounds are not malformed.
. No reserved bit in the capability encoding is set.
. The permissions can be legally produced by <<ACPERM>>.
. The <<section_cap_malformed_top_gt_inf_top,top bound must be no greater than 2^XLEN^>>.

A tagged capability that violates those invariants (i.e., a tagged but malformed capability or a tagged
capability with any reserved bit set) can only possibly be caused by
Expand Down
3 changes: 2 additions & 1 deletion src/insns/cadd_32bit.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>>,
Copy link
Collaborator

@jrtc27 jrtc27 Feb 5, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is ADD singled out? (Well, and SHxADD too, by virtue of their special fragment file not being updated)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

because they don't expand the bounds, so for cheaper implementation we're only including instructions which do expand the bounds

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

They still need to perform a representability check

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

or if any of the reserved fields are set.

Exceptions::
include::require_cre.adoc[]
Expand Down
4 changes: 2 additions & 2 deletions src/insns/cbld_32bit.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,13 @@ Description::
Copy `cs2` to `cd` and set `cd.tag` to 1 if

. `cs1.tag` is set, and
. `cs1` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and
. `cs1` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and the <<section_cap_malformed_top_gt_inf_top,top bound is not out of range>>, and
. `cs1` 's permissions could have been legally produced by <<ACPERM>>, and
. `cs1` is not sealed, and
. `cs2` 's permissions and bounds are equal to or a subset of `cs1` 's, and
. `cs2` 's <<section_cap_level>> is equal to or lower than `cs1` 's, and
.. _This is only relevant if {cheri_levels_ext_name} is implemented._
. `cs2` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and
. `cs2` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and the <<section_cap_malformed_top_gt_inf_top,top bound is not out of range>>, and
. `cs2` 's permissions could have been legally produced by <<ACPERM>>, and
. All reserved bits in `cs2` 's metadata are 0;

Expand Down
1 change: 1 addition & 0 deletions src/insns/malformed_clear_tag.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <<section_cap_malformed,malformed>>,
the <<section_cap_malformed_top_gt_inf_top,top bound is out of range>>,
or if any of the reserved fields are set.
1 change: 1 addition & 0 deletions src/insns/scss_32bit.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ Description::
. `cs2` 's <<section_cap_level>> is equal to or lower than `cs1` 's
.. _This is only relevant if {cheri_levels_ext_name} is implemented._
. neither `cs1` or `cs2` have bounds which are <<section_cap_malformed,malformed>>, and
. neither `cs1` or `cs2` have the <<section_cap_malformed_top_gt_inf_top,top bound out of range>>, and
. neither `cs1` or `cs2` have any bits set in reserved fields, and
. neither `cs1` or `cs2` have permissions that could not have been legally produced by <<ACPERM>>

Expand Down
Loading