CUnseal: permit any in-bound type

FIXES #71

Co-authored-by: Robert Norton <[email protected]>

archdoc/chap-changes.tex

@@ -41,5 +41,8 @@ \chapter{Version history}
     Make it explicitly 16-byte aligned and point out the unaligned write spanning \mshwmb{} corner case, which we do not require hardware to handle.
     \item[\ghpr{54}] Create backward sentries for function returns and add more checks in \rvcheriasminsnref{CJAL}
     Because CHERIoT allows manipulating the status of the interrupt through a function call (and function return) by encoding the interrupt type in the otype, the following attack can occur: A caller calling an interrupt-disabling callee can set the return sentry of the callee to the same callee. This means, the callee will call itself on return all the while operating with interrupts disabled. This will lead to infinite repeated calls to the callee with interrupts disabled, violating availability. This attack can be prevented in CHERIoT by adding two new ``backwards-edge'' sentries and adding more checks on \rvcheriasminsnref{CJALR}.
+    \item[\ghissue{71}, \ghpr{87}] \rvcheriasminsnref{CUnseal} now no longer requires exact equality between sealed input otype and authority address.
+      Instead, it merely requires that the otype of the sealed input is within bounds to yield a tagged result.
+      The address of a sealing-root capability is now meaningful only to \rvcheriasminsnref{CSeal}.
   \end{description}
 \end{description}

src/cheri_insts.sail

@@ -743,7 +743,8 @@ union clause ast = CUnseal : (regidx, regidx, regidx)
  * Capability register *cd* is replaced with capability register *cs1* and is
  * unsealed, using capability register *cs2* as the authority for the unsealing
  * operation. If *cs2*.**perms** does not grant **Global** then *cd*.**perms**
- * is stripped of **Global**. If *cs2* is unable to authorize the unsealing,
+ * is stripped of **Global**. If *cs2* is unable to authorize the unsealing
+ * (because *cs1*.**otype** is not within the bounsd of *cs2*),
  * the **tag** field of *cd* is cleared.
  */
 function clause execute (CUnseal(cd, cs1, cs2)) = {
@@ -754,10 +755,8 @@ function clause execute (CUnseal(cd, cs1, cs2)) = {
   let permitted = cs2_val.tag
                 & isCapSealed(cs1_val)
                 & not(isCapSealed(cs2_val))
-                & (cs2_addr == unsigned(cs1_val.otype))
-                & cs2_val.permit_unseal
-                & (cs2_addr >= cs2_base)
-                & (cs2_addr < cs2_top);
+                & inCapBounds(cs2_val, zero_extend(cs1_val.otype), 1)
+                & cs2_val.permit_unseal;
   let new_global = cs1_val.global & cs2_val.global;
   let newCap = {unsealCap(cs1_val) with global=new_global};
   C(cd) = clearTagIf(newCap, not(permitted));