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

The protection architectures in the previous section guarantee that
applications that do not interact explicitly with the OS
execute correctly, because the integrity of code and data is
protected, and control flow proceeds as normal. Assuming the basic
protection architecture is sound, no loss of integrity or data leakage
is possible, although availability is not guaranteed
because the OS could simply stop scheduling the application.

% To start, it becomes impossible to guarantee application
% availability, since the OS could simply refuse to schedule the
% application. But even an availability problem could develop into a
% safety problem: if an application consists of multiple processes,
% stopping one could cause another to behave incorrectly.

However, any non-trivial program makes system calls, and this presents
an opportunity for a malicious OS to influence the program's data and
control flow by manipulating system call results. To take a simple
example, if a multithreaded program relies on the OS to implement a
mutual-exclusion lock, the OS could grant the lock to two threads at
once. Since the OS also handles scheduling, this has the
potential to create a race condition even in correctly written code,
with arbitrarily bad consequences.

Characterizing the security properties that are possible when the
operating system is malicious is challenging.  Ultimately, we would
like to provide a high-level guarantee like ``sensitive data is never
exposed to unauthorized parties.''  However, we would like to operate
with unmodified applications, treating them as black boxes, and
therefore cannot make such statements about application
semantics. Indeed, a buggy application might expose its own sensitive
data (\emph{e.g.\ }via a buffer overflow), even if the OS behaves
correctly. Thus, our problem must be one of \emph{ensuring that
  applications continue to run normally} (or fail-stop) even if the OS
behaves maliciously, rather than one of protecting application data.

\subsection{Approaches to Ensuring Security}
\label{sec:security:system-call}

For programs to run normally, we must guarantee that the action
performed and value returned by each system call conforms to the
application's model of how system calls behave. Ideally, this model
would be the same as the standard OS contract for system calls
(\emph{e.g.\ }the POSIX specification). However, modeling all
behaviors of every system call would be tantamount to reimplementing
nearly the entire OS.  Moreover, there may be behavior that
technically complies with the specification, but still violates
application assumptions.

Instead, we propose to develop a new specification consisting only of
\emph{safety properties}, \emph{i.e.}~a model of normal OS semantics
that pertains only to security, not to availability. By weakening the
specification to only provide safety properties, it becomes easier to
hold the OS to its contract. For example, with the mutex system call
described above, we might guarantee only that if a lock is granted, it
is held by no other thread, saying nothing about availability or
fairness. Providing weaker semantics does mean that it is impossible
to guarantee correctness of arbitrary unmodified applications, but we
anticipate that the additional requirements will not pose a large
burden for developers, and correspond in many cases to good programming
practice on a correctly-functioning OS.

There are three fundamental methods for ensuring that system calls are
executed correctly:

\begin{itemize}
\item We can \textbf{disallow} use of the system call in
  security-critical code, permitting applications to use it ``only at
  their own risk.'' Clearly, this is to be avoided from a
  compatibility perspective. However, certain system calls are so
  intimately related to the OS implementation that their correctness
  cannot be guaranteed --- for example, those related to kernel
  modules or scheduling policies.
\item We can \textbf{emulate} the system call in trusted code. This
  option should also be used sparingly, since reimplementing
  system calls adds to the size of the TCB. Nevertheless, it may be
  the best option for simpler system calls, such as those
  related to time.
\item We can \textbf{verify} the results of the system call after the
  OS has executed it. This is our preferred approach, since verifying
  a system call's safety properties can often be substantially simpler
  than emulating it. This is the approach that Overshadow and XOM
  already use for protecting memory: they delegate memory management
  to the OS, but verify hashes at access time to ensure that the
  correct data is in the correct memory location.
\end{itemize}

Returning to the mutex system call example, we can verify that
only one thread holds the lock at once using a flag stored in a
protected shared memory region to indicate whether the lock is
held. Each thread updates the flag as it acquires or releases
the lock, and verifies that the flag is not already set when it
acquires the lock. This is a simple procedure that ensures the key
safety property of locking while still delegating the rest of the
implementation details (waking up the right process when the lock is
available, ensuring fairness, etc.) to the OS.

We propose to implement emulation and verification using Overshadow's
existing system call interposition mechanism, which redirects control to
the shim, a trusted component, whenever an application makes a system
call. However, these techniques can be used independently of
Overshadow, by using a different interposition technique, or by modifying
the application.

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