\HeadingLevelC{The Security of Software Attestation}
\label{sec:sanctum_software_attestation_correctness}

The security of Sanctum's software attestation scheme depends on the
correctness of the measurement root and the security monitor. \texttt{mroot}'s
sole purpose is to set up the attestation chain, so the attestation's security
requires the correctness of the entire \texttt{mroot} code. The monitor's
enclave measurement code also plays an essential role in the attestation
process, because it establishes the identity of the attested enclaves, and is
also used to distinguish between the signing enclave and other enclaves.
Sanctum's attestation also relies on mailboxes, which are used to securely
transmit attestation data from the attested enclave to the signing enclave.

At a high level, the measurement root's correctness proof is lengthy and
tedious, because setting up the attestation chain requires implementations for
cryptographic hashing, symmetric encryption, RSA key generation, and RSA
signing. Before the monitor measurement is performed, the processor must be
placed into a cache-as-RAM mode, and the monitor must be copied into the
processor's cache. Fortunately, the proof can be simplified by taking into
account that when \texttt{mroot} starts executing, the computer is in a
well-defined post-reset state, interrupt processing is disabled, and no other
software is being executed by the CPU. Furthermore, \texttt{mroot} runs in
machine mode on the RISC-V architecture, so the code uses physical addresses,
and does not have to deal with the complexities of address translation.

Measuring the security monitor requires initializing the flash memory that
stores it. Interestingly, the correctness of the initialization code is not
critical to Sanctum's security. If the flash memory is set up incorrectly, the
monitor software that is executed may not match the version stored on the flash
chip. However, this does not impact the software attestation's security, as
long as the measurement computed by \texttt{mroot} matches the monitor that is
executed. Storage initialization code is generally complex, so this argument
can be used to exclude a non-trivial piece of the measurement root's code from
correctness proofs.

The correctness proof for the monitor's measurement code consists of a
sub-proof for the cryptographic hash implementation, and sub-proofs for the
code that invokes the cryptographic hash module in each of the enclave loading
APIs~(\S~\ref{sec:monitor_enclave_lifecycle}), which are
\textit{create enclave}, \textit{load page}, \textit{load page table entry},
and \textit{load thread}. The cryptographic hash implementation can be shared
with the measurement root, so the correctness proof can be shared as well. The
hash implementation operates on public data, so it does not need to be
resistant to side-channel attacks. The correctness proofs for the enclave
loading API implementations are tedious but straightforward.

The security analysis of the monitor's mailbox API~(\S~\ref{sec:mailboxes})
implementation relies on proving the claims below. Each claim can be proved by
analyzing a specific part of the mailbox module's code. It is worth noting that
these claims only cover the subset of the mailbox implementation that the
signing enclave depends on.

\begin{enumerate}
\item An enclave's mailboxes are initialized to the empty state.
\item The \textit{accept message} API correctly sets the target mailbox into
  the empty state, and copies the expected sender enclave's measurement
  into the mailbox metadata.
\item The \textit{send message} API errors out without making any modifications
  if the sending enclave's measurement does not match the expected value in the
  mailbox's metadata.
\item The \textit{send message} API copies the sender's message into the
  correct field of the mailbox's metadata.
\item The \textit{receive message} API errors out if the mailbox is not in the
  full state.
\item The \textit{receive message} API correctly copies the message from the
  mailbox metadata to the calling enclave.
\end{enumerate}
