\HeadingLevelB{The Case for Hardware Isolation}

The best known practical method for securing a software system amounts to
modularizing the system's code in a way that minimizes code in
the modules responsible for the system's security. Formal verification techniques
are then applied to these modules, which make up the system's trusted
codebase (TCB). The method assumes that software modules are isolated, so
the TCB must also include the mechanism providing the isolation
guarantees.

Today's systems rely on an operating system kernel, or a hypervisor (such as
Linux or Xen, respectively) for software isolation. However \textbf{each} of
the last three years (2012-2014) witnessed over 100 new security
vulnerabilities in Linux \citep{cvedetails2014linux, chen2011linux}, and over 40
in Xen \citep{cvedetails2014xen}.

%\ExtendedVersionOnly{
One may hope that formal verification methods can produce a secure kernel or
hypervisor. Unfortunately, these codebases are far outside our verification
capabilities: Linux and Xen have over
\emph{17 million} \citep{anthony2014linuxsize} and 150,000 \citep{xen2015loc} lines
of code, respectively. In stark contrast, the seL4 formal verification effort
\citep{klein2009sel4} spent \emph{20 man-years} to cover 9,000 lines of code.
%}

Given Linux and Xen's history of vulnerabilities and uncertain prospects for
formal verification, a prudent system designer cannot include either in a TCB
(trusted computing base), and must look elsewhere for a software isolation
mechanism.

Fortunately, Intel's Software Guard Extensions (SGX)
\citep{mckeen2013sgx, anati2013sgx} has brought attention to the alternative of
providing software isolation primitives in the CPU's hardware. This avenue is
appealing because the CPU is an unavoidable TCB component, and processor
manufacturers have strong economic incentives to build correct hardware.
