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.

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

Introduce capability levels #355

Merged
merged 8 commits into from
Oct 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 2 additions & 0 deletions src/attributes.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@ endif::[]
:cheri_default_ext_name: Zcherihybrid
// Extension for CHERI PTE bits
:cheri_pte_ext_name: Zcheripte
// Extension for capability levels (flow control)
:cheri_levels_ext_name: Zcherilevels
// Extension for thread identification
:tid_ext_name: Zstid

Expand Down
7 changes: 6 additions & 1 deletion src/cap-description.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ Reserved bits are available for future extensions to {cheri_base_ext_name}.

NOTE: Reserved bits must be 0 in tagged capabilities.

NOTE: The CL field is only present if {cheri_levels_ext_name} is implemented, otherwise it is reserved.

=== Components of a Capability

Capabilities contain the software accessible fields described in this section.
Expand Down Expand Up @@ -102,6 +104,7 @@ The byte-address of a memory location is encoded as MXLEN integer value.
ifdef::cheri_v9_annotations[]
WARNING: *CHERI v9 Note:* The permissions are encoded differently in this
specification.
Additionally, this specification incorporates permissions that were present in Morello and/or CHERIoT but not CHERI v9.
endif::[]

This field encodes architecturally defined permissions of the capability.
Expand Down Expand Up @@ -240,8 +243,10 @@ permission.
| 3 | <<x_perm>>
| 4 | <<asr_perm>>
| 5 | <<lm_perm>>
//| 6 | <<m_bit>>
| 6 | <<el_perm>>^1^
| 7 | <<sl_perm>>^1^
|==============================================================================
^1^ This permission is only supported if the implementation supports <<section_ext_cheri_levels,{cheri_levels_ext_name}>>.

The <<m_bit>> is only assigned meaning when the
implementation supports {cheri_default_ext_name} _and_ <<x_perm>> is set.
Expand Down
10 changes: 7 additions & 3 deletions src/img/acperm_bit_field.edn
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(def left-margin 100)
(def right-margin 100)
(def boxes-per-row 32)
(draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "1" "2" "" "4" "5" "6" "" "" "SDPLEN+5" "" "" "" "" "" "15" "16" "17" "18" "19" "" "" "" "" "" "" "" "" "" "" "" "XLEN-1"])})
(draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "1" "2" "3" "4" "5" "6" "" "" "SDPLEN+5" "" "" "" "" "" "15" "16" "17" "18" "19" "" "" "" "" "" "" "" "" "" "" "" "XLEN-1"])})

(draw-box "Reserved" {:span 13})
(draw-box "R" {:span 1})
Expand All @@ -15,7 +15,9 @@
(draw-box "Reserved" {:span 6})
(draw-box "SDP" {:span 4})
(draw-box "C" {:span 1})
(draw-box "Reserved" {:span 3})
(draw-box "CL" {:span 1})
(draw-box "SL" {:span 1})
(draw-box "EL" {:span 1})
arichardson marked this conversation as resolved.
Show resolved Hide resolved
(draw-box "LM" {:span 1})
(draw-box "W" {:span 1})

Expand All @@ -26,7 +28,9 @@
(draw-box "8" {:span 6 :borders {}})
(draw-box "SDPLEN" {:span 4 :borders {}})
(draw-box "1" {:span 1 :borders {}})
(draw-box "3" {:span 3 :borders {}})
(draw-box "1" {:span 1 :borders {}})
(draw-box "1" {:span 1 :borders {}})
(draw-box "1" {:span 1 :borders {}})
(draw-box "1" {:span 1 :borders {}})
(draw-box "1" {:span 1 :borders {}})
----
5 changes: 3 additions & 2 deletions src/img/cap-encoding-xlen32.edn
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,12 @@
(def left-margin 100)
(def right-margin 100)
(def boxes-per-row 32)
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "1" "2" "" "" "" "" "" "" "9" "10" "11" "12" "" "" "" "" "17" "18" "19" "20" "21" "" "" "24" "25" "" "" "" "29" "30" "31"])})
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "1" "2" "" "" "" "" "" "" "9" "10" "11" "12" "" "" "" "" "17" "18" "19" "20" "21" "" "23" "24" "25" "" "" "" "29" "30" "31"])})

(draw-box "SDP" {:span 2})
(draw-box "AP, M" {:span 5})
(draw-box "Reserved" {:span 4})
(draw-box "CL" {:span 1})
(draw-box "Reserved" {:span 3})
arichardson marked this conversation as resolved.
Show resolved Hide resolved
(draw-box "CT" {:span 1})
(draw-box "EF" {:span 1})
(draw-box "L8" {:span 1})
Expand Down
7 changes: 4 additions & 3 deletions src/img/cap-encoding-xlen64.edn
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,14 @@
(def left-margin 100)
(def right-margin 100)
(def boxes-per-row 32)
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "2" "3" "" "" "" "13" "14" "16" "17" "" "" "25" "26" "27" "28" "" "" "" "" "45" "46" "" "" "51" "52" "53" "56" "57" "" "" "63"])})
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "2" "3" "" "" "" "13" "14" "16" "17" "" "" "25" "26" "27" "28" "" "42" "43" "44" "" "" "" "" "51" "52" "53" "56" "57" "" "" "63"])})

(draw-box "Reserved" {:span 4})
(draw-box "SDP" {:span 2})
(draw-box "M" {:span 1})
(draw-box "AP" {:span 4})
(draw-box "Reserved" {:span 6})
(draw-box "AP" {:span 6})
(draw-box "CL" {:span 1})
(draw-box "Reserved" {:span 3})
arichardson marked this conversation as resolved.
Show resolved Hide resolved
(draw-box "CT" {:span 1})
(draw-box "EF" {:span 1})
(draw-box "T[11:3]" {:span 4})
Expand Down
6 changes: 6 additions & 0 deletions src/insns/acperm_32bit.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,10 @@ The common rules are:
.. Clear <<m_bit>> unless <<x_perm>> is set
. <<lm_perm>> cannot be set without <<c_perm>> being set
.. Clear <<lm_perm>> unless <<c_perm>> is set.
. <<sl_perm>> cannot be set without <<c_perm>> being set
.. Zero <<sl_perm>> unless <<c_perm>> is set.
. <<el_perm>> cannot be set without <<c_perm>> being set
.. Zero <<sl_perm>> unless <<c_perm>> is set.

NOTE: The combination of <<x_perm>> clear and <<m_bit>> set is reserved for future extensions.

Expand All @@ -64,6 +68,8 @@ The MXLEN=32 additional rules are:
[#acperm_bit_field]
include::../img/acperm_bit_field.edn[]

NOTE: The <<el_perm,EL>>, <<sl_perm,SL>> and <<section_cap_level,CL>> fields are only defined if the implementation supports <<section_ext_cheri_levels,{cheri_levels_ext_name}>>.

Exceptions::
include::require_cre.adoc[]

Expand Down
4 changes: 3 additions & 1 deletion src/insns/atomic_exceptions.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@ Requires <<r_perm>> and <<w_perm>> in the authorising capability.
+
If <<c_perm>> is not granted then store the memory tag as zero, and load `cd.tag` as zero.
+
If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the final permissions on `cd` (see <<LC>>).
If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd` (see <<LC>>).
+
If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd` (see <<LC>>).
+
endif::[]
ifndef::cap_atomic[]
Expand Down
10 changes: 4 additions & 6 deletions src/insns/hypv-virt-store-cap.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -19,17 +19,15 @@ include::wavedrom/hypv-virt-store-cap.adoc[]
Store a CLEN+1 bit value in `cs2` to memory as though V=1; i.e., with the
address translation and protection, and endianness, that apply to memory
accesses in either VS-mode or VU-mode. The effective address is the address of
`cs1`. The authorising capability for the operation is `cs1`. The capability
written to memory has the tag set to 0 if the tag of `cs2` is 0 or `cs1` does
not grant <<c_perm>>.
`cs1`. The authorising capability for the operation is `cs1`.

{cheri_int_mode_name} Description::
Store a CLEN+1 bit value in `cs2` to memory as though V=1; i.e., with the
address translation and protection, and endianness, that apply to memory
accesses in either VS-mode or VU-mode. The effective address is the `rs1`. The
authorising capability for the operation is <<ddc>>. The capability written to
memory has the tag set to 0 if the tag of `cs2` is 0 or <<ddc>> does not grant
<<c_perm>>.
authorising capability for the operation is <<ddc>>.

include::store_tag_perms.adoc[]

include::malformed_no_check.adoc[]

Expand Down
7 changes: 6 additions & 1 deletion src/insns/load_tag_perms.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,14 @@ Resulting value of `cd`::
The tag value written to `cd` is 0 if the tag of the memory location loaded is
0 or the authorizing capability (<<ddc>> or `cs1`) does not grant <<c_perm>>.
+
If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the final permissions on `cd`.
If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd`.
+
If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd`.

NOTE: Missing <<lm_perm>> does not affect untagged values since this could result in surprising bit patterns when copying non-capability data.
Similarly, sealed capabilities are not modified as they are not directly dereferenceable.

NOTE: Missing <<el_perm>> also affects the level of sealed capabilities since notionally the <<section_cap_level>> of a capability is not a permission but rather a data flow label attached to the loaded value.
However, untagged values are not affected by <<el_perm>>.

NOTE: While the implicit <<ACPERM>> introduces a dependency on the loaded data, microarchitectures can avoid this by deferring the actual masking of permissions until the loaded capability is dereferenced or the metadata bits are inspected using <<GCPERM>> or <<GCHI>>.
10 changes: 4 additions & 6 deletions src/insns/store_32bit_cap.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -20,16 +20,14 @@ include::wavedrom/storecap.adoc[]
{cheri_cap_mode_name} Description::
Store the CLEN+1 bit value in `cs2` to memory. The capability in `cs1`
authorizes the operation. The effective address of the memory access is
obtained by adding the address of `cs1` to the sign-extended 12-bit offset. The
capability written to memory has the tag set to 0 if the tag of `cs2` is 0 or
`cs1` does not grant <<c_perm>>.
obtained by adding the address of `cs1` to the sign-extended 12-bit offset.

{cheri_int_mode_name} Description::
Store the CLEN+1 bit value in `cs2` to memory. The capability
authorising the operation is <<ddc>>. The effective address of the memory
access is obtained by adding `rs1` to the sign-extended 12-bit offset. The
capability written to memory has the tag set to 0 if `cs2` 's tag is 0 or
<<ddc>> does not grant <<c_perm>>.
access is obtained by adding `rs1` to the sign-extended 12-bit offset.

include::store_tag_perms.adoc[]

include::malformed_no_check.adoc[]

Expand Down
5 changes: 5 additions & 0 deletions src/insns/store_tag_perms.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Tag of the written capability value::

The capability written to memory has the tag set to 0 if the tag of `cs2` is 0 or if the authorizing capability (<<ddc>> or `cs1`) does not grant <<c_perm>>.
+
The stored tag is also set to zero if the authorizing capability does not have <<sl_perm>> set but the stored data has a <<section_cap_level>> of 0.
3 changes: 3 additions & 0 deletions src/introduction.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,8 @@ RISC-V.
{lr_sc_bh_ext_name}:: Addition of <<LR_B>>, <<LR_H>>, <<SC_B>>, <<SC_H>> for more accurate atomic locking as the memory ranges are restricted by using bounds, therefore precise locking is needed.
{cheri_pte_ext_name}:: CHERI extension for RISC-V harts supporting page-based
virtual-memory.
{cheri_levels_ext_name}:: Extension for supporting capability flow control.
This extension allows limiting storing of capabilities to specific regions and can be used e.g. for safer data sharing between compartments.
{tid_ext_name}:: Extension for supporting thread identifiers. This extension
improves software compartmentalization on CHERI systems.

Expand All @@ -107,6 +109,7 @@ CAUTION: The extension names are provisional and subject to change.
|{lr_sc_bh_ext_name} | Stable | This extension is a candidate for freezing
|{cheri_pte_ext_name} | Prototype | This extension is a prototype, software is being developed to use it to increase the maturity level
|{tid_ext_name} | Prototype | This extension is a prototype, software is being developed to use it to increase the maturity level
|{cheri_levels_ext_name} | Prototype | This extension is a prototype, software is being developed to use it to increase the maturity level
|==============================================================================

{cheri_base_ext_name} is defined as the base extension which all CHERI RISC-V
Expand Down
Loading
Loading