From 82438a81b9f3a108ae619c459dc3bdcfd95463bb Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Mon, 5 Feb 2024 08:13:24 +0000 Subject: [PATCH] Addressed Konrad's feedback --- app-experimental.tex | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/app-experimental.tex b/app-experimental.tex index 71aea24a..0d1cfe0a 100644 --- a/app-experimental.tex +++ b/app-experimental.tex @@ -1329,7 +1329,10 @@ \subsection{Points-to-PCC} % <<< \subsubsection{Definition of linked pair of instructions} -In this extension, we propose to split the \insnnoref{CISentryJ }(CHERI indirect sealed entry jump) instruction into two sub instructions: \insnnoref{CLIL} (CHERI load isentry linked) and \insnnoref{CJAURL} (CHERI jump and unseal into register linked). +In this extension, we propose to split the functionality needed for a jump to a ``points to PCC'' isentry into two sub instructions: \insnnoref{CLIL} (CHERI load isentry linked) and \insnnoref{CJAURL} (CHERI jump and unseal into register linked). +A different approach would be to manage the entire functionality in one instructions, which could be called \insnnoref{CIPTCCJ} (CHERI Isentry Points to PCC Jump). +However, one big instruction would be against the RISC approach and we currently do not see a feasible path to implementation and less sophisticated microarchitectures. +Therefore, we decided to define a pair of linked instructions. In the following paragraphs, we will explain what these instructions do and how they enforce the security model we are designing. The \insnnoref{CLIL} instruction loads a capability through an isentry capability and seals it. @@ -1338,7 +1341,7 @@ \subsubsection{Definition of linked pair of instructions} The two instructions are linked and all security properties are held as explained in the following paragraphs. If attackers executed only the \insnnoref{CLIL} instruction, this will leave them with a sealed code capability. -This code capability cannot be used in regular jumps because it is seald with the \cotype{} $2^{64} - 5$. +This code capability cannot be used in regular jumps because it is sealed with the \cotype{} $2^{64} - 5$. The only way it can be used for a jump is in a subsequent \insnnoref{CJAURL} instruction. An attacker can only jump to a code capability with the isentry it came from. @@ -1353,7 +1356,7 @@ \subsubsection{Definition of linked pair of instructions} Loading the code capability does not break CHERI confidentiality. Isentries are not designed for secrecy about where a compartment wants to jump, but to implement jumping to a sealed pair of capabilities. -Similar methods, e.g., cinvoke gives out sealed code and data capabilities, which are then invoked as a pair. +Similar methods, e.g., \insnref{CInvoke} gives out sealed code and data capabilities, which are then invoked as a pair. The code capability itself is not secret. It is important to note that in the current state of this proposal the linked pair of a \insnnoref{CLIL} and \insnnoref{CJAURL} instruction does not give any guarantees about memory consistency. @@ -1469,7 +1472,7 @@ \subsection{Points to Pair} % <<< any validation on their contents. We allocate the following \cotype{} $2^{64} - 6$ from the reserved otype space for ``points to pair'' isentries. -%Furthermore, we allocate the \cotype{} $2^{64} - 7$ for capabilities that have been loaded through ``points to pair'' linked isentry loads. +Furthermore, we allocate the \cotype{} $2^{64} - 7$ for capabilities that have been loaded through ``points to pair'' linked isentry loads. As described in the previous section about ``points to PCC'' isentries, an instruction facilitating all operations is complex and imposes the need for @@ -1541,16 +1544,6 @@ \subsubsection{Security model} \subsection{Encoding of isentry instructions} -We specified multiple instructions in this Chapter. -Some of them exhibit similar functionality. -Therefore, we propose to encode the following instructions in the same encoding space and use ``mode'' bits to distinguish between the respective behaviour. - -\begin{itemize} - \item \insnref{CSealEntry}, \insnnoref{CISealPCC}, and \insnnoref{CISealPair} - \item \insnnoref{CLIL}, \insnnoref{CLILC}, and \insnnoref{CLILD} - \item \insnnoref{CJAURL} and \insnnoref{CJAURLP} -\end{itemize} - We propose the following encodings as laid out below: %TODO: incorporate into the framework of this repo @@ -1683,6 +1676,20 @@ \subsubsection*{Format} \end{bytefield}% \end{center} +\subsubsection{Different encoding possibilities} + +We specified multiple instructions in this Chapter. +Some of them exhibit similar functionality. +Therefore, we envision to encode the following instructions in the same encoding space and use ``mode'' bits to distinguish between the respective behaviour. + +\begin{itemize} + \item \insnref{CSealEntry}, \insnnoref{CISealPCC}, and \insnnoref{CISealPair} + \item \insnnoref{CLIL}, \insnnoref{CLILC}, and \insnnoref{CLILD} + \item \insnnoref{CJAURL} and \insnnoref{CJAURLP} +\end{itemize} + +However, we have not yet laid out the encoding of these instructions. + % >>> % >>> \section{Anti-tamper Seals}