Remove reverse sentry pseudolocality

archdoc/chap-changes.tex

@@ -41,7 +41,5 @@ \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[\ghpr{64}] Attempting to store a ``backwards-edge'' sentry through an authorizing cap lacking \cappermSLC will clear the tag of the stored value.
-    This enables the RTOS to confine ``backwards-edge'' sentries to the stack and register spill area.
   \end{description}
 \end{description}

archdoc/chap-cheri-riscv.tex

@@ -327,7 +327,7 @@ \subsection{Capability permissions}
 It is intended to be used as a software defined permission.
 \item[GL] If \cappermG is set then this capability is global and can be stored anywhere, otherwise it is local and may be stored only via capabilities with the \cappermSLC permission.
 \item[SL] If \cappermSLC is set (along with \cappermS and \cappermMC) then any capability may be stored via this capability.
-Otherwise, attempting to store a local capability (with GL unset) or a backwards sentry (see \cref{sec:sealing}) will store the capability with the tag cleared.
+Otherwise, attempting to store a local capability (with GL unset) will store the capability with the tag cleared.
 \item[LM] If \cappermLM is not set then any tagged capabilities loaded via this capability will have SD and LM cleared.
 Thus, if SD and LM are cleared on a capability then it, and any capability loaded via it (including via indirection), will be read-only.
 This is useful for delegating a read-only pointer to a data structure, for example to enforce a language level transitive \asm{const}.
@@ -487,9 +487,6 @@ \subsection{Sealed capabilities}
   \end{tabular}
 \end{center}
 
-As an additional special case, \insnriscvref{CSC} will require an authority with \cappermSLC to store a backwards sentry (that is, a capability sealed with type 4 or 5).
-This allows the RTOS to confine backward sentries to stacks and register store areas.
-
 \subsection{Capability bounds}
 \label{sec:bounds}
 

src/cheri_insts.sail

@@ -862,8 +862,8 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12))
  * replaced with capability register *cs2*.
  *
  * The stored capability will have its tag forcibly cleared if *cs1*.**perms**
- * does not grant **Permit_Store_Local_Capability** and either *cs2*.**perms** does not
- * grant **Global** or *cs2* is a backwards sentry.
+ * does not grant **Permit_Store_Local_Capability** and *cs2*.**perms** does not
+ * grant **Global**.
  *
  * ## Exceptions
  *
@@ -907,9 +907,7 @@ function clause execute StoreCapImm(cs2, cs1, imm) = {
         MemException(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
         MemValue(_) => {
           let stored_val =
-              clearTagIf(cs2_val, not (auth_val.permit_store_local_cap) &
-                          ( not(cs2_val.global)
-                          | isCapBackwardSentry(cs2_val) ));
+              clearTagIf(cs2_val, not (auth_val.permit_store_local_cap) & not (cs2_val.global));
           let res : MemoryOpResult(bool) = mem_write_cap(addr, stored_val, false, false, false);
           match (res) {
             MemValue(true)  => RETIRE_SUCCESS,