From 9561ffff9b238294f75ba8fcb91f77f7edcb4597 Mon Sep 17 00:00:00 2001
From: Alexander Richardson <alexrichardson@google.com>
Date: Fri, 1 Nov 2024 16:10:14 -0400
Subject: [PATCH] Clarify interaction of levels with sealed capabilities (#439)

Sealed capabilities should only have their `CL` changed, but not the
`EL` permission.

See also https://github.com/CHERIoT-Platform/cheriot-sail/issues/14

Co-authored-by: Tariq Kurd <tariq.kurd@codasip.com>
---
 src/cap-description.adoc         |  2 ++
 src/insns/atomic_exceptions.adoc |  3 ++-
 src/insns/load_tag_perms.adoc    |  3 +++
 src/level-ext.adoc               | 18 +++++++-----------
 4 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/cap-description.adoc b/src/cap-description.adoc
index 6bfef8dd..bb57434f 100644
--- a/src/cap-description.adoc
+++ b/src/cap-description.adoc
@@ -308,6 +308,8 @@ around. The only way of clearing the type bit of a capability is by rebuilding
 it via a superset capability with <<CBLD>>. {cheri_base_ext_name} does not offer
 an unseal instruction.
 
+NOTE: The <<section_cap_level>> field can be reduced even if the capability is sealed, see <<cap_level_load_summary>>.
+
 For code capabilities, the sealing bit is used to implement immutable
 capabilities that describe function entry points, known as sealed entry (sentry) capabilities. Such capabilities can be leveraged
 to establish a form of control-flow integrity between mutually distrusting code. A program may jump to a
diff --git a/src/insns/atomic_exceptions.adoc b/src/insns/atomic_exceptions.adoc
index 0e1f8031..c3cdb9fe 100644
--- a/src/insns/atomic_exceptions.adoc
+++ b/src/insns/atomic_exceptions.adoc
@@ -8,7 +8,8 @@ If <<c_perm>> is not granted then store the memory tag as zero, and load `cd.tag
 +
 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 the <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final 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>> restricting the <<section_cap_level>> to the level of the authorizing capability is performed.
+If `cd` is not sealed, this implicit <<ACPERM>> also clears <<el_perm>> to obtain the final permissions on `cd` (see <<cap_level_load_summary>> and <<LC>>).
 +
 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 (see <<SC>>).
 endif::[]
diff --git a/src/insns/load_tag_perms.adoc b/src/insns/load_tag_perms.adoc
index db1323f0..b3fdd6c3 100644
--- a/src/insns/load_tag_perms.adoc
+++ b/src/insns/load_tag_perms.adoc
@@ -5,6 +5,9 @@ The tag value written to `cd` is 0 if the tag of the memory location loaded is
 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 the <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd`.
++
+If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> restricting the <<section_cap_level>> to the level of the authorizing capability is performed.
+If `cd` is not sealed, this implicit <<ACPERM>> also clears <<el_perm>> to obtain the final permissions on `cd` (see <<cap_level_load_summary>>).
 
 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.
diff --git a/src/level-ext.adoc b/src/level-ext.adoc
index e8711721..14e1dbb4 100644
--- a/src/level-ext.adoc
+++ b/src/level-ext.adoc
@@ -122,20 +122,16 @@ NOTE: A capability with <<section_cap_level,CL>>=1 is _global_ and with <<sectio
 
 NOTE: if W=0 or C=0 then SL is irrelevant
 
-.{cheri_levels_ext_name} `LVLBITS=1` summary table for loaded capabilities
-[#cap_level_load_summary,width="100%",options=header,align=center,cols="1,1,1,1,1,6"]
+.{cheri_levels_ext_name} additional rules for loading capabilities
+[#cap_level_load_summary,width="100%",options=header,align=center,cols="1,1,1,1,1,1,6"]
 |==============================================================================
-   4+|Auth cap field             | Data cap field |
-    h|*R*   h|*C* h|*EL* h|*CL* h| Tag           h|Action
-.5+.^|1 .5+.^| 1   | 1    | X    | X              |Load data capability unmodified
-              .4+.^| 0    | 1    | 1              |Load data capability with EL=0
-                          | 1    | 0              |Load data capability unmodified
-                     .2+.^| 0    | 1              |Load data capability with CL=0,EL=0
-                                 | 0              |Load data capability unmodified
+   4+|Auth cap field                  2+| Data cap field |
+    h|*R*   h|*C* h|*EL*      h|*CL*   h| Tag h| Sealed h|Action
+.2+.^|1 .2+.^| 1 .2+.^| 0 .2+.^| X .2+.^| 1    | Yes     |Load data capability with `CL=min(auth.CL, data.CL)`, EL unchanged
+                                               | No      |Load data capability with `EL=0, CL=min(auth.CL, data.CL)`
+   6+| All other cases                                   |Load data capability with EL, CL unmodified
 |==============================================================================
 
-NOTE: if R=0 or C=0 then EL and CL are irrelevant
-
 [#section_ext_cheri_multiple_levels]
 === Extending {cheri_levels_ext_name} to more than two levels
 When `LVLBITS>1`, the behaviour of <<ACPERM>> can no longer use masking to adjust the <<section_cap_level>> or <<sl_perm>>, but instead must perform an integer minimum operation on those `LVLBITS`-wide fields.