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, we observe that it is often easier to verify correct behavior
than to implement that behavior, \emph{i.e.}~OS components can often
be refactored into a small trusted part that verifies the safety
properties and a larger untrusted part that manages the system
resource in question. 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, and argue that the
principles involved are relevant to other systems. 


%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.

%