From 46925930477ad3a19e4985db4a4eca8c450ed95b Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 25 Jul 2024 09:07:07 -0400 Subject: [PATCH 1/3] Belatedly fix StoreCapImmediate docs We no longer throw exceptions for !SL authorities storing !G capabilities, just clear the tag. --- src/cheri_insts.sail | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 9be6527..d582e79 100644 --- a/src/cheri_insts.sail +++ b/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 *cs2*.**perms** does not + * grant **Global**. + * * ## 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**. */ From ad96f35e729c7527a4f7e7e3aa2228bd0dbe0dfc Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 25 Jul 2024 08:08:18 -0400 Subject: [PATCH 2/3] 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 https://github.com/microsoft/cheriot-sail/pull/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 https://github.com/microsoft/cheriot-sail/issues/63 ("Have CJALR create !G sentries?"). Co-authored-by: Robert Norton --- archdoc/chap-changes.tex | 6 ++++-- archdoc/chap-cheri-riscv.tex | 5 ++++- src/cheri_insts.sail | 7 +++++-- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/archdoc/chap-changes.tex b/archdoc/chap-changes.tex index bd6e49c..fa0d36b 100644 --- a/archdoc/chap-changes.tex +++ b/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 recieve 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} diff --git a/archdoc/chap-cheri-riscv.tex b/archdoc/chap-cheri-riscv.tex index 4446e30..efc4cd5 100644 --- a/archdoc/chap-cheri-riscv.tex +++ b/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}. @@ -486,6 +486,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} diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index d582e79..bce6198 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -862,7 +862,7 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12)) * * The stored capability will have its tag forcibly cleared if *cs1*.**perms** * does not grant **Permit_Store_Local_Capability** and *cs2*.**perms** does not - * grant **Global**. + * grant **Global** or *cs2* is a backwards sentry. * * ## Exceptions * @@ -905,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, From a5ff784492150bcf137fb9b83961b0a3a7d592c5 Mon Sep 17 00:00:00 2001 From: Nathaniel Filardo <105816689+nwf-msr@users.noreply.github.com> Date: Mon, 29 Jul 2024 13:50:40 -0400 Subject: [PATCH 3/3] Review feedback Co-authored-by: Robert Norton <1412774+rmn30@users.noreply.github.com> --- src/cheri_insts.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index bce6198..f346d8e 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -861,7 +861,7 @@ 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 *cs2*.**perms** does not + * does not grant **Permit_Store_Local_Capability** and either *cs2*.**perms** does not * grant **Global** or *cs2* is a backwards sentry. * * ## Exceptions