\section{Design}
\label{section:implementation}

The \Arch\ architecture focuses on thorough testing of drivers to
ensure the code does not incorrectly use the kernel/driver interface,
crash, or hang. We target test situations where the driver code is
available, and use that code to simplify testing with a combination
of symbolic execution, static code analysis and transformation, and an
extensible \tf executing in the kernel.

The design of \Arch\ is shown in Figure \ref{fig:symdrive-arch}.  The OS
kernel and driver under test, as well as user-mode test programs,
execute in a virtual machine. The symbolic execution engine provides
symbolic devices for the driver. \Arch\ provides stubs that invoke
checkers on every call into or out of the driver. A \tf\ tracks
execution state and passes information to plugins running in the
engine to speed testing and improve test coverage.

During the development of \Arch, we considered a more limited design
in which symbolic execution was limited to driver code.  In this
model, exploring multiple paths through the kernel was not possible;
callbacks to the kernel instead required a model of kernel behavior to
allow them to execute on multiple branches. However, after
implementing a prototype of this design, we concluded that full-system
symbolic execution is preferable because it greatly reduces the effort
to test drivers by using real kernel code rather than a kernel model.

We implemented \Arch\ for Linux and FreeBSD, as these kernels provide
a large number of drivers to test.  Only the \tf\ code running in the
kernel is specialized to the OS.  We made small, conditionally
compiled changes to both kernels to print failures and stack traces to
the \see\ log and to register the module under test with \see.  The
breakdown of \Arch\ code is shown in Table~\ref{table:lines-of-code}.

\Arch\ consists of five components: (i) a modified version of the
\see\ symbolic-execution engine, which consists of a
\Arch-specific plugin plus changes to \see;
(ii) symbolic devices to provide
symbolic hardware input to the driver; (iii) a {\em \tf} executing
within the kernel that guides symbolic execution; (iv) the {\em \ds}
static-analysis and code transformation tool to analyze and
prepare drivers for testing; and (v) a set of OS-specific {\em
  checkers} that interpose on the driver/kernel interface for
verifying and validating driver behavior.

\begin{figure}
\begin{center}
\includegraphics[keepaspectratio=true,width=2.2in]{figures/SymArch.pdf}
\end{center}
\vspace{-0.3in}
\caption{\small \bf The \Arch\ architecture. A developer produces the
  transformed driver with \ds\ and can write checkers and test
  programs to verify correctness.}
\label{fig:symdrive-arch}
\vspace{-0.1in}
\end{figure}

\begin{table}
\small
\centering
\begin{tabular}{l|r}
{\bf Component} & {\bf LoC} \\
\hline
Changes to \see & 1,954 \\
\ds & 2,681 \\
\Tf & 3,002 \\
Checkers & 564 \\
Support Library & 1,579 \\
Linux kernel changes & 153 \\
FreeBSD kernel changes & 81 \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Implementation size of \Arch. }
\label{table:lines-of-code}
\vspace{-0.2in}
\end{table}

\input{sect/impl_vm}
\input{sect/impl_symbolic_devices}
\input{sect/impl_tf}
\input{sect/impl_symgen}

\subsection{Limitations}
\Arch\ is neither sound nor complete.  The false positives we have
experienced fall into two major categories.  First, symbolic execution
is slow, which may cause the kernel to print timing warnings and cause
driver timers to fire at the wrong time.  Second, our initial
checkers were imprecise and disallowed (bizarre) behavior the kernel
considers legal.  We have since fixed the checkers, and have not seen
them generate false positives.


Although we have observed no false negatives among the checkers we
wrote, \Arch\ cannot check for all kinds of bugs.  Of 11 common
security vulnerabilities~\cite{chen:linux-vuln:apsys:2011}, \Arch\
cannot detect integer overflows and data races between threads, though
support for overflow detection is possible in principle because the
underlying VMM interprets code rather than executing it directly.  In
addition, \Arch\ cannot achieve full path coverage for all drivers because
\Arch's aggressive path pruning may terminate paths that lead to bugs.
\Arch\ may also miss race conditions, such as those requiring the
interrupt handler to interleave with another thread in a specific way.
