\svnInfo $Id$

The protection architectures in the previous section guarantee that
applications that do not have explicit interactions 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.

We note that characterizing the security properties that can be
provided 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 run correctly}, rather than one of protecting
application data.


\paragraph{Approaches to ensuring security.}
\label{sec:security:system-call}

To ensure that programs that make system calls execute correctly, we
must guarantee that the action performed and value returned by each
system call is correct, in that it conforms to the application's model
of how system calls behave. Ideally, we would like this model to be
the same as the standard OS contract for system calls (\emph{e.g.\
}the POSIX specification). However, fully achieving this goal is
unlikely to be possible without reimplementing nearly the entire OS in
the trusted components. Moreover, there may be behavior that 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. In many cases, this can 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}

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.

Returning to the example of the mutex system call, 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 will update the flag whenever it acquires or
releases the lock, and verifies that the flag is not already set when
it acquires the lock. This is a very simple procedure, but it
nevertheless 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.

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