Skip to content

Commit

Permalink
Addressed Konrad's feedback
Browse files Browse the repository at this point in the history
  • Loading branch information
francislaus committed Feb 5, 2024
1 parent 6e3fe86 commit 82438a8
Showing 1 changed file with 21 additions and 14 deletions.
35 changes: 21 additions & 14 deletions app-experimental.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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}
Expand Down

0 comments on commit 82438a8

Please sign in to comment.