\section{Motivation}

The goal of our work is to improve driver quality through thorough
testing and validation.  To be successful, \Arch\ must demonstrate (i)
usefulness, (ii) simplicity, and (iii) efficiency.  First, \Arch\ must
be able to find bugs that are hard to find using other mechanisms,
such as normal testing or static analysis tools.  Second, \Arch\ must
require low developer effort to test a new driver and therefore support
many device classes, buses, and operating systems.  Finally, \Arch\
must be fast enough to apply to every patch.

% From Matt:  commented this out because of comment from reviewer 4G.
% We don't make the deep/broad distinction later on like we used to,
% so it may make sense just to cut it.

%We have two use cases for \Arch: {\em deeper} testing of drivers, by
%providing high coverage of individual patches, and {\em broader}
%testing of drivers by allowing more people to test drivers and find
%bugs.

\subsection{Symbolic Execution}

\Arch\ uses symbolic execution to execute device-driver code without
the device being present.  Symbolic execution allows a program's input
to be replaced with a {\em symbolic value}, which represents all
possible values the data may have. A {\em symbolic-execution engine}
runs the code and tracks which values are symbolic and which have {\em
  concrete} (\ie, fully defined) values, such as initialized
variables. When the program compares a symbolic value, the engine
forks execution into multiple {\em paths}, one for each outcome of the
comparison. It then executes each path with the symbolic value
constrained by the chosen outcome of the comparison. For example, the
predicate $x > 5$ forks execution by copying the running program. In
one copy, the code executes the path where $x \le 5$ and the other
executes the path where $x > 5$.  Subsequent comparisons can further
constrain a value.  In places where specific values are needed, such
as printing a value, the engine can concretize data by producing a
single value that satisfies all constraints over the data.

Symbolic execution detects bugs either through illegal operations,
such as dereferencing a null pointer, or through explicit assertions
over behavior, and can show the state of the executing path at the
failure site.

\paragraph{Symbolic execution with \see.}
\Arch\ is built on a modified version of the \see\ symbolic execution
framework.  \see\ executes a complete virtual machine as the program
under test. Thus, symbolic data can be used anywhere in the operating
system, including drivers and applications.  \see\ is a virtual
machine monitor (VMM) that tracks the use of symbolic data within an
executing virtual machine.  The VMM tracks each executing path within
the VM, and schedules CPU time between paths. Each path is treated
like a thread, and the scheduler selects which path to execute
and when to switch execution to a different path.

\see\ supports {\em plug-ins}, are modules loaded into the VMM that
can be invoked to record information or to modify execution. \Arch\
uses plugins to implement symbolic hardware, path scheduling, and
code-coverage monitoring.

\subsection{Why Symbolic Execution?}

Symbolic execution is often used to achieve high coverage of code by
testing on all possible inputs. For device drivers, symbolic execution
provides an additional benefit: executing without the device. Unlike
most code, driver code can not be loaded and executed without its
device present. Furthermore, it is difficult to force the device to
generate specific inputs, which makes it difficult to thoroughly test
error handling.

Symbolic execution eliminates the hardware requirement, because it can
use symbolic data for all device input. An alternate approach is to
code a software model of the
device~\cite{nelson:driver-model:plumbers:2011}, which allows more
accurate testing but greatly increases the effort required.  In
contrast, symbolic execution uses the driver itself as a model of
device behavior: any device behavior used by the driver will be
exposed as symbolic data.

Symbolic execution may provide inputs that correctly functioning
devices may not. However, because hardware can provide unexpected or
faulty driver input~\cite{krs09}, this unconstrained
device behavior is reasonable: drivers should not crash simply
because the device provided an errant value.

In comparison to static analysis tools, symbolic execution provides
several benefits. First, it uses existing kernel code as a model of
kernel behavior rather than requiring a programmer-written
model. Second, because driver and kernel code actually execute, it can
reuse kernel debugging facilities, such as deadlock detection, and
existing test suites. Thus, many bugs can be found without any
explicit description of correct driver behavior. Third, symbolic
execution can invoke a sequence of driver entry points, which allows
it to find bugs that span invocations, such as resource leaks. In
contrast, most static analysis tools concentrate on bugs occurring
within a single entry point.


\subsection{Why not Symbolic Execution?}

While symbolic execution has previously been applied to drivers with
DDT and \see, there remain open problems that preclude its widespread
use:

\paragraph{Efficiency.}  The engine creates a new path for every
comparison, and branchy code may create hundreds or thousands of
paths, called {\em path explosion}. This explosion can be reduced by
distinguishing and prioritizing paths that complete
successfully.  This approach enables executing deeper into the driver: if driver
initialization fails, the operating system could not otherwise invoke
most driver entry points. \see\ and DDT require complex, manually
written annotations to provide this information. These annotations
depend on kernel function names and behavioral details, which are
difficult for programmers to provide.  For example, the annotations
often examine kernel function parameters, and modify the memory of the
current path on the basis of the parameters.  The path-scheduling
strategies in DDT and \see\ favor exploring new code, but may not
execute far enough down a path to test all functionality.
%
\paragraph{Simplicity.} Existing symbolic testing tools require
extensive developer effort to test a single class of drivers, plus
additional effort to test each individual driver. For example,
supporting Windows NDIS drivers in \see\ requires over 1,000 lines of
code specific to this driver class.  For example, the \see\ wrapper
for the \codesm{NdisReadConfiguration} Windows function consists of
code to (a) read all of the call's parameters, which is not trivial
because the code is running outside the kernel, (b) fork additional
paths for different possible symbolic return codes, (c) bypass the
call to the function along these additional paths, and (d) register a
separate wrapper function, of comparable complexity, to execute when
this call returns.  Since developers need to implement similarly
complex code for many other functions in the driver/kernel interface,
testing many drivers becomes impractical in these systems. Thus, these
tools have only been applied to a few driver classes and drivers.
Expanding testing to many more drivers requires new techniques to
automate the testing effort.

%
%
\paragraph{Specification.} Finally, symbolic  execution by itself does
not provide  any specification of correct behavior:  a ``hello world''
driver does nothing wrong, nor  does it do anything right, such as
registering a device  with the kernel.  In existing  tools, tests must be
coded like  debugger extensions, with  calls to read and  write remote
addresses,  rather than as  normal test  code. Allowing  developers to
write   tests   in   the   familiar  kernel   environment   simplifies
the specification of correct behavior.


Thus, our work focuses on improving the state of the art to greatly
simplify the use of symbolic execution for testing, and to broaden its
applicability to almost any driver in any class on any bus.

% Very similar text appears at the start of the next section (design)
%
%\Arch\
%provides solutions to all three open problems through its combined use
%of static analysis and code generation, symbolic hardware, and the
%\tf.
