\HeadingLevelC{Security Monitor Protection}
\label{sec:monitor_protection}

The security monitor is in Sanctum's TCB, so the system's security depends on
the monitor's ability to preserve its integrity and protect its secrets from
attackers. The monitor does not use address translation, so it is not exposed
to any attacks via page tables. The monitor also does not protect
itself from cache timing attacks, and instead avoids making any memory accesses
that would reveal sensitive information.

Proving that the monitor is protected from direct attacks from a malicious OS
or enclave can be accomplished in a few steps. First, we invoke the proof that
the circuits in \S~\ref{sec:pmh_walker_input} and \S~\ref{sec:pmh_walker},
are correct. Second, we must prove that the
security monitor configures Sanctum's extended page walker registers correctly.
Third, we must prove that the DRAM regions that contain monitor code or data
are always allocated to the OS.

The circuit correctness proof was outlined in
\S~\ref{sec:direct_attack_protection}, and effectively comes down to
reasoning through all possible input classes and simulating the circuit.

The register configuration correctness proof consists of analyzing Sanctum's
initialization code and ensuring that it sets up the \texttt{parbase} and
\texttt{parmask} registers to cover all of the monitor's code and data. These
registers will not change after the security monitor hands off control to the
OS in the boot sequence.

Last, proving that the DRAM regions that store the monitor always belong to
the OS requires analyzing the monitor's DRAM region management code. At boot
time, all DRAM regions must be allocated to the OS correctly. During
normal operation, the \textit{block DRAM region} API
call~(\S~\ref{sec:monitor}) must reject DRAM regions that contain
monitor code or data. At a higher level, the DRAM region management code must
implement the state machine shown in Figure~\ref{fig:dram_region_states}, and
the \texttt{drbmap} and \texttt{edrbmap} registers~(\S~\ref{sec:pmh_walker})
must be updated to correctly reflect DRAM region ownership.

Since the monitor is exposed to cache timing attacks from the OS,
Sanctum's security guarantees rely on proofs that the attacks would not yield
any information that the OS does not already have. Fortunately, most of the
security monitor implementation consists of acknowledging and verifying the OS'
resource allocation decisions. The main piece of private information held by
the security monitor is the attestation key. We can be assured that the monitor
does not leak this key, as long as we can prove that the monitor implementation
only accesses the key when it is provided to the signing
enclave~(\S~\ref{sec:sanctum_signing_enclave}), that the key is provided via a
data-independent memory copy operation, such as \texttt{memcpy}, and that the
attestation key is only disclosed to the signing enclave.

Superficially, proving the last claim described above comes down to ensuring
that the API providing the key compares the current enclave's measurement
with a hard-coded value representing the correct signing enclave, and errors
out in case of a mismatch. However, the current enclave's measurement is
produced by a sequence of calls to the monitor's enclave loading APIs, so a
complete proof also requires analyzing each loading API implementation and
proving that it modifies the enclave measurement as expected.

Sanctum's monitor requires a complex security argument when compared to SGX's
microcode, because the microcode is burned into a ROM that is not accessible
by software, and is connected to the execution core via a special path that
bypasses caches. We expect that the extra complexity in the security argument
is much smaller than the complexity associated with the microcode
programming.  Furthermore, SGX's architectural enclaves, such as its quoting
enclave, must operate under the same regime as Sanctum's monitor, as SGX does
not guarantee cache isolation to its enclaves.
