rearranged table

archdoc/chap-cheri-riscv.tex

@@ -474,16 +474,16 @@ \subsection{Sealed capabilities}
 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 \insnriscvref{CJALR}, i.e. only the following combinations are allowed in \insnriscvref{CJALR}:
 
 \begin{center}
-\begin{tabular}{|c|c|c|c|}
-\hline
-\asm{cs1} & \asm{cd} & Used for & Valid \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 & \asm{\$cra} & Function call & Unsealed or forward sentries $(0, 1, 2, 3)$\\
-any & $\ne$ \asm{\$cnull} & Function call & Unsealed or interrupt inheriting forward sentry $(0, 1)$\\
-\hline
-\end{tabular}
+ \begin{tabular}{|c|c|c|c|}
+ \hline
+ \asm{cs1} & \asm{cd} & Used for & Valid \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 & $\ne$ \asm{\$cnull} & Function call & Unsealed or interrupt inheriting forward sentry $(0, 1)$\\
+ any & \asm{\$cra} & Function call & Unsealed or forward sentries $(0, 1, 2, 3)$\\
+ \hline
+ \end{tabular}
 \end{center}
 
 \subsection{Capability bounds}

src/cheri_insts.sail

@@ -138,8 +138,8 @@ union clause ast = CJALR : (bits(12), regidx, regidx)
  * - None of the following combinations hold:
  * 1. *cd* = *cnull*, *cs1* = *cra* and *cs1* is a backwards sentry (Function return aka *cret* is only permitted to backwards sentry)
  * 2. *cd* = *cnull*, *cs1* $ne$ *cra* and *cs1* is unsealed or a forwards interrupt inheriting sentry (Tail calls are only permitted to unsealed caps or interrupt handling sentry using a target register different from *cra*, with the return register *cra* set by a different instruction)
- * 3. *cd* = *cra* and *cs1* is unsealed or a forwards sentry (Function calls are only permitted to unsealed caps or forwards sentry, with link register *cra*)
- * 4. *cd* $\ne$ *cnull* and *cs1* is unsealed or a forwards interrupt inheriting sentry (Less restricted function calls to interrupt inheriting sentries)
+ * 3. *cd* $\ne$ *cnull* and *cs1* is unsealed or a forwards interrupt inheriting sentry (Less restricted function calls to interrupt inheriting sentries)
+ * 4. *cd* = *cra* and *cs1* is unsealed or a forwards sentry (Function calls are only permitted to unsealed caps or forwards sentry, with link register *cra*)
  * - *cs1*.**perms** does not grant **Permit_Execute**.
  * - *cs1*.**address** $+$ *imm* is unaligned, ignoring bit 0.
  *
@@ -162,8 +162,8 @@ function clause execute(CJALR(imm, cs1, cd)) = {
  } else if (isCapSealed(cs1_val) & imm != zeros()) |
  not ((cd == zreg & cs1 == ra & isCapBackwardSentry(cs1_val)) |
  (cd == zreg & cs1 != ra & (not(isCapSealed(cs1_val)) | isCapForwardInheritSentry(cs1_val))) |
- (cd == ra & (not(isCapSealed(cs1_val)) | isCapForwardSentry(cs1_val))) |
- (cd != zreg & (not(isCapSealed(cs1_val)) | isCapForwardInheritSentry(cs1_val)))) then {
+ (cd != zreg & (not(isCapSealed(cs1_val)) | isCapForwardInheritSentry(cs1_val))) |
+ (cd == ra & (not(isCapSealed(cs1_val)) | isCapForwardSentry(cs1_val)))) then {
  handle_cheri_reg_exception(CapEx_SealViolation, cs1);
  RETIRE_FAIL
  } else if not (cs1_val.permit_execute) then {