\HeadingLevelC{Protection Against Direct Attacks}
\label{sec:direct_attack_protection}

The correctness proof for Sanctum's DRAM isolation can be divided into two
sub-proofs that cover the hardware and software sides of the system. First,
we need to prove that the page walker modifications described in
\S~\ref{sec:pmh_walker_input} and \S~\ref{sec:pmh_walker} behave according to
their descriptions. Thanks to the small sizes of the circuits involved, this
sub-proof can be accomplished by simulating the circuits for all logically
distinct input cases. Second, we must prove that the security monitor
configures Sanctum's extended page walker registers in a way that prevents
direct attacks on enclaves. This part of the proof is significantly more
complex, but it follows the same outline as the proof for SGX's memory access
protection presented in~\S~\ref{sec:sgx_access_correctness}.
%cite{costan2016sgxexplained}.

The proof revolves around a main invariant stating that all TLB entries in
every core are consistent with the programming model described in
\S~\ref{sec:programming_model}. The invariant breaks down into three cases that
match~\S~\ref{sec:sgx_access_correctness}, after substituting DRAM regions for pages.

These three cases are outlined below.

\begin{enumerate}
\item At all times when a core is not executing enclave code, its TLB may only
  contain physical addresses in DRAM regions allocated to the OS.
\item At all times when a core is executing an enclave's code, the TLB entries
  for virtual addresses outside the current enclave's EVRANGE must contain
  physical addresses belonging to DRAM regions allocated to the OS.
\item At all times when an core is executing an enclave's code, the TLB entries
  for virtual addresses inside the current enclave's EVRANGE must match the
  virtual memory layout specified by the enclave's page tables.
\end{enumerate}
