Proposed relaxing of cjalr sealing

Attempt at capturing #85

Co-authored-by: Robert Norton <robert.norton@microsoft.com>

archdoc/chap-changes.tex

@@ -41,5 +41,11 @@ \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}.
+      \begin{description}
+        \item[\ghissue{85}, \ghpr{86}] Relaxes the original change to better support code outlining,
+          by allowing \rvcheriasminsnref{CJALR} to create unsealed return addresses
+          when its (output) link register is not \asm{\$cra}.
+          See the discussion in \cref{sec:sealing}.
+      \end{description}
   \end{description}
 \end{description}

archdoc/chap-cheri-riscv.tex

@@ -458,11 +458,11 @@ \subsection{Sealed capabilities}
 The \cotype{} field uses the following values:
 \begin{description}
   \item[0] unsealed
-  \item[1] sealed as sentry
-  \item[2] sealed as interrupt disabling sentry
-  \item[3] sealed as interrupt enabling sentry
-  \item[4] sealed as backward interrupt disabling sentry
-  \item[5] sealed as backward interrupt enabling sentry
+  \item[1] sealed as interrupt inheriting forward sentry
+  \item[2] sealed as interrupt disabling forward sentry
+  \item[3] sealed as interrupt enabling forward sentry
+  \item[4] sealed as interrupt disabling backward sentry
+  \item[5] sealed as interrupt enabling backward sentry
   \item[6-7] executable capability sealed with given \cotype{}
   \item[8] reserved (due to encoding)
   \item[9-15] non-executable capability sealed with given \cotype{}
@@ -477,16 +477,40 @@ \subsection{Sealed capabilities}
   \footnotesize
   \begin{tabular}{|c|c|c|c|}
     \hline
-    \asm{cs1} & \asm{cd} & Used for & Valid \cotype{}s \\
+    \asm{cs1} & \asm{cd} (out \cotype{}s) & Used for & Valid \asm{cs1} \cotype{}s \\
     \hline
-    \asm{\$cra} & \asm{\$cnull} & Function return & Return sentries $(4, 5)$\\
-    $\ne$ \asm{\$cra} & \asm{\$cnull} & Tail call & Unsealed or interrupt inheriting forward sentry $(0, 1)$\\
-    any & $\not\in \{ \text{\asm{\$cnull}}, \text{\asm{\$cra}} \}$ & Function call & Unsealed or interrupt inheriting forward sentry $(0, 1)$\\
-    any & \asm{\$cra} & Function call & Unsealed or forward sentries $(0, 1, 2, 3)$\\
+    \asm{\$cra} & \asm{\$cnull} (n/a) & Function return & Backward sentries $(4, 5)$\\
+    $\ne$ \asm{\$cra} & \asm{\$cnull} (n/a) & Tail call & Unsealed or IRQ inheriting forward sentry $(0, 1)$\\
+    any & $\not\in \{ \text{\asm{\$cnull}}, \text{\asm{\$cra}} \}$ (0) & Code outlining & Unsealed or IRQ inheriting forward sentry $(0, 1)$\\
+    any & \asm{\$cra} (4,5) & Function call & Unsealed or forward sentries $(0, 1, 2, 3)$\\
     \hline
   \end{tabular}
 \end{center}
 
+Thus, ordinary function calls, for which the calling convention is to use \asm{\$cra} as the return register,
+can call any unsealed (executable) capability or forward sentry,
+and will always create backward sentries, suitable for the function return case.
+Tail calls, which must preserve \asm{\$cra} for their callee and do not generate return capabilities of their own,
+are also permitted.
+Last, code \emph{outlining}, the dual of code \emph{inlining}, is supported;
+outlined code may use a specialized calling convention, not using \asm{\$cra} to exit
+(so return from such outlined code looks like a ``tail call'' in the above table),
+especially in cases where the outlined code must preserve \asm{\$cra} for its caller.
+In this case, the \insnriscvref{CJALR} used to enter the outlined code
+will have a \asm{cd} that is neither \asm{\$cnull} nor \asm{\$cra},
+and so will create \emph{unsealed} return capabilities,
+so that all forward sentries in the system must have been built by the RTOS loader.
+(Outlined code that \emph{does} use \asm{\$cra} as its return address will also function correctly,
+as if it were an ordinary function call and return.)
+
+Given the overloading of the single \insnriscvref{CJALR} instruction,
+with register selector operands selecting between multiple semantics,
+compilers \emph{must} be careful to use matching entry and exit \insnriscvref{CJALR}s.
+For example, entering a function with a \asm{\$cra} link register,
+transfering the contents of \asm{\$cra} to another register,
+and then ``tail calling'' through that latter register will not work on CHERIoT,
+even though analogous code would have worked on base RISC-V.
+
 \subsection{Capability bounds}
 \label{sec:bounds}
 

src/cheri_insts.sail

@@ -116,8 +116,16 @@ function clause execute(CJAL(imm, cd)) = {
     let (success, linkCap) = setCapAddr(PCC, nextPC); /* Note that nextPC accounts for compressed instructions */
     assert(success, "Link cap should always be representable.");
     assert(not (isCapSealed(linkCap)), "Link cap should always be unsealed");
-    let sentry_type = if mstatus.MIE() == 0b1 then otype_sentry_bie else otype_sentry_bid;
-    C(cd) = sealCap(linkCap, to_bits(cap_otype_width, sentry_type));
+
+    if cd == ra then {
+      /* When writing to ra, generate a sealed return capability. */
+      let sentry_type = if mstatus.MIE() == 0b1 then otype_sentry_bie else otype_sentry_bid;
+      C(cd) = sealCap(linkCap, to_bits(cap_otype_width, sentry_type));
+    } else {
+      /* Generate an unsealed return capability. */
+      C(cd) = linkCap;
+    };
+
     nextPC = newPC;
     RETIRE_SUCCESS
   }
@@ -176,8 +184,22 @@ function clause execute(CJALR(imm, cs1, cd)) = {
     let (success, linkCap) = setCapAddr(PCC, nextPC); /* Note that nextPC accounts for compressed instructions */
     assert(success, "Link cap should always be representable.");
     assert(not (isCapSealed(linkCap)), "Link cap should always be unsealed");
-    let sentry_type = if mstatus.MIE() == 0b1 then otype_sentry_bie else otype_sentry_bid;
-    C(cd) = sealCap(linkCap, to_bits(cap_otype_width, sentry_type));
+
+    if cd == ra then {
+      /*
+       * When writing to ra, generate a sealed return capability.  We can get
+       * here with cs1 unsealed or any forward sentry type.
+       */
+      let sentry_type = if mstatus.MIE() == 0b1 then otype_sentry_bie else otype_sentry_bid;
+      C(cd) = sealCap(linkCap, to_bits(cap_otype_width, sentry_type));
+    } else {
+      /*
+       * Generate an unsealed return capability.  From the conditions above, it
+       * must be the case that cs1 is unsealed or a forward inheriting sentry.
+       */
+      C(cd) = linkCap;
+    };
+
     nextPC = newPC;
     nextPCC = unsealCap(cs1_val);
     if unsigned(cs1_val.otype) == otype_sentry_id | unsigned(cs1_val.otype) == otype_sentry_bid then