\section{Introduction}
\label{section:introduction}

%
% Comments from Julia
%

%\fixme{Julia: It seems like a major point of the paper is ``s2e is incredibly
%  hard to use, so we have done sonething to make it easier''. But
%  easier is not easy, and presumably the s2e paper did not go into
%  gory detail about how hard it is to use either. So it could be
%  useful to have a small user study, ie a student in your group who
%  has not worked on symdrive but who knows the kernel and perhaps even
%  knows the driver he wants to test should down load the tool and test
%  his code. You do have the case of yourselves not knowing the driver
%  under test, but I'm not sure that is the most realistic use case. I
%  would imagine that symdrive would be useful for a maintainer who
%  wants to check that each patch he accepts is OK. The people who
%  write the patches in the first place might not know the code well,
%  but they don't have the same burden of producing something that is
%  absolutely correct either.}

%\fixme{I took a look at the SymDrive paper. So far (up through page 6)
%  I think that the position of the paper could be more clear. Why not
%  do static analysis if you have the source code? Is the extension to
%  more types of buses a conceptual contribution over s2e or is it just
%  engineering? In the related work section, it is not clear what it is
%  that solves the problems with loops etc found in s2e.The solution is
%  probably that you have the source code and they do not, but that is
%  not mentioned at all.}

%\fixme{Overall, it would seems that the contribution of the paper is
%  some sort of sweet spot between static and dynamic analysis, but the
%  issues involved (ie why do other approaches not work well, not just
%  that they do not work well) and the benefits of the approach (ie why
%  does symdrive do better?)  could be more clear in the
%  introduction.}

% From Matt - Counted 29 patches with the phrase ``compile tested
% only'' I suspect the number is much higher but there's no way to
% know.  One developer I spoke to while submitting a patch
% specifically said he did not have the hardware to test the patch, so
% we just ``assumed'' the proposed change was reasonable.  The issue
% in that case related to whether reading some device register had a
% side effect -- it did not look like it would, but nobody seemed to
% know for sure.

Device drivers are critical to operating-system reliability, yet are
difficult to test and debug.  They run in kernel mode, which prohibits
the use of many runtime program-analysis tools available for user-mode
code, such as Valgrind~\cite{ns07}.  Their need for hardware can
prevent testing altogether: over two dozen driver Linux and FreeBSD
patches include the comment ``compile tested only,'' indicating that
the developer was unable or unwilling to run the driver. Even with
hardware, it is difficult to test error-handling code that runs in
response to a device error or malfunction. Thorough testing of
failure-handling code is time consuming and requires exhaustive
fault-injection tests with a range of faulty inputs.

%\fixme{Gilles: any numbers we can incorporate that demonstrate this
%is more common}  From Matt:  I can't think of any way to measure this
%quantitatively

Complicating matters, a single driver may support dozens of devices
with different code paths.  For example, one of the 18 supported
medium access controllers in the E1000 network driver requires an
additional EEPROM read operation while configuring flow-control and
link settings. Testing error handling in this driver requires the
specific device, and consideration of its specific failure modes. 

Static analysis tools such as Coverity~\cite{coverity04} and
Microsoft's Static Driver Verifier~\cite{microsoft10} can find many
bugs quickly.  However, these tools are tuned for fast, relatively
shallow analysis of large amounts of code and therefore only
approximate the behavior of some code features, such as
pointers. Furthermore, they have difficulty with bugs that span
multiple invocations of the driver. Hence, static analysis misses
large aspects of driver behavior.

%\fixme{Gilles: Focus on following paragraph.  This should be said before
%  introducing symdrive. If I understand correctly, you are making the
%  case that existing symbolic execution tools are promising, but they
%  are not yet usable by the ordinary driver developer. I think this
%  should come first before introducing symdrive. You must then point
%  out what are the (fundamental) limitations and then show how
%  symdrive solve them.}

We address these challenges using {\em symbolic execution} to test
device drivers.  This approach executes driver code on all possible
device inputs, allows driver code to execute without the device
present, and provides more thorough coverage of driver code,
including error handling code.  DDT~\cite{kcc10} and \see~\cite{ckc11,
  ckc12} previously applied symbolic execution to driver testing, but
