%\subsection{Software Defect Mitigation}

%The seL4 \citep{klein2009sel4} formal verification effort shows that trusted system software with 9 kloc can be successfully verified. Sanctum's measurement root and security monitor are smaller ($<$ 5 kloc) providing reason for optimism.
