\section{Related Work}
\label{section:related}

\Arch\ draws on past work in a variety of areas, including symbolic
execution, static and dynamic analysis, test frameworks, and formal
specification.

\paragraph{DDT and \see.}
The DDT and \see\ systems have been used for finding bugs in binary
drivers~\cite{ckc11, ckc12, kcc10}.  \Arch\ is built upon \see\ but
significantly extends its capabilities in three ways by leveraging 
driver source code. First and most important, \Arch\ automatically
detects the driver/kernel interface and generates code to interpose
checkers at that interface.  In contrast, \see\ requires programmers
to identify the interface manually and write plugins that execute {\em
  outside the kernel}, where kernel symbols are not available, though
\see\ and \Arch\ both support re-using existing testing tools. Second,
\Arch\ automatically detects and annotates loops, which in \see\ must
be identified manually and specified as virtual addresses. As a
result, the effort to test a driver is much reduced compared to
\see. Third, checkers in \Arch\ are implemented as standard C code
executing in the kernel, making them easy to write, and are only
necessary for kernel functions of interest. When the kernel interface
changes, only the checkers affected by interface changes must be
modified. In contrast, checkers in \see\ are written as plugins
outside the kernel, and the consistency model plugins must be updated
for all changed functions in the driver interface, not just those
relevant to checks.

\paragraph{Symbolic testing.}
There are numerous prior approaches to symbolic execution~\cite{bel75,
  cde08, chipounov2009selective, gks05, kcc10, sma05,
  Song:2008:BNA:1496255.1496257, xmsn05, zamfir10}. However, most
apply to standalone programs with limited environmental
interaction. Drivers, in contrast, execute as a library and make
frequent calls into the kernel.  BitBlaze supports environment
interaction but not I/O or
drivers~\cite{Pasareanu:2008:CUS:1390630.1390635}.

To limit symbolic execution to a manageable amount of state, previous
work limited the set of symbolically executed paths by applying
smarter search heuristics and/or by limiting program
inputs~\cite{cgp08, glm08, kcc10, la03, ms07,yst06}, which is similar to
\Arch's path pruning and prioritization.

Other systems combine static analysis with symbolic
execution~\cite{cfb06, cbz11, ecch00, pyr11}.  \Arch\ uses
static analysis to insert checkers and to dynamically guide the path
selection policy from code features such as loops and return
values. In contrast, these systems use the output of static analysis
directly within the symbolic execution engine to select paths.
Execution Synthesis~\cite{zamfir10} combines symbolic execution with
static analysis, but is designed to reproduce existing bug reports
with stack traces, and is thus complementary to \Arch.

\paragraph{Static analysis tools.}
Static analysis tools can find specific kinds of bugs common to large
classes of drivers, such as misuses of the
driver/kernel~\cite{bbc+06,Ball:2011:DSM:1965724.1965743,br02,microsoft10,padioleau:coccinelle:eurosys:2008}
or driver/device interface~\cite{krs09} and ignored error
codes~\cite{graal08, susskraut:error-handling:edcc:2006}.  Static
bug-finding tools are often faster and more scalable than symbolic
execution~\cite{Bessey:2010:FBL:1646353.1646374}.

We see three key advantages of testing drivers with symbolic
execution. First, symbolic execution is better able to find bugs that
arise from multiple invocations of the driver, such as when state is
corrupted during one call and accessed during another. It also
has a low false-positive rate because it makes few
approximations. Second, symbolic execution has full access to driver
and kernel state, which facilitates checking driver behavior. Furthermore,
checkers that verify behavior can be written as ordinary C, which
simplifies their development, and can track arbitrary runtime state
such as pointers and driver data. Symbolic execution also supports the
full functionality of C including pointer arithmetic, aliasing, inline
assembly code, and casts. In contrast, most static analysis tools
operate on a restricted subset of the language. Thus, symbolic
execution often leads to fewer false positives.  Finally, static tools
require a model of kernel behavior, which in Linux changes
regularly~\cite{stableapinonsense}.  In contrast, \Arch\ executes
checkers written in C and has no need for an operating system model,
since it executes kernel code symbolically.  Instead, \Arch\ relies
only on models for each I/O bus, which are much simpler and shorter to
write.

\paragraph{Test frameworks.}
Test frameworks such as the Linux Test Project (LTP)~\cite{ltp10} and
Microsoft's Driver Verifier (DV)~\cite{windows-device-testing,
  microsoft05b} can invoke drivers and verify their behavior, but
require the device be present.  In addition, LTP tests at the
system-call level and thus cannot verify properties of individual
driver entry points. \Arch\ can use these frameworks, either as
checkers, in the case of DV, or as a test program, in the case of LTP.

\paragraph{Formal specifications for drivers.}
Formal specifications express a device's or a driver's operational
requirements.  Once specified, other parts of the system can verify
that a driver operates
correctly~\cite{Barnett:2011:SVS:1953122.1953145,
  ryzhyk:formalize-dd:plos:2007, williams:nexus-drivers:osdi:2008}.
However, specifications must be created for each driver or
device. Amani et al. argue that the existing driver architecture is
too complicated to be formally specified, and propose a new
architecture to simplify
verification~\cite{amani:static-driver:apsys:2011}. Many of the
challenges to static verification also complicate symbolic testing,
and hence their architecture would address many of the issues solved
by \Arch.