these systems require substantial developer effort to test new classes
of drivers and, in many cases, even specific new drivers.

This paper presents {\em \Arch}, a system to test Linux and FreeBSD
drivers without devices. \Arch\ uses static
analysis to identify key features of the driver code, such as
entry-point functions and loops. With this analysis, \Arch\ produces
an instrumented driver with callouts to test code that allows many
drivers to be tested with no modifications. The remainder require a
few annotations to assist symbolic execution at locations that \Arch\
identifies.

We designed \Arch\ for three purposes. First, a driver developer can
use \Arch\ to test driver patches by thoroughly executing all branches
affected by the code changes. Second, a developer can use \Arch\ as a
debugging tool to compare the behavior of a functioning driver against
a non-functioning driver. Third, \Arch\ can serve as a general-purpose
bug-finding tool and perform broad testing of many drivers with little
developer input.

% Next paragraph:
%\fixme{Gilles: it looks like SymDrive is only a engineering
%  delta on S2E, and that all hard problems are solved by S2E.  The
%  rest of this paragraph contains the novelty, you should focus on
%  it. Why is it complex to develop a testing environment for drivers,
%  why this is not ``just an improved symbolic execution
%  environment''.}

\Arch\ is built with the \see\ system by Chipounov et al.~\cite{ckc11,
  ckc12} ,
which can make any data within a virtual machine symbolic and explore
its effect.  \Arch\ makes device inputs to the driver symbolic,
thereby eliminating the need for the device and allowing execution on
the complete range of device inputs.  In addition, \see\ enables
\Arch\ to further enhance code coverage by making other inputs to the
driver symbolic, such as data from the applications and the kernel.
When it detects a failure, either through an invalid operation or an
explicit check, \Arch\ reports the failure location and inputs that
trigger the failure.

%\fixme{Julia: Answer ``why?'' for various parts of the next two
%  paragraphs -- I think.  her comment was unclear}

% Next paragraph: \fixme{Gilles: Make sure the next paragraph does not
% make SymDrive look merely like a delta over existing tools,
% e.g. symbolic hardware.}

% Next paragraph: \fixme{Gilles: engineering limitation or novel?
% referring to I/O memory and DMA}

\Arch\ extends \see\ with three major components. First, \Arch\ uses
{\em \ds}, a static-analysis and code transformation tool, to analyze
and instrument driver code before testing. \ds\ automatically performs
nearly all the tasks previous systems left for developers, such as
identifying the driver/kernel interface, and also provides hints to
\see\ to speed testing. Consequently, little effort is needed to apply
\Arch\ to additional drivers, driver classes, or buses. As
evidence, we have applied \Arch\ to eleven classes of drivers on five buses
in two operating systems.

Second, \Arch\ provides a {\em \tf} that allows {\em checkers} that
validate driver behavior to be written as ordinary C code and execute
in the kernel.  These checkers have access to kernel state and the
parameters and results of calls between the driver and the kernel. A
checker can make pre- and post-condition assertions over driver
behavior, and raise an error if the driver misbehaves.  Using bugs and
kernel programming requirements culled from code, documentation, and
mailing lists, we wrote 49 checkers comprising 564 lines of code to
enforce rules that maintainers commonly check during code reviews, such as
matched allocation/free calls across entry points, no memory leaks,
and proper use of kernel APIs.

Finally, \Arch\ provides an {\em execution-tracing} mechanism for
logging the path of driver execution, including the instruction
pointer and stack trace of every I/O operation. These traces can be
used to compare execution across different driver revisions and
implementations.  For example, a developer can debug where a buggy
driver diverges in behavior from a previous working one. We have also
used this facility to compare driver implementations across operating systems.

We demonstrate \Arch's value by applying it to
\howmanydrivers\ drivers, and find \howmanybugs\ bugs, including two
security vulnerabilities.  We also find two driver/device interface
violations when comparing Linux and FreeBSD drivers.  To the best of
our knowledge, no symbolic execution tool has examined as many
drivers.  In addition, \Arch\ achieved over 80\% code coverage in most
drivers, and is largely limited by the ability of user-mode tests to
invoke driver entry points.  When we use \Arch\ to execute code
changed by driver patches, \Arch\ achieves over 95\% coverage on 12
patches in 3 drivers.
