From b48c50e2249cf60e422923f48222a81467356062 Mon Sep 17 00:00:00 2001 From: Tariq Kurd Date: Wed, 5 Feb 2025 15:03:30 +0100 Subject: [PATCH] detection of out of range top --- src/cap-description.adoc | 13 +++++++++++++ src/insns/cadd_32bit.adoc | 3 ++- src/insns/cbld_32bit.adoc | 2 +- src/insns/malformed_clear_tag.adoc | 1 + src/insns/scss_32bit.adoc | 1 + 5 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index 1cbc126a..3d9538d9 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -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 <> 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 <> which expand bounds and output a capability will clear +the output tag if the top bound is out of range. + + [#section_cap_malformed] ===== Malformed Capability Bounds @@ -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 <>. +. The <> 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 diff --git a/src/insns/cadd_32bit.adoc b/src/insns/cadd_32bit.adoc index 2b269e13..4b67a5e0 100644 --- a/src/insns/cadd_32bit.adoc +++ b/src/insns/cadd_32bit.adoc @@ -48,7 +48,8 @@ For <>, the address is incremented by the value in For <>, 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 <>, +or if any of the reserved fields are set. Exceptions:: include::require_cre.adoc[] diff --git a/src/insns/cbld_32bit.adoc b/src/insns/cbld_32bit.adoc index 7ba1eefb..dd1e7867 100644 --- a/src/insns/cbld_32bit.adoc +++ b/src/insns/cbld_32bit.adoc @@ -30,7 +30,7 @@ Copy `cs2` to `cd` and set `cd.tag` to 1 if . `cs2` 's permissions and bounds are equal to or a subset of `cs1` 's, and . `cs2` 's <> 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 <>, and all reserved fields are zero, and +. `cs2` 's bounds are not <>, and all reserved fields are zero, and the <> is in range, and . `cs2` 's permissions could have been legally produced by <>, and . All reserved bits in `cs2` 's metadata are 0; diff --git a/src/insns/malformed_clear_tag.adoc b/src/insns/malformed_clear_tag.adoc index 84a7009c..d68595d1 100644 --- a/src/insns/malformed_clear_tag.adoc +++ b/src/insns/malformed_clear_tag.adoc @@ -1,2 +1,3 @@ NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <>, +the <> is out of range, or if any of the reserved fields are set. diff --git a/src/insns/scss_32bit.adoc b/src/insns/scss_32bit.adoc index 17c882ac..ae63c99e 100644 --- a/src/insns/scss_32bit.adoc +++ b/src/insns/scss_32bit.adoc @@ -29,6 +29,7 @@ Description:: . `cs2` 's <> 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 <>, and +. neither `cs1` or `cs2` have the <> 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 <>