Require store local when storing return sentries (#64)

* Belatedly fix StoreCapImmediate docs

We no longer throw exceptions for !SL authorities storing !G capabilities, just
clear the tag.

* Require store local when storing return sentries

Backwards control-flow arcs should ideally be confined to the stack and register
save areas.  Conveniently, we have mechanism in the RTOS to identify exactly
those areas of memory, with capabilities bearing `SL` (store local) permission.
And, after #54, the ISA has
mechanism for identifying backwards control-flow arcs, with the two return
sentry types.  We should have capability store impose the requirement for `SL`
in the authorizing cap if the cap being stored is a return sentry.

Credit where it's due: this is Robert's idea, originally suggested in the
obviously-wrong-in-retrospect
#63 ("Have CJALR create !G
sentries?").

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

* Review feedback

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

---------

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

Author: 3 people

archdoc/chap-changes.tex

@@ -6,7 +6,7 @@ \chapter{Version history}
 \begin{description}
 \item[0.5] The version released as technical report MSR-TR-2023-6: \emph{CHERIoT: Rethinking security for low-cost embedded systems}, February 2023\footnote{\url{https://aka.ms/cheriot-tech-report}}.
 \item[0.6] The current, under-development version of the ISA. The following changes have been made since the previous released version:
-    \begin{description}
+  \begin{description}
     \item[\ghissue{20}, \ghpr{26}] Capability stores now clear the tag of the stored value instead of raising an exception in case of a store-local violation
     (i.e. an attempt to store a non-global capability via a capability without the store-local permission).
     Tag clearing is preferable for software because it removes the possibility of a trap when copying untrusted inputs.
@@ -37,9 +37,11 @@ \chapter{Version history}
           Software accepting sealed capabilities must be prepared to receive local (that is, \cappermG-lacking) variants,
           even if none were ever explicitly constructed.
       \end{description}
-    \end{description}
     \item[\ghissue{15}, \ghpr{49}] Document stack high water mark.
     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) will store the capability with the tag cleared.
+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.
 \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,6 +487,9 @@ \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

@@ -860,6 +860,10 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12))
  * The capability located in memory at *cs1*.**address** $+$ *imm* is
  * 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.
+ *
  * ## Exceptions
  *
  * An exception is raised if:
@@ -868,8 +872,6 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12))
  *   - *cs1*.**perms** does not grant **Permit_Store**.
  *   - *cs1*.**perms** does not grant **Permit_Store_Capability** and
  *     *cs2*.**tag** is set.
- *   - *cs1*.**perms** does not grant **Permit_Store_Local_Capability**,
- *     *cs2*.**tag** is set and *cs2*.**perms** does not grant **Global**.
  *   - *cs1*.**address** $+$ *imm* $\lt$ *cs1*.**base**.
  *   - *cs1*.**address** $+$ *imm* $+$ **CLEN** $/$ 8 $\gt$ *cs1*.**top**.
  */
@@ -903,7 +905,10 @@ function clause execute StoreCapImm(cs2, cs1, imm) = {
       match (eares) {
         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));
+          let stored_val =
+              clearTagIf(cs2_val, not (auth_val.permit_store_local_cap) &
+                          ( not(cs2_val.global)
+                          | isCapBackwardSentry(cs2_val) ));
           let res : MemoryOpResult(bool) = mem_write_cap(addr, stored_val, false, false, false);
           match (res) {
             MemValue(true)  => RETIRE_SUCCESS,