\begin{latexonly}
\svnInfo $Id$  
\end{latexonly}

Our experience in building the Overshadow system for enhancing
assurance of applications built on commodity operating systems has
suggested two key lessons. First, systems looking to enhance OS assurance
typically focus on core isolation mechanisms such as memory and CPU
protection, but this is not sufficient to build a secure system. We
observe that additional attention must be paid to how applications are
affected by malicious OS behavior. To talk about ``trusted'' and
``untrusted'' parts of the OS interface without looking more deeply
into what can and cannot be safely relied upon from the OS, is to
casually dismiss a non-trivial problem.

Next, to address this problem, we observe that it is often easier to
verify correct behavior than to implement that behavior. Many OS
components can be refactored into an untrusted part that manages the
system resource in question and a smaller trusted part that verifies
the safety properties. In our experience, the trusted part can be
made considerably smaller than the untrusted part: our implementation
of Overshadow required under 20,000 lines of code to provide
protection for application memory, files, and control flow, in
contrast to the millions of lines of code that make up a typical
OS~\cite{chen08:_overs}.  We propose extensions to Overshadow that
allow it to tolerate more complex malicious behavior from the OS,
based on this principle of verifying system call results. Similar
techniques can be used in other systems that rely on untrusted OS or
application components.


%how a system can be meaningfully refactored to minimize TCB given that an isolation mechanism is present.  Any discussion of
%isolation which excludes these more holostic concerns is incomplete.
%application on, if a compromise in any of the components e.g.~ file
%system, drivers, virtual memory system allows any application to be
%compromised then at best your microkernel is only providing fault
%isolation, and for all practical purposes you have the same
%assurance as a monolithic kernel. 


%While a naive breakdown of an OS kernel by functional part will not
%neccessarily yeild better assurance, a cruicial observation is that
%often verifying the correct function of an OS component can be made
%considerably simpler than implementing that function or in other
%words, its is often easier to secure a resource than manager it.
%Storage provide the easiest example, with file systems and volume
%management code easily reaching into the hundreds of thousands of
%lines of code. While simply providing an encryption and metadata
%protection layer that secures this can be done with far less
%complexity~\cite{chen08:_overs, weinhold08:_vpfs}. Of course, this
%observation applies beyond just this example, to a wide range
%of encryption technologies.

%


%%% Local Variables: 
%%% mode: latex
%%% TeX-command-default: "Make"
%%% TeX-PDF-mode: t
%%% TeX-master: "paper"
%%% End: