%DIF PREAMBLE EXTENSION ADDED BY LATEXDIFF
%DIF UNDERLINE PREAMBLE
\RequirePackage[normalem]{ulem}
\RequirePackage{color}\definecolor{RED}{rgb}{1,0,0}\definecolor{BLUE}{rgb}{0,0,1}
\providecommand{\DIFadd}[1]{{\protect\color{blue}\uwave{#1}}}
\providecommand{\DIFdel}[1]{{\protect\color{red}\sout{#1}}}
%DIF SAFE PREAMBLE
\providecommand{\DIFaddbegin}{}
\providecommand{\DIFaddend}{}
\providecommand{\DIFdelbegin}{}
\providecommand{\DIFdelend}{}
%DIF FLOATSAFE PREAMBLE
\providecommand{\DIFaddFL}[1]{\DIFadd{#1}}
\providecommand{\DIFdelFL}[1]{\DIFdel{#1}}
\providecommand{\DIFaddbeginFL}{}
\providecommand{\DIFaddendFL}{}
\providecommand{\DIFdelbeginFL}{}
\providecommand{\DIFdelendFL}{}
%DIF END PREAMBLE EXTENSION ADDED BY LATEXDIFF

%% Important Dates
%% Paper titles and abstracts due: January 10, 2012, 11:59 p.m. EST
%% Complete paper submissions due: January 17, 2012,
%% 11:59 p.m. EST
%% Notification to authors: March 26, 2012
%% Final papers due: May 2, 2012

%------------------------------------------------------------------------------
%                                  Preamble. 
%------------------------------------------------------------------------------
%\documentclass[letterpaper,twocolumn,10pt]{article}
%\documentclass[nocopyrightspace,preprint,plainnat,9pt]{acm_proc_article-sp}
%\documentclass[nocopyrightspace,preprint,plainnat,9pt]{sig-alternate}
%\documentclass[nocopyrightspace,preprint,plainnat,10pt]{sigplanconf}
\documentclass[10pt,twocolumn]{article}
%DIF 16-18c16
%DIF < %\usepackage{styles/usenix_2011} % This is a modified version from last time
%DIF < \usepackage{fullpage}
%DIF < \usepackage[margin=1in]{geometry}
%DIF -------
\usepackage{styles/usenix_2011} % This is a modified version from last time %DIF > 
%DIF -------
%\usepackage{styles/usenix_2012} % This is the one from the web page this year
\usepackage{graphicx}
%DIF 21c19
%DIF < %\usepackage{fancyvrb}
%DIF -------
\usepackage{fancyvrb} %DIF > 
%DIF -------
\usepackage[small,compact]{titlesec}
\usepackage{times}
\usepackage{multirow}
\usepackage{textcomp}
%DIF 26-27d24
%DIF < \usepackage[pdftex, colorlinks=true, citecolor=black, linkcolor=black,
%DIF < citebordercolor={0 0 0}, urlcolor=black]{hyperref}
%DIF -------

%DIF 29-40c25-26
%DIF < %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%DIF < % This junk shrinks the amount of space devoted to the title.
%DIF < % The package is not installed though and hopefully we'll not need it.
%DIF < %%\usepackage{titling/titling}
%DIF < %%\setlength{\droptitle}{-0.5in}
%DIF < %\pretitle{\begin{center}\LARGE}
%DIF < %\posttitle{\par\end{center}\vskip 0.5em}
%DIF < %\preauthor{\begin{center}\large \lineskip 0.5em\begin{tabular}[t]{c}}
%DIF < %\postauthor{\end{tabular}\par\end{center}}
%DIF < %\predate{\begin{center}\large}
%DIF < %%\postdate{\par\end{center}\vskip -1em}
%DIF < %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%DIF -------
%\usepackage[T1]{fontenc} %DIF > 
%\usepackage{pslatex} %DIF > 
%DIF -------

\usepackage{styles/tweaklist}
%this sets the spacings in the itemize environment
\renewcommand{\itemhook}{\setlength{\topsep}{0pt}%
 \setlength{\itemsep}{0pt}%
 \setlength{\parsep}{0ex}%
}

% this sets the spacings in the enumerate environment
\renewcommand{\enumhook}{\setlength{\topsep}{0pt}%
  \setlength{\itemsep}{0pt}%
  \setlength{\parsep}{0ex}%
}

% this sets the spacings in the description environment
\renewcommand{\descripthook}{\setlength{\topsep}{0pt}%
 \setlength{\itemsep}{0pt}%
  \setlength{\parsep}{0ex}%
}
%DIF 60a46-48
 %DIF > 
\usepackage[pdftex, colorlinks=true, citecolor=black, linkcolor=black, %DIF > 
citebordercolor={0 0 0}, urlcolor=black]{hyperref} %DIF > 
%DIF -------

\input{macros.tex}

%% % Tom Reps' space saving tips.
%% \setlength{\abovecaptionskip}{5pt}
%% \setlength{\belowcaptionskip}{5pt}
%% \setlength{\intextsep}{5pt} 
%% \setlength{\floatsep}{5pt} 
%% \setlength{\abovedisplayskip}{5pt}
%% \setlength{\belowdisplayskip}{5pt}
%% \setlength{\topskip}{0pt}
%% \setlength{\parskip}{0pt}
%% \setlength{\topsep}{0pt}
%% \setlength{\partopsep}{0pt}
%% \setlength{\itemsep}{0pt}

%------------------------------------------------------------------------------
%                              Title and Authors.
%------------------------------------------------------------------------------
%DIF PREAMBLE EXTENSION ADDED BY LATEXDIFF
%DIF UNDERLINE PREAMBLE %DIF PREAMBLE
\RequirePackage[normalem]{ulem} %DIF PREAMBLE
\RequirePackage{color}\definecolor{RED}{rgb}{1,0,0}\definecolor{BLUE}{rgb}{0,0,1} %DIF PREAMBLE
\providecommand{\DIFadd}[1]{{\protect\color{blue}\uwave{#1}}} %DIF PREAMBLE
\providecommand{\DIFdel}[1]{{\protect\color{red}\sout{#1}}}                      %DIF PREAMBLE
%DIF SAFE PREAMBLE %DIF PREAMBLE
\providecommand{\DIFaddbegin}{} %DIF PREAMBLE
\providecommand{\DIFaddend}{} %DIF PREAMBLE
\providecommand{\DIFdelbegin}{} %DIF PREAMBLE
\providecommand{\DIFdelend}{} %DIF PREAMBLE
%DIF FLOATSAFE PREAMBLE %DIF PREAMBLE
\providecommand{\DIFaddFL}[1]{\DIFadd{#1}} %DIF PREAMBLE
\providecommand{\DIFdelFL}[1]{\DIFdel{#1}} %DIF PREAMBLE
\providecommand{\DIFaddbeginFL}{} %DIF PREAMBLE
\providecommand{\DIFaddendFL}{} %DIF PREAMBLE
\providecommand{\DIFdelbeginFL}{} %DIF PREAMBLE
\providecommand{\DIFdelendFL}{} %DIF PREAMBLE
%DIF END PREAMBLE EXTENSION ADDED BY LATEXDIFF

\begin{document}

\title{\DIFdelbegin \DIFdel{\textbf{SymDrive:  Testing Drivers without Devices}}\DIFdelend \DIFaddbegin \DIFadd{\textbf{\Large SymDrive:  Who Needs a Device to Test a Driver?}}\DIFaddend }
%DIF < \author{\today}
\author{\DIFdelbegin \DIFdel{Matthew J. Renzelmann, Asim Kadav and Michael M. Swift }%DIFDELCMD < \\
%DIFDELCMD <   %%%
\DIFdel{Computer Sciences Department,
  University of Wisconsin--Madison}%DIFDELCMD < \\
%DIFDELCMD <   \small %%%
\DIFdel{\textsf{\{mjr,kadav,swift\}@cs.wisc.edu}}\DIFdelend \DIFaddbegin \today\DIFaddend }
%DIF > \author{Matthew J. Renzelmann, Asim Kadav and Michael M. Swift \\
%DIF >   Computer Sciences Department,
%DIF >   University of Wisconsin--Madison\\
%DIF >   \small \textsf{\{mjr,kadav,swift\}@cs.wisc.edu}}
% \authorinfo{}{}{}
\date{}

\maketitle
\DIFdelbegin %DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend %\raggedbottom
%\widowpenalty=1
%\clubpenalty=1

% Use the following at camera-ready time to suppress page numbers.
% Comment it out when you first submit the paper for review.
\DIFdelbegin %DIFDELCMD < \thispagestyle{empty}
%DIFDELCMD < \pagestyle{empty}
%DIFDELCMD < %%%
\DIFdelend %DIF >  \thispagestyle{empty}

\begin{abstract}
Device-driver development and testing is a complex and error-prone
undertaking.  For example, \DIFdelbegin \DIFdel{testing error-handling code is difficult,
because it requires faulty inputs from the device.  In addition, }\DIFdelend a single driver may support dozens of
devices, and a developer may not have access to any of them. \DIFdelbegin \DIFdel{Consequently}\DIFdelend \DIFaddbegin \DIFadd{As a
result}\DIFaddend , many Linux driver patches include the comment ``compile tested
only.''  \DIFaddbegin \DIFadd{Furthermore, testing error-handling code is difficult, as it
requires faulty inputs from the device.
}\DIFaddend 

\Arch\ is a system for testing Linux and FreeBSD drivers without their
devices\DIFdelbegin \DIFdel{present}\DIFdelend . The system uses symbolic execution to remove the need for
hardware, and provides three new features beyond prior
symbolic-testing tools. First, \Arch\ greatly reduces the effort of
testing a new driver with a static-analysis and source-to-source
transformation tool. Second, \Arch\ \DIFdelbegin \DIFdel{checkers are ordinary C code }\DIFdelend \DIFaddbegin \DIFadd{allows checkers to be written as
ordinary C }\DIFaddend and execute in the kernel, where they have full access to
kernel and driver state. Finally, \Arch\ provides an execution-tracing
tool to identify how a patch changes I/O to the device and to compare
\DIFdelbegin \DIFdel{device-driver }\DIFdelend \DIFaddbegin \DIFadd{device driver }\DIFaddend implementations.  In applying \Arch\ to 21 Linux drivers
and 5 FreeBSD drivers, we found \howmanybugs\ bugs.

% \howmanydrivers = 21 + 5

\end{abstract}

%------------------------------------------------------------------------------
%                                Main Contents. 
%------------------------------------------------------------------------------
%DIF < \pagestyle{plain}
\DIFaddbegin \pagestyle{plain}
\DIFaddend \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}.  The need for hardware can prevent
testing altogether: \DIFdelbegin \DIFdel{Linux and FreeBSD }\DIFdelend kernel developers often do not have access to the
device needed by a driver, and thus over two dozen driver patches
include the comment ``compile tested only,'' indicating that the
developer was unable or unwilling to run the driver.

%\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

Even with hardware, it is difficult to test error-handling code that
runs in response to a device error or malfunction. 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. In addition, thorough testing of failure-handling code
is time consuming and requires exhaustive fault-injection tests with a
range of faulty inputs.

\DIFdelbegin \DIFdel{Static }\DIFdelend \DIFaddbegin \DIFadd{While static }\DIFaddend analysis tools such as Coverity~\cite{coverity04} and
Microsoft's Static Driver Verifier~\cite{microsoft10} can find many
bugs\DIFdelbegin \DIFdel{quickly.  However}\DIFdelend , these tools are tuned for fast analysis of large amounts of code
and miss large aspects of driver behavior, such as bugs that propagate
across multiple invocations of the driver.

%\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, and allows (i) driver code to execute without the
device present, and (ii) more thorough coverage of driver code,
including error handling code. While DDT~\cite{kcc10} and
\see~\DIFdelbegin %DIFDELCMD < \cite{ckc11, ckc12} %%%
\DIFdelend \DIFaddbegin \cite{ckc11} \DIFaddend applied symbolic execution to driver testing\DIFdelbegin \DIFdel{previously}\DIFdelend , these
systems did not address the many complexities of symbolic execution as
evidenced by \DIFdelbegin \DIFdel{their application to }\DIFdelend \DIFaddbegin \DIFadd{testing }\DIFaddend only a few drivers in two classes \DIFdelbegin \DIFdel{. Testing a wider variety of drivers}\DIFdelend \DIFaddbegin \DIFadd{on one
bus. Testing additional drivers, classes of drivers, or drivers on
other buses }\DIFaddend requires substantial developer effort to encode the
driver/bus interfaces into the testing tool.

This paper presents {\em \Arch}, a system to test Linux and FreeBSD
drivers without devices.  Compared with prior symbolic execution
tools, \Arch\ greatly reduces developer effort. \Arch\ uses static
analysis to identify key features of the driver code, such as
entry-point functions and loops. \DIFdelbegin \DIFdel{With }\DIFdelend \DIFaddbegin \DIFadd{Based on }\DIFaddend this analysis, \Arch\ produces
an instrumented driver with callouts to test code\DIFdelbegin \DIFdel{that allows many drivers to }\DIFdelend \DIFaddbegin \DIFadd{, and hints to improve
testing performance. As a result, many drivers can }\DIFaddend be tested with no
modifications. The remainder require a few annotations \DIFdelbegin \DIFdel{to assist symbolic execution at
locations that }\DIFdelend \DIFaddbegin \DIFadd{at
locations identified by }\DIFaddend \Arch\ \DIFdelbegin \DIFdel{identifies}\DIFdelend \DIFaddbegin \DIFadd{to assist symbolic execution}\DIFaddend .

We designed \Arch\ for three purposes. First, a driver developer can
use \Arch\ to test \DIFdelbegin \DIFdel{driver patches by thoroughly executing all branches through }\DIFdelend \DIFaddbegin \DIFadd{a patch and target thorough exploration of }\DIFaddend the
changed code. 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, similar to static analysis tools, and perform broad
testing of an entire driver 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.~\DIFdelbegin %DIFDELCMD < \cite{ckc11,
%DIFDELCMD <   ckc12} %%%
\DIFdelend \DIFaddbegin \cite{ckc11} \DIFaddend ,
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 \DIFdelbegin \DIFdel{developers}\DIFdelend \DIFaddbegin \DIFadd{a developer}\DIFaddend , such as
identifying the driver/kernel interface, \DIFdelbegin \DIFdel{and also provides }\DIFdelend \DIFaddbegin \DIFadd{as well as providing }\DIFaddend hints to
\see\ to speed testing. \DIFdelbegin \DIFdel{Consequently}\DIFdelend \DIFaddbegin \DIFadd{As a result}\DIFaddend , little effort is needed to apply
\Arch\ to additional drivers, \DIFdelbegin \DIFdel{driver classes }\DIFdelend \DIFaddbegin \DIFadd{classes of drivers}\DIFaddend , 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:
matched allocation/free calls across entry points, no memory leaks,
and proper use of kernel APIs.

In addition, \Arch\ provides an {\em execution-tracing} mechanism for
logging the path of driver execution, including the instruction
pointer and stack trace \DIFdelbegin \DIFdel{of }\DIFdelend \DIFaddbegin \DIFadd{for }\DIFaddend 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
\DIFaddbegin \DIFadd{different }\DIFaddend operating systems.

We demonstrate \Arch's value by applying it to \howmanydrivers\ drivers,
and \DIFdelbegin \DIFdel{find }\DIFdelend \DIFaddbegin \DIFadd{found }\DIFaddend \howmanybugs\ bugs, including two security vulnerabilities.
We also \DIFdelbegin \DIFdel{find }\DIFdelend \DIFaddbegin \DIFadd{found }\DIFaddend 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, which is largely
limited by the ability of user-mode tests to invoke driver entry
points.  When \DIFdelbegin \DIFdel{we use }%DIFDELCMD < \Arch\ %%%
\DIFdel{to execute code
changed by }\DIFdelend \DIFaddbegin \DIFadd{applied to }\DIFaddend driver patches, \Arch\ \DIFdelbegin \DIFdel{achieves }\DIFdelend \DIFaddbegin \DIFadd{achieved }\DIFaddend over 95\%
coverage on 12 patches in 3 drivers.

\section{Motivation}

The goal of our work is to improve driver quality through more
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, which consist both of other tools as well as testing
on real hardware.  Second, \Arch\ must minimize developer effort to
test a new driver and therefore support many device classes, buses,
and operating systems. Finally, \Arch\ must be fast enough that 
developers can apply it to each of their patches.

%DIF <  From Matt:  commented this out because of comment from reviewer 4G.
%DIF <  We don't make the deep/broad distinction later on like we used to,
%DIF <  so it may make sense just to cut it.
\DIFaddbegin \DIFadd{We have two use cases for }\Arch\DIFadd{: }{\em \DIFadd{deeper}} \DIFadd{testing of drivers, by
providing high coverage of individual patches, and }{\em \DIFadd{broader}}
\DIFadd{testing of drivers by allowing more people to test drivers and find
bugs.
}\DIFaddend 

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

%DIFDELCMD < %%%
\DIFdelend \subsection{Symbolic Execution}

\Arch\ uses symbolic execution to execute device-driver code without
the device being present.  Symbolic execution allows \DIFdelbegin \DIFdel{a program 's input }\DIFdelend \DIFaddbegin \DIFadd{program inputs }\DIFaddend 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 {\em 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 comparison can further constrain a value.  In places where
specific values are needed, such as printing a value,
the engine can {\em 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 shows \DIFdelbegin \DIFdel{the state of the executing path }\DIFdelend \DIFaddbegin \DIFadd{a stack trace }\DIFaddend at the failure site before
resuming execution of another path.

\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.
\DIFdelbegin \DIFdel{Each path is logically
similar to a thread executing a different outcome of a branch, and the
scheduler (}%DIFDELCMD < \Arch%%%
\DIFdel{) periodically switches execution to a different path.
}\DIFdelend 

\see\ supports {\em plug-ins}, which it invokes to record information
or to modify execution. \Arch\ relies on 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
a driver.

Symbolic execution eliminates the hardware requirement, because it can
use symbolic data for all device input. Alternative testing
approaches rely on a programmer to create a device
model~\cite{nelson:driver-model:plumbers:2011}. Models allow
driver/device interface verification, but require \DIFdelbegin \DIFdel{a large
}\DIFdelend \DIFaddbegin \DIFadd{much more
}\DIFaddend effort to faithfully replicate device behavior.

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.  As \Arch\ executes the driver code, it
effectively builds a model of the device's behavior by tracking
successful and failing execution paths, and finds bugs as it does so.

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

In \DIFdelbegin \DIFdel{comparison }\DIFdelend \DIFaddbegin \DIFadd{contrast }\DIFaddend 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 invokes many driver entry points in series, allowing it to
find bugs that span invocations, such as resource leaks. In contrast,
static analysis tools tend to focus on bugs 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}. It is useful to distinguish and
prioritize paths that successfully complete \DIFdelbegin \DIFdel{successfully.  For
example, if driver initialization fails, the operating system could
not otherwise invoke most driver entry points}\DIFdelend \DIFaddbegin \DIFadd{initialization and allow
the remainder of the driver to execute}\DIFaddend . \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.  \DIFdelbegin \DIFdel{For example, the annotations often examine kernel function parameters,
and modify the memory of the current path on the basis of the
parameters.  }\DIFdelend 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, such as
unloading a driver, because of path explosion.
%
\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 \DIFdelbegin \DIFdel{over 1,000 }\DIFdelend \DIFaddbegin \DIFadd{2,230 }\DIFaddend lines of code\DIFdelbegin \DIFdel{specific to this
  driver class}\DIFdelend . 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 most or all of the testing
  effort.
%
%
\paragraph{Specification.} Finally, symbolic execution by itself does
  not provide any specification of correct behavior.  A ``hello
  world'' driver is correct but does not initialize a network device.
  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 specification.


Thus, our work focuses on improving the state of the art to greatly
simplify the use of symbolic execution for testing, and 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.

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

The \Arch\ architecture focuses on thorough testing of drivers to
ensure the code does not crash, hang, or incorrectly use the
kernel/driver interface. \DIFdelbegin \DIFdel{We target }\DIFdelend \DIFaddbegin \DIFadd{Thus, }\Arch\ \DIFadd{specifically targets }\DIFaddend test
situations where the driver code is available, and uses that code to
simplify testing by combining symbolic execution, static
source-code analysis and transformation, and a fine-grained \tf.

%DIF > We have two primary goals for \Arch: (i) allow the developer to verify
%DIF > and validate any relevant part or parts of a driver to the greatest
%DIF > extent possible, while (ii) minimizing the developer effort for
%DIF > testing each new driver.  The first goal enables {\em deeper} testing
%DIF > of drivers for higher quality code, while the second goal enables {\em
%DIF >   broader} testing of drivers by eliminating the requirements for
%DIF > hardware.
\DIFaddbegin 

%DIF >  \subsection{Overview} % Maybe not have a separate ``overview''
%DIF >  section and just leave the text under the main ``Design'' heading?

\DIFaddend 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.

We implemented \Arch\ for Linux and FreeBSD, as these kernels provide
a large number of drivers to test. The design applies to any operating
system supported by \see\DIFdelbegin %DIFDELCMD < \ %%%
\DIFdel{(32-bit OSes that run on QEMU~}%DIFDELCMD < \cite{b05b}%%%
\DIFdel{)}\DIFdelend , and only the \tf\ code is specialized to the
OS.  We made small, \DIFdelbegin \DIFdel{conditionally compiled }\DIFdelend \DIFaddbegin \DIFadd{conditionally-compiled }\DIFaddend changes to both kernels to
print failures and \DIFdelbegin \DIFdel{stack traces }\DIFdelend \DIFaddbegin \DIFadd{panics }\DIFaddend to the \see\ log\DIFdelbegin \DIFdel{and }\DIFdelend \DIFaddbegin \DIFadd{, as well as }\DIFaddend 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\DIFdelbegin \DIFdel{, which consists of a
}%DIFDELCMD < \Arch%%%
\DIFdel{-specific plugin as well as changes to the underlying system}\DIFdelend ; (ii) symbolic devices to provide symbolic
hardware input to the driver; (iii) a {\em \tf} executing within the
kernel that guides symbolic execution; (iv) \DIFdelbegin \DIFdel{the }\DIFdelend {\em \ds}\DIFaddbegin \DIFadd{, a
}\DIFaddend static-analysis and code transformation tool \DIFdelbegin \DIFdel{to analyze and
prepare }\DIFdelend \DIFaddbegin \DIFadd{that analyzes and
prepares }\DIFaddend 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}
\DIFdelbeginFL %DIFDELCMD < \vspace{-0.3in}
%DIFDELCMD < %%%
\DIFdelendFL \DIFaddbeginFL \vspace{-0.2in}
\DIFaddendFL \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}
\DIFdelbeginFL %DIFDELCMD < \vspace{-0.1in}
%DIFDELCMD < %%%
\DIFdelendFL %DIF > \vspace{-0.2in}
\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}

\subsection{Virtual Machine}
\label{section:vm}

\Arch\ uses \see~\DIFdelbegin %DIFDELCMD < \cite{ckc12} %%%
\DIFdelend \DIFaddbegin \cite{ckc11} \DIFaddend version 1.1-10.09.2011, itself based on
QEMU~\cite{b05b} and KLEE \cite{cde08}, for symbolic execution.  \see\
provides the execution environment and constraint solving capability
necessary for symbolic execution.  It also implements the path forking
that takes place as symbolic values are compared against each other.
All driver and kernel code, including the \tf, executes within the
\see\ VM.
\DIFdelbegin \DIFdel{Changes to }%DIFDELCMD < \see\ %%%
\DIFdel{fall into two categories: (i)
improved support for symbolic hardware, and (ii) the }%DIFDELCMD < \Arch\ 
%DIFDELCMD < %%%
\DIFdel{path-selection mechanism, which is an }%DIFDELCMD < \see\ %%%
\DIFdel{plugin.
}\DIFdelend 

We augment \see\ with new opcodes for the \tf\ that pass information
into the VMM and its plugins.  \DIFdelbegin %DIFDELCMD < \Arch%%%
\DIFdelend \DIFaddbegin \see\DIFaddend \ uses invalid x86 opcodes for
communication with the VMM\DIFdelbegin \DIFdel{to provide additional control over the
executing code.  These opcodesare }\DIFdelend \DIFaddbegin \DIFadd{.  }\Arch\ \DIFadd{adds opcodes, }\DIFaddend inserted into driver
code by \ds\ \DIFdelbegin \DIFdel{and }\DIFdelend \DIFaddbegin \DIFadd{or }\DIFaddend invoked by the \tf\DIFdelbegin \DIFdel{.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{The purpose of the opcodes is to communicate source-level information
to the VMM, which uses the information to guide the driver's
execution. The opcodes fall into three sets that: (i) }\DIFdelend \DIFaddbegin \DIFadd{, to provide additional control over
the executing code. The new opcodes serve three purposes. First, a set
of opcodes }\DIFaddend control whether memory regions are symbolic, \DIFdelbegin \DIFdel{as }\DIFdelend \DIFaddbegin \DIFadd{and are used
}\DIFaddend when mapping data for DMA \DIFdelbegin \DIFdel{; (ii)
influence }\DIFdelend \DIFaddbegin \DIFadd{and for making data concrete.  Second, a set
of opcodes control }\DIFaddend path scheduling by adjusting priority, search
strategy, or killing other paths\DIFdelbegin \DIFdel{; and (iii) support tracing by turning it on/off
and providing stack information. }\DIFdelend \DIFaddbegin \DIFadd{. We discuss their use in the
following sections. Finally, a set of opcodes provide stack
information for tracing.
}\DIFaddend 

\ignore{
\begin{table}[t!]
\small
\centering
\begin{tabular}{p{1.2in}|p{1.7in}}
{\bf Opcode} & {\bf Description} \\
\hline
\hline

\codesm{make\_dma\_symbolic}, \codesm{free\_dma\_symbolic} & Allocate
/ deallocate regions of DMA memory. \\

\hline

\codesm{concretize} & Concretize all symbolic data in the current
state. \\

\hline
\hline

\codesm{prioritize}, \codesm{deprioritize} & Modify the relative
priority of the currently executing path. \\

\hline

\codesm{favor\_successful} & Toggle the heuristic that favors
successful path exploration at the expense of coverage. \\

\hline

\codesm{loop\_before}, \codesm{loop\_body} \codesm{loop\_after} &
Notify the VMM that a loop is beginning, executing its body, or
ending. \\

\hline

\codesm{kill\_all\_others} & Terminate all other paths but leave the
current one executing. \\

\hline
\hline

\codesm{driver\_call\_stack} & Notify the VMM of the location
of the current path in the code. \\

\hline

\codesm{enable\_tracing}, \codesm{disable\_tracing} & Enable / disable
tracing of I/O operations. \\

\end{tabular}
\caption{\small \bf Opcodes added in \Arch.}
\label{fig:table-opcodes}
\vspace{-0.2in}
\end{table}
} %% \ignore

\DIFdelbegin \subsection{\DIFdel{Symbolic Devices}}
%DIFAUXCMD
\addtocounter{subsection}{-1}%DIFAUXCMD
%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{Drivers interact with devices according to well-defined, narrow
interfaces.  For PCI device drivers, this interface is comprised of
I/O memory accessed via normal loads and stores, port I/O
instructions, bus operations, DMA memory, and interrupts.  Drivers
using other buses, such as SPI and }%DIFDELCMD < \itwoc%%%
\DIFdel{, use wrapper functions for
similar operations.
}%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF <  From Matt - I cut the following paragraph as we seem to cover this
%DIF <  in the subsequent sections.
%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < To provide symbolic hardware, \see\ provides symbolic data of the
%DIF < appropriate size each time the driver performs a read operation using
%DIF < memory or port I/O.  Similarly, the VMM treats the contents of DMA
%DIF < memory, indicated through DMA mapping functions, as symbolic.  The VMM
%DIF < does not insert symbolic interrupts; instead, \Arch\ invokes the
%DIF < driver's interrupt handler each time control passes from the driver to
%DIF < the kernel. For buses such as \itwoc\ that use I/O wrapper functions,
%DIF < \Arch\ rewrites the wrappers to return symbolic data.
%DIFDELCMD < 

%DIFDELCMD < \Arch\ %%%
\DIFdel{provides a symbolic device for the driver under test, while at
the same time emulating the other devices in the
system. A symbolic
device provides three key behaviors. First, it must be discovered, so
the kernel loads the appropriate driver. Second, it must provide
methods to read from and write to the device and return symbolic data
from reads. Third, it supports interrupts and DMA, if needed.
}%DIFDELCMD < \Arch\ %%%
\DIFdel{currently supports 5 buses on Linux: PCI (and its variants),
}%DIFDELCMD < \itwoc\ %%%
\DIFdel{(including SMBus), Serial Peripheral Interface (SPI), General
Purpose I/O (GPIO), and Platform;}\footnote{\DIFdel{The ``platform bus'' is a
  Linux-specific term that encompasses many embedded devices.  Linux's
  ARM implementation, for example, supports a variety of SoCs, each
  with its own set of integrated devices.  The drivers for these
  devices are often of the ``platform'' type.}} %DIFAUXCMD
\addtocounter{footnote}{-1}%DIFAUXCMD
\DIFdel{and the PCI bus on
FreeBSD.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\paragraph{\DIFdel{Device Discovery.}}
%DIFAUXCMD
\addtocounter{paragraph}{-1}%DIFAUXCMD
%DIF < \fixme{Julia: this section is rather technical -- can it be simplified
%DIF <   and/or can we provide an example}
%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{When possible, }%DIFDELCMD < \Arch\ %%%
\DIFdel{creates symbolic devices in the }%DIFDELCMD < \see\ %%%
\DIFdel{virtual
machine and lets existing bus code discover the new device and load
the appropriate driver.  For some buses, such as }%DIFDELCMD < \itwoc%%%
\DIFdel{, the kernel or
another driver normally creates a statically configured device object
during initialization. For such devices, we created a small kernel
module, consisting of 715 lines of code, that creates the desired
symbolic device.
}%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%DIF <  one reviewer wanted to know why we don't do USB.  Here's an example
%DIF <  response that's way too long
%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < We believe SymDrive
%DIF < would work with USB, but would require a more effort to implement a
%DIF < symbolic bus.  USB device drivers interface with other drivers lower
%DIF < in a stack.  The host controller interface driver communicates with
%DIF < the hardware, and modern operating systems typically only need one
%DIF < such driver for USB 1.0, 2.0, and 3.0.  Supplying symbolic data at
%DIF < this level of abstraction is not practical, because it would need to
%DIF < pass through the host controller driver, and likely generate many
%DIF < uninteresting paths.
%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < To address this issue, we would need to write a symbolic bus similar
%DIF < to the one used by SymDrive's I2C support.  I2C provides a similar,
%DIF < high-level communication interface with the device, implemented in
%DIF < Linux's i2c-core and one of the various chip-specific drivers,
%DIF < e.g. PIIX4.  We've not done a similar implementation for USB because
%DIF < of time constraints.
%DIF < %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < For example, \Arch\ uses \see's symbolic
%DIF < hardware plugin to create a virtual PCI device with the desired I/O
%DIF < memory configuration and PCI identifiers, both easily found in
%DIF < driver source code. This device triggers the PCI code in Linux to load the
%DIF < driver.
%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF <  Edited to add that a number of drivers also create these devices.
%DIF <  For example, many PCI-E video cards have thermal monitoring
%DIF <  features, and these temperature sensors are often I2C, so the video
%DIF <  card driver then creates the corresponding I2C device.
%DIFDELCMD < 

%DIFDELCMD < \Arch\ %%%
\DIFdel{can make the device configuration space symbolic after loading
the driver by returning symbolic data from PCI bus functions with the
}%DIFDELCMD < \tf %%%
\DIFdel{(similar to }%DIFDELCMD < \see%%%
\DIFdel{'s NDIS driver support).  PCI devices use this
region of I/O memory for plug-and-play information, such as the vendor
and device identifiers.  If this memory is symbolic, the driver will
execute different paths for each of its supported devices. Other buses
have similar configuration data, such as ``platform data'' on the SPI
bus. A developer can copy this data from the kernel source and provide
it when creating the device object, or make it symbolic for additional
code coverage.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\paragraph{\DIFdel{Symbolic I/O.}}
%DIFAUXCMD
\addtocounter{paragraph}{-1}%DIFAUXCMD
\DIFdel{Most Linux and FreeBSD drivers do a mix of programmed I/O and DMA.
}%DIFDELCMD < \Arch\ %%%
\DIFdel{supports two forms of programmed I/O. For drivers that perform
I/O through hardware instructions, such as }%DIFDELCMD < \codesm{inb}%%%
\DIFdel{, or through
memory-mapped I/O, }%DIFDELCMD < \Arch\ %%%
\DIFdel{directs }%DIFDELCMD < \see\ %%%
\DIFdel{to ignore write operations,
because they do not return values that influence driver execution, and
return symbolic data from reads. The }%DIFDELCMD < \tf\ %%%
\DIFdel{overrides bus I/O functions, such as those used in }%DIFDELCMD < \itwoc\ %%%
\DIFdel{drivers, to function analogously.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\paragraph{\DIFdel{Symbolic Interrupts.}}
%DIFAUXCMD
\addtocounter{paragraph}{-1}%DIFAUXCMD
\DIFdel{After a driver registers an interrupt handler, the }%DIFDELCMD < \tf\ %%%
\DIFdel{invokes the interrupt
handler on every transition from the driver into the kernel.  This
model ensures the interrupt handler is called often enough to keep the
driver executing successfully, but represents a trade-off between
realism and complexity. A real device may generate interrupts more often,
including while the driver executes. However, testing the driver's
response to this many potential interrupts would result in path
explosion.  A real device may also raise fewer interrupts, in which case
case our approach tests the driver with spurious interrupts.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\paragraph{\DIFdel{Symbolic DMA.}}
%DIFAUXCMD
\addtocounter{paragraph}{-1}%DIFAUXCMD
\DIFdel{When a driver invokes a DMA mapping function, such as
}%DIFDELCMD < \codesm{dma\_alloc\_coherent}%%%
\DIFdel{, the }%DIFDELCMD < \tf\ %%%
\DIFdel{uses an }%DIFDELCMD < \see\ %%%
\DIFdel{opcode to make
the memory act like a memory-mapped I/O region: each read returns a
new symbolic value and writes have no effect. Discarding writes to DMA
memory reflects the ability of the device to write the data via DMA at
any time.  The driver should not assume that data written here will be
available subsequently. When the driver unmaps the memory, the
}%DIFDELCMD < \tf\ %%%
\DIFdel{directs }%DIFDELCMD < \see\ %%%
\DIFdel{to revert the region to normal symbolic data, so
writes are seen by subsequent reads.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend \subsection{Test Framework}

\DIFdelbegin \DIFdel{The }%DIFDELCMD < \tf\ %%%
\DIFdel{is a kernel module executing with the virtual machinethat
assists symbolic execution and executes checkers.  }\DIFdelend \Arch\ \DIFdelbegin \DIFdel{relies on the
}\DIFdelend \DIFaddbegin \DIFadd{relies on a }{\em \DIFaddend \tf\DIFdelbegin %DIFDELCMD < \ %%%
\DIFdelend \DIFaddbegin }\DIFadd{, executing within the virtual machine, }\DIFaddend to
guide and monitor symbolic execution in three ways.  First, the \tf\
implements policy regarding which paths to prioritize or deprioritize.
Second, the \tf\ may inject additional symbolic data to increase code
coverage.  As mentioned above, it implements symbolic I/O interfaces
for some device classes. Finally, it provides the VMM with a stack
trace for {\em execution tracing}, which produces a trace of the
driver's I/O operations.

The \tf\ \DIFaddbegin \DIFadd{is a kernel module that }\DIFaddend supports several load-time 
parameters for controlling its behavior. When loading the \tf\ with
\codesm{insmod} or FreeBSD's \codesm{kldload}, developers can direct
the \tf\ to enable high-coverage mode (described in
Section~\ref{sec:exec-broadly}), tracing, or a \DIFdelbegin \DIFdel{specific }\DIFdelend symbolic device.
To configure the device, developers pass the device's I/O capabilities
and name as parameters. Thus, developers can script the creation of
symbolic devices to automate testing.

\Arch\ has to address two conflicting goals in testing drivers: (i)
executing as far as possible along a path, to complete initialization
and expose the rest of the driver's functionality; and (ii) executing
as much code as possible within each function for thoroughness.

\subsubsection{Reaching Deeply}
\label{sec:exec-broadly}
A key challenge in fully testing drivers is symbolically executing
branch-heavy code, such as loops and initialization code that probes
hardware. \Arch\ relies on two techniques to limit path explosion in
these cases: {\em favor-success scheduling} and {\em loop
  elision}. \DIFdelbegin \DIFdel{These techniques allow developers to execute }\DIFdelend \DIFaddbegin \DIFadd{Executing }\DIFaddend further into a driver \DIFdelbegin \DIFdel{, and test functionalitythat is only available after
initialization }\DIFdelend \DIFaddbegin \DIFadd{often exposes more
functionality, such as code the kernel invokes only after
initialization has completed}\DIFaddend .

\paragraph{Favor-success scheduling.} Executing past driver
initialization is difficult because the code \DIFdelbegin \DIFdel{often has many conditionals }\DIFdelend \DIFaddbegin \DIFadd{has many conditional
branches }\DIFaddend to support multiple chips and configurations.
Initializing a sound driver, for example, may require branching on
hardware-specific details over a thousand times. Each branch creates additional
paths to explore.

\Arch\ mitigates this problem with a {\em favor-success}
path-selection algorithm that prioritizes successfully executing
paths, making it a form of best-first search.  Notifications from the
\tf\ increase the priority of the current path at every successful
function return, both within the driver and at the driver/kernel
interface. Higher priority causes the current path to be explored
further before switching to another path.

% Next paragraph:
% Linux uses negative errno values, whereas FreeBSD uses positive
% errno values.  The text does not distinguish this detail but it
% doesn't seem important.

At every function exit, the \tf\ notifies \see\ of whether the
function completed successfully, which enables the VMM to prioritize
successful paths to facilitate deeper exploration of code. The
\tf\ determines success based on the function's return value. For
functions returning integers, the \tf\ detects success when the
function returns a value other than an \codesm{errno}, which are
standard Linux and FreeBSD error values. On success, the \tf\ will notify the VMM
to prioritize the current path.  If the developer wishes to prioritize
paths using another heuristic, he/she can add an annotation
prioritizing any piece of code. We use this approach only in some
network drivers to select paths where the carrier is on, \DIFdelbegin \DIFdel{which }\DIFdelend \DIFaddbegin \DIFadd{to }\DIFaddend allow
execution of the driver's packet transmission code.

The \tf\ prunes paths when control returns to the kernel \DIFdelbegin \DIFdel{successfully }\DIFdelend to focus
symbolic execution just on the driver. It kills all other paths still
executing in the driver and uses an opcode to concretize all data in
the virtual machine, so the kernel executes on real values and will
not fork new paths.  This ensures that a single path runs in the
kernel, which allows developers to interact with the system and run
user-mode tests.

%
% E1000 checksum loop for reference
%
%     for (i = 0; i < (EEPROM_CHECKSUM_REG + 1); i++) {
%         if (e1000_read_eeprom(hw, i, 1, &eeprom_data) < 0) {
%             DEBUGOUT(``EEPROM Read Error\n'');
%             return -E1000_ERR_EEPROM;
%         }
%         checksum += eeprom_data;
%     }
%
%     if (checksum == (u16)EEPROM_SUM)
%         return E1000_SUCCESS;
%     else {
%         DEBUGOUT(``EEPROM Checksum Invalid\n'');
%         return -E1000_ERR_EEPROM;
%     }
%

\paragraph{Loop elision.} Loops are challenging for symbolic
execution, because each iteration may fork new paths.  \DIFdelbegin %DIFDELCMD < \Arch\ %%%
\DIFdel{addresses loops explicitly by prioritizing those paths that
exit them quickly.  When }%DIFDELCMD < \Arch\ %%%
\DIFdel{starts executing a loop's second
iteration, it checks whether the loop created any new paths on the
first iteration.  If so, }%DIFDELCMD < \Arch\ %%%
\DIFdel{automatically deprioritizes the path
that began the second loop iteration.  If a different path executes
the same loop for a second iteration, }%DIFDELCMD < \Arch\ %%%
\DIFdel{prioritizes this path on
subsequent iterations, hoping that it will terminate quickly.  The
rationale behind this heuristic is that it forces at least one other
possible path to execute the loop for one iteration, with the hope
that this other path will exit the loop.  If the loop executes more
than 20 iterations and continues generating paths, }%DIFDELCMD < \Arch\ %%%
\DIFdel{prints a
message warning of poor performance, since it was unable break out of
the loop early.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{This approach executes hardware polling loops efficiently and
automatically, and warns developers when loops cause
performance problems.  However, this approach may fail if a loop is
present in uninstrumented kernel code.  It can also result in worse
coverage of code that executes only if a polling loop times
out.  Nevertheless, we have not found these problems to be
significant.
}%DIFDELCMD < 

%DIFDELCMD < %%%
%DIF < For example, the E1000 network driver code shown in
%DIF < Figure~\ref{fig:eeprom} calculates a checksum over the device EEPROM
%DIF < data, and only continues if the checksum is valid.
%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend \see\ provides
an ``EdgeKiller'' plugin that a developer may use to terminate complex
loops early, but requires developers to identify each loop's offset
into the driver binary~\DIFdelbegin %DIFDELCMD < \cite{ckc12}%%%
\DIFdelend \DIFaddbegin \cite{ckc11}\DIFaddend .  Moreover, loops that produce a
value, such as a checksum calculation, cannot exit early without
stopping the driver's progress.

%DIF <  Other problematic situations:
%DIF <  - Some driver entry points are called within loops in the kernel,
%DIF <  and we can't instrument those typically, unless we do something like
%DIF <  running SymGen over that code as well.
%DIF <  
%DIF <  These loop problems have become much less significant since S2E was
%DIF <  updated to defer calls to the constraint solver.
%DIF > For example, the E1000 network driver code shown in
%DIF > Figure~\ref{fig:eeprom} calculates a checksum over the device EEPROM
%DIF > data, and only continues if the checksum is valid.

\Arch\DIFdelbegin \DIFdel{'s approach extends the EdgeKiller plugin in two directions.  First, it allows developers to annotate driver source rather than
having to parse compiled code.  Second, source annotations persist
across driver revisions, whereas the binary offsets used in the
EdgeKiller pluginneed updating each time the driver changes.  %DIF < Finally, \Arch\ provides more flexibility in path selection than
%DIF < EdgeKiller's simple termination strategy, and allows driver execution
%DIF < to proceed along a successful path.  For example, EdgeKiller does not
%DIF < allow checksum loops to exit early successfully.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{Annotating code manually to improve its execution performance does
reduce }\DIFdelend \DIFaddbegin \ \DIFadd{addresses loops explicitly by prioritizing those paths that
exit the loop.  Thus, it does not need the EdgeKiller plugin.  For
loops that cannot be terminated, }\DIFaddend \Arch\DIFdelbegin \DIFdel{'s ability to find bugs in that code.  Wherever
annotations were needed in the drivers we examined, we strove to write
them in such a way as to execute the problematic loop at least once
before terminating early.  For example, after a checksum loop , we would
add a line to return a symbolic checksum value, which could then be
compared against a correct one}\DIFdelend \DIFaddbegin \ \DIFadd{notifies the developer during
testing if a loop creates too many paths. A developer can use
}\codesm{\#ifdef} \DIFadd{statements to disable the code during testing}\DIFaddend .

\subsubsection{Increasing Coverage}
\label{sec:exec-deeply}

\Arch\ provides a {\em high-coverage} mode for testing specific
functions, for example those modified by a patch. This mode 
changes the path-prioritization policy and the behavior of kernel
functions. When the developer loads the \tf\ module, he/she can
specify any driver function to execute in this mode.  

When execution enters the specified function, the \tf\ notifies \see\ to
favor unexecuted code (the default \see\ policy) rather than favoring
successful paths. The \tf\ also terminates all paths that return to
the kernel in order to focus execution within the driver. Finally,
when the driver invokes a kernel function, the \tf\ makes the return
value symbolic.  \DIFdelbegin \DIFdel{This mode is similar to the
local consistency mode in }%DIFDELCMD < \see%%%
\DIFdel{~}%DIFDELCMD < \cite{ckc12}%%%
\DIFdel{, but requires no
developer-provided annotations or plugins, and supports all kernel
functions that return standard error values.  }\DIFdelend For example, \codesm{kmalloc} returns a symbolic
value constrained to be either NULL or a valid address, which tests
error handling in the driver. \DIFdelbegin %DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend For the small number of kernel functions
that return non-standard values, \ds\ has a list of exceptions and how
to treat their return values. \DIFdelbegin \DIFdel{The full list of exceptions for Linux currently contains 100
functions shared across all supported drivers.  Of these, 64 are
hardware-access functions, such as }%DIFDELCMD < \codesm{inb} %%%
\DIFdel{and }%DIFDELCMD < \codesm{readl}%%%
\DIFdel{,
that always return symbolic data.
A further 14 functions are
arithmetic operations, such as }%DIFDELCMD < \codesm{div32}%%%
\DIFdel{.  The remaining 22
functions return negative numbers in successful cases, or are used by
the compiler to trigger a compilation failure when used incorrectly,
such as }%DIFDELCMD < \codesm{\_\_bad\_percpu\_size}%%%
\DIFdel{.
}\DIFdelend \DIFaddbegin \DIFadd{This mode is
similar to the local consistency mode in }\see\DIFadd{~}\cite{ckc11}\DIFadd{, but
requires no developer-provided annotations or plugins, and supports
all kernel functions that return standard error values.
}\DIFaddend 

%DIF <  I'm not very confident in these results.
%DIF < In addition, we did a first-pass static analysis of the drivers/base/*
%DIF < and drivers/pci/* kernel source files, and found that none of the 118
%DIF < functions exported from there return negative values on success, and
%DIF < so would need no special treatment with \Arch's favor-success
%DIF < scheduling, though 14 may need special treatment with \Arch's
%DIF < high-coverage mode.  We believe a static analysis of Linux error
%DIF < codes, as in~\cite{graal08}, would provide a complete accounting of
%DIF < this list.
\DIFdelbegin %DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend \Arch\ also improves code coverage by introducing additional symbolic
data, which allows a driver to execute code that requires specific
inputs from the kernel or applications.  \Arch\ can automatically make
a Linux driver's module parameters symbolic, which allows a driver to
execute with all possible parameters.  Checkers can also make
parameters to the driver symbolic, such as \codesm{ioctl} command
values. This allows all \codesm{ioctl} code to be tested with a single
invocation of the driver, because each comparison of the command will
fork execution. In addition, \see\ allows using symbolic data anywhere
in the virtual machine, so a user-mode \DIFdelbegin \DIFdel{test }\DIFdelend \DIFaddbegin \DIFadd{tests }\DIFaddend can pass symbolic data to
the driver.

% Note that FreeBSD does not support making parameters symbolic.
% FreeBSD module parameters don't exist -- instead, they access
% ``kernel environment variables'' or use the ``sysctl'' interface.
% We could add support for these in the future but don't have it yet.


%\fixme{Julia: did not like the next bit about PTR\_ERR.  She says
%  there are lots of functions like this.  Not a small number (over
%  1800 in a recent linux-next).  Presumably you do the same for NULL
%  as for negative ints?  It's not clear how short this list of
%  functions is.  Matt says: I'm confused by her comment.  All the
%  function does is cast a pointer to a long.  It does not necessarily
%  make sense to make a decision about whether to prioritize /
%  deprioritize based on that alone, which is why we have it in the
%  list.  As for the over 1800 functions like that, in those cases, it
%  likely is fine to apply the usual prio/deprio heuristic.  If we do
%  another example, there's e.g. test\_and\_set\_bit or any other
%  bit-manipulation function.  We currently have 23 functions in this
%  list though some I'd added preemptively and we may not need to leave
%  there.  We could also mention, e.g. \_\_bad\_percpu\_size which is a
%  function we should not instrument because it's specifically written
%  not to exist -- it's a C idiom to prevent compilation if the driver
%  developer specifies a bad parameter to certain macros/code.  Others
%  are \_\_bad\_size\_call\_parameter or \_\_xchg\_wrong\_size}


\DIFdelbegin \subsubsection{\DIFdel{Execution Tracing}}
%DIFAUXCMD
\addtocounter{subsubsection}{-1}%DIFAUXCMD
\DIFdelend \DIFaddbegin \subsection{\DIFadd{Execution Tracing}}
\DIFaddend 

The \tf\ can generate execution traces, which are helpful to compare
the execution of two versions of a driver.  For example, when a driver
patch introduces new bugs, the traces can be used to compare its
behavior against previous versions. In addition, developers can use
other implementations of the driver, even from another operating
system, to find discrepancies that may signify incorrect interaction
with the hardware.

A developer can enable tracing via a command-line tool that \DIFdelbegin \DIFdel{uses a
custom opcode to notify }%DIFDELCMD < \Arch%%%
\DIFdelend \DIFaddbegin \DIFadd{notifies
an }\see\DIFaddend \ \DIFdelbegin \DIFdel{to begin recording}\DIFdelend \DIFaddbegin \DIFadd{plugin to enable tracing}\DIFaddend . In this mode, an \see\ plugin
records every driver I/O operation, including reads and writes to
port, MMIO, and DMA memory, and the driver stack at the operation. The
\tf\ passes the current stack to \see\ on every function call.

The traces are stored as a trie (prefix tree) to represent multiple
paths through the code compactly\DIFdelbegin \DIFdel{(similar to }%DIFDELCMD < \see%%%
\DIFdel{)}\DIFdelend , and can be compared using the
\codesm{diff} utility.  However, \DIFdelbegin %DIFDELCMD < \Arch\ %%%
\DIFdel{annotates
each trace entry with the driver call stack at the I/O operation. This
facilitates analysis of specific functions and comparing drivers
function-by-function, which is useful since }\DIFdelend traces are subject to timing
variations and different thread interleavings.  \DIFaddbegin \DIFadd{Because the stack
information allows a developer to compare execution in specific
functions, the traces are most useful for comparing drivers
function-by-function.
}\DIFaddend 

\subsection{\ds}

All features of the \tf\ that interact with code, such as
favor-success scheduling, loop prioritization, and making kernel
return values symbolic are handled automatically via static analysis
and code generation.  The \ds\ tool analyzes driver code to identify
code relevant to testing, such as function boundaries and loops, and
instruments code with calls to the \tf\ and checkers.  \ds\ is built
using CIL~\cite{nmr+02}.

% \fixme{Julia: do we ever want to prioritize failure}

\paragraph{Stubs.}
\Arch\ interposes on all calls into and out of the driver with stubs
that call the \tf\ and checkers.  For each function in the
driver, \ds\ generates two stubs: a preamble, invoked at the top of
the function, and a postscript, invoked at the end. The generated code
passes the function's parameters and return value to these stubs, to
be used by checkers.  In addition, for each kernel function the driver
imports, \ds\ generates a stub function with the same signature that
wraps the function. These stubs ensure that the \tf\ can interpose on
all calls within the driver as well as calls into the kernel.

To support pre- and post-condition assertions, stubs invoke checkers
when the kernel calls into the driver or the driver calls into the
kernel. Checkers associated with a specific function
\codesm{function\_x} are named \codesm{function\_x\_check}. On the
first execution of a stub, the \tf\ looks for a corresponding checker
in the kernel symbol table. If such a function exists, the stub
records its address for future invocations.  While targeted at
functions in the kernel interface, this mechanism can invoke checkers
for any driver function.

Stubs employ a second lookup to find checkers associated with a
function pointer passed from the driver to the kernel, such as a PCI
probe function. Kernel stubs, when passed a function pointer, record
the function pointer and its purpose in a table. For example, the
Linux \codesm{pci\_register\_driver} function associates the address
of each function in the \codesm{pci\_driver} parameter with the name
of the structure and the field containing the function.  The stub for
the \codesm{probe} method of a \codesm{pci\_driver} structure is thus
named \codesm{pci\_driver\_probe\_check}.  FreeBSD drivers use a
similar technique.

% Note -
% FreeBSD drivers have a probe() function but these only look for the
% right PCI device and vendor IDs.  FreeBSD uses the term ``attach''
% to refer to their version of Linux's ``probe'' function.  FreeBSD
% also requires a slightly customized analysis to support the way they
% communicate these driver function addresses to the kernel, but the
% rest is the same.

Stubs detect that execution enters the driver by tracking the depth of
the call stack. The first function in the driver notifies the \tf\ at
its entry that driver execution is starting, and at its exit notifies
the \tf\ that control is returning to the kernel. 
\DIFdelbegin \DIFdel{Stubs also
communicate this information to the VMM so that it can make path
scheduling decisions based on function return values.
}\DIFdelend 

\paragraph{Instrumentation.}
\DIFdelbegin \DIFdel{As in the case of the stubs, the underlying principle behind }\DIFdelend \ds\DIFdelbegin \DIFdel{'s
instrumentation is to inform the VMM of source level information as it
executes the driver so it can make better decisions about which paths
to execute.  }%DIFDELCMD < \ds%%%
\DIFdelend \ instruments the start and end of each driver function with a call
into the stubs.  As part of the rewriting, it converts functions to
have a single exit point. It generates the same instrumentation for
inline functions, which are commonly used in the Linux and FreeBSD kernel/driver
interfaces.

\ds\ also instruments the start, end, and body of each loop with
\DIFdelbegin \DIFdel{calls to short functions that execute }%DIFDELCMD < \Arch%%%
\DIFdel{-specific }\DIFdelend opcodes.  These opcodes direct the VMM to prioritize and deprioritize paths
depending on whether they exit the loop quickly. This instrumentation
replaces \DIFdelbegin \DIFdel{most of the }\DIFdelend \DIFaddbegin \DIFadd{much of }\DIFaddend per-driver effort required by \see\ to identify
loops, as well as the per-class effort of writing a consistency model
for every function in the driver/kernel interface.  \ds\ inserts loop
opcodes into the driver, as shown in Figure~\ref{fig:auto-loop-annot},
to tell \see\ which paths exit the loop, and should receive a priority
boost.
\DIFdelbegin \footnote{\DIFdel{One interesting
  alternative is to prioritize paths that execute loops in their
  entirety.  The problem with this approach is that it may generate
  many states in the process, and slow testing.}}
%DIFAUXCMD
\addtocounter{footnote}{-1}%DIFAUXCMD
\DIFdelend 

For complex code that slows testing, \ds\ supports programmer-supplied annotations
to simplify or disable the code temporarily. \DIFdelbegin \DIFdel{Short loops
and those which do not generate states require no manual developer
effort.  Only loops that must execute for many iterations and generate
new paths on each iteration need manual annotation, which we implement
through C }%DIFDELCMD < \codesm{\#ifdef} %%%
\DIFdel{statements.  }\DIFdelend For example, \DIFdelbegin \DIFdel{the E1000 network
}\DIFdelend \DIFaddbegin \DIFadd{a }\DIFaddend driver
that verifies \DIFdelbegin \DIFdel{an checksum over EEPROM, and we modified it
accept }\DIFdelend \DIFaddbegin \DIFadd{a checksum over device data may need to be modified to
allow }\DIFaddend any checksum value.
\DIFdelbegin \DIFdel{We have found these cases to be rare.
When loops result poor performance, }%DIFDELCMD < \Arch\ %%%
\DIFdel{prints a warning with the
loop's location in the source code.  Identifying the root cause, such
as a checksum calculation, is then straightforward.
}\DIFdelend 

\begin{figure}[t!]
%\fvset{fontfamily=courier, fontsize=\footnotesize,xleftmargin=-5mm}
%\LVerbatimInput{code/e1000_checksum.c}
\begin{center}
\includegraphics[keepaspectratio=true,width=3in]{figures/auto_loop_annotation.pdf}
\end{center}
\vspace{-0.3in}
\caption{\small \bf \ds\ instruments the start, end, and body of loops
  automatically.  This code, from the 8139cp driver, was modified
  slightly since \ds\ produces preprocessed output.}
\label{fig:auto-loop-annot}
\vspace{-0.2in}
\end{figure}

\DIFdelbegin \subsection{\DIFdel{Limitations}}
%DIFAUXCMD
\addtocounter{subsection}{-1}%DIFAUXCMD
%DIFDELCMD < \Arch\ %%%
\DIFdel{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 warnings. In addition,
driver timers may fire at the wrong time causing the driver to behave
differently and report warnings.  Second, the quality of the checkers
is important.  If a checker verifies an execution property
incorrectly, then it will mistakenly report a bug even though the
driver is correct. Our current checkers have no known bugs, and 
we have not seen them generate false positives.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdel{Although we have observed no false negatives among the checkers we
wrote, }%DIFDELCMD < \Arch\ %%%
\DIFdel{cannot check for all kinds of bugs.  Of 11 common
security vulnerabilities~}%DIFDELCMD < \cite{chen:linux-vuln:apsys:2011}%%%
\DIFdel{, }%DIFDELCMD < \Arch\
%DIFDELCMD < %%%
\DIFdel{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, }%DIFDELCMD < \Arch%%%
\DIFdel{'s aggressive path pruning may terminate a path that
leads to a bug, causing }%DIFDELCMD < \Arch\ %%%
\DIFdel{to miss it. }%DIFDELCMD < \Arch\ %%%
\DIFdel{may also miss race
conditions, such as those requiring the interrupt handler to
interleave with another thread in a specific way.  Despite these
limitations, we find the tool to be a useful addition to the driver
development and patching process.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend %
% No references to \tf in here.
% ``Support library'' is the name for the checker-specific support
% library
% Includes object tracker, state variables
%

\section{Checkers}
\label{section:example-checkers}

A checker is a function interposing on control transfer between the
driver and kernel that verifies and validates driver behavior.  Each
function in the driver/kernel interface can, but need not, have its
own checker. Drivers invoke the checkers from stubs, described above,
which call separate checkers at every function in the driver/kernel
interface\DIFdelbegin \DIFdel{.  Since checkers run in the VM alongside the symbolically
executing driver, they can verify runtime properties along each tested
path}\DIFdelend \DIFaddbegin \DIFadd{, or even every function in the driver}\DIFaddend . 

The checkers use a {\em support library} that simplifies their
development by providing much of the functionality needed. \DIFdelbegin \DIFdel{The library
}\DIFdelend \DIFaddbegin \DIFadd{First, it
}\DIFaddend provides state variables to track the state of the driver and current
thread, such as whether it has registered itself successfully and
whether it can be rescheduled. The library also provides an object
tracker to record kernel objects currently in use in the driver. This
object tracker provides an easy mechanism to track whether locks have
been initialized and to discover memory leaks. Finally, the library
provides generic checkers for common classes of kernel objects, such
as locks and allocators. The generic checkers encode the semantics of
these objects, and thus do much of the work. For example, checkers for
a mutex lock and a spin lock use the same generic checker, as they
share semantics.

\begin{figure}
\begin{center}
\includegraphics[keepaspectratio=true,width=3in]{figures/test_example.pdf}
\end{center}
%\fvset{fontfamily=courier, fontsize=\footnotesize,xleftmargin=-5mm}
%\LVerbatimInput{code/test_example.c}
\vspace{-0.3in}
\caption{\small \bf Example checkers.  The first checker ensures that
  PCI drivers are registered exactly once.  The second verifies that a
  driver allocates memory with the appropriate \codesm{mem\_flags}
  parameter. The third ensures lock/unlock functions are properly
  matched.  Unlike Static Driver Verifier checkers~\cite{microsoft10}, these checkers can
  track any path-specific run-time state expressible in C.}
\label{fig:test_example}
\vspace{-0.2in}
\end{figure}

Writing a checker requires implementing checks within a call-out
function.  We have implemented 49 checkers comprising 564 lines of
code for a variety of common device-driver bugs using the library
API. Test \#1 in Figure~\ref{fig:test_example} shows an example
call-out for \codesm{pci\_register\_driver}. The driver-function stub
invokes the checker function with the parameters and return value of
the kernel function and sets a \codesm{precondition} flag to indicate
whether the checker was called before or after the function.  In
addition, the library provides the global \codesm{state} variable that
a checker can use to record information about the driver's
activity. As shown in this example, a checker can verify that the
state is correct as a precondition, and update the state based on the
result of the call. Checkers have access to the runtime state of the
driver and can store arbitrary data, so they can find interprocedural,
pointer-specific bugs that span multiple driver invocations.

Not every behavior requirement needs a checker. Symbolic execution
leverages the extensive checks already included as kernel debug options,
such as for memory corruption and locking. Most of these checks
execute within functions called {\em from} the driver, and thus will
be invoked on multiple paths.  In addition, any bug that causes a
kernel crash or panic will be detected by the operating system and therefore requires
no checker.

\ignore{, unless the driver returns to the kernel and concretizes
  symbolic data in such a way as to mask the bug.}

\paragraph{Execution Context.}
Linux prohibits the calling of functions that block when executing an
interrupt handler or while holding a spinlock. The execution context
checker verifies that flags passed to memory-allocation functions such
as \codesm{kmalloc} are valid in the context of the currently
executing code. The support library provides a state machine to track
the driver's current context using a stack.  When entering the driver,
the library updates the context based on the entry point.  The library
also supports locks and interrupt management \DIFaddbegin \DIFadd{functionality}\DIFaddend .  When the
driver acquires or releases a spinlock, for example, the library
pushes or pops the necessary context.

% From Matt:  removed this sentence:
%
% In contrast to static-analysis tools, there is no need to
%specify which driver entry points are non-blocking.

% From Matt re: previous sentence, better to say that we don't ``have
% to'' specify entry points as non-blocking, but it helps to.  We do
% push/pop spin lock blocking/non-blocking state, but we still need
% manual specification for blocking/non-blocking entry points if we
% want to check that.
%
% E.g. the code does not ``know'' that the PCI probe function is
% non-blocking -- we need to specify that.
%
% But the code does ``know'' if a driver function acquires a spinlock,
% calls into the kernel, which then calls back into the driver.


%\fixme{Julia: [not sure] specify
%  which entry points are not allowed to block?  Are the only relevant
%  locks the ones taken by the driver?}

\paragraph{Kernel API Misuse.}
The kernel requires that drivers follow the proper protocol for kernel
APIs, and errors can lead to a non-functioning driver or a resource
leak.  The support library state variables provide context for these
tests.  For example, a checker can track the success and failure of
significant driver entry points, such as the \codesm{init\_module} and
PCI \codesm{probe} functions, and ensure that if the driver is
registered on initialization, it is properly unregistered on
shutdown. Test \#1 in Figure~\ref{fig:test_example} shows a use of
these states to ensure that a driver only invokes
\codesm{pci\_register\_driver} once.

%\fixme{Julia: This is not what was just described.}  \fixme{Julia:
%did you find any bugs that could not be found via static analysis
%[using?] the same knowledge, i.e.  reg/unreg functions are
%probe/remove functions?}

\paragraph{Collateral Evolutions.}
\DIFdelbegin \DIFdel{Collateral evolutions occur when a small change to a kernel interface
necessitates changes in many drivers simultaneously.  }\DIFdelend A developer can use \Arch\ to verify that collateral
evolutions~\cite{padioleau:coccinelle:eurosys:2008} are correctly
applied by ensuring that patched drivers do not regress on any
tests. \DIFdelbegin %DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend \DIFaddbegin \DIFadd{In addition, }\DIFaddend \Arch\ can \DIFdelbegin \DIFdel{also }\DIFdelend ensure that the {\em effect} of a patch
is reflected in the driver's execution. For example, recent kernels no
longer require that network drivers update the
\codesm{net\_device->trans\_start} variable in their
\codesm{start\_xmit} functions.  We wrote a checker to verify that
\codesm{trans\_start} is constant across \codesm{start\_xmit} calls.

\paragraph{Memory Leaks.}
The leak checker uses the support library's object tracker to store an
allocation's address and length. We \DIFaddbegin \DIFadd{have }\DIFaddend implemented checkers to
verify allocation and free requests from 19 pairs of functions, and
ensure that an object's allocation and freeing use paired routines.

The API library simplifies adding support for additional allocators
down to adding only a few lines of code.  Test \#2 in
Figure~\ref{fig:test_example} shows the \codesm{generic\_allocator}
call to the library used when checking \codesm{kmalloc}, which records
that \codesm{kmalloc} allocated the returned memory. A corresponding
checker for \codesm{kfree} verifies that \codesm{kmalloc} allocated
the supplied address.

\ignore{
\paragraph{Driver ioctl Requirements}
Another source of driver bugs are driver \codesm{ioctl} functions,
which can cause security vulnerabilities.  For example, the function
\codesm{ec\_dev\_ioctl} in the network protocol driver \codesm{econet}
did not check that the caller of \codesm{ioctl} has sufficient
privileges, resulting in a security advisory~\cite{CVE-2010-3850}. We
wrote a checker to verify that all drivers in a class invoke the
kernel's \codesm{capable} function appropriately.  The checker
executes as a postcondition and verifies that specific \codesm{ioctl}
commands were matched with a call to \codesm{capable} for the
appropriate privilege. Adding a test for another \codesm{ioctl}
command is easy: add the \codesm{ioctl} command identifier and
a corresponding capability to a table.
} %% ignore

\DIFaddbegin \subsection{\DIFadd{Limitations}}
\Arch\ \DIFadd{is neither sound nor complete, although we have not experienced
any false positives. While we have observed no false negatives among
the checkers we wrote, }\Arch\ \DIFadd{cannot check for all kinds of bugs.  Of
11 common security vulnerabilities~}\cite{chen:linux-vuln:apsys:2011}\DIFadd{,
}\Arch\ \DIFadd{cannot detect integer overflows and data races between threads.
In addition, }\Arch\DIFadd{'s aggressive path pruning may terminate a path that
leads to a bug, causing }\Arch\ \DIFadd{to miss it.  Nevertheless, we find the
tool to be a useful addition to the driver development and patching
process.
}


\DIFaddend %\fixme{Julia: seems likely.
%  These would be false negatives.  Matt: evidently we need to be
%  extremely clear when we say ``false negatives among the checks we do
%  support.''  Addressing the kind of false negative Julia is talking
%  about is setting a very high standard as we'd be comparing the bugs
%  we find against essentially all bugs present in the driver, not some
%  subset.  Every static tool seems to have false negatives according
%  to that definition.}  

\section{Evaluation}
\label{section:evaluation}

The purpose of the evaluation is to verify that \Arch\ achieves its
goals: \DIFdelbegin \DIFdel{(i) usefulness, (ii) simplicity, and (iii) efficiency.
}\DIFdelend \DIFaddbegin \DIFadd{is it useful as a bug-finding tool, and can it be it used to
thoroughly execute driver patches?
}\DIFaddend 

\subsection{Methodology}

% Next paragraph:
% 19 + 7 = \howmanydrivers = 26
% 13 + 4 + 5 + 4 = \howmanydrivers = 26

As shown in Figure~\ref{fig:table-drivers}, we tested \Arch\ on
\howmanydrivers\ drivers in 11 classes from several Linux kernels
including 2.6.29 (13 drivers) and 3.1.1 (4 drivers), and FreeBSD 9 (5
drivers).  Four other drivers normally run only on Android-based
phones, and were from other Linux kernel distributions.  Of the
\howmanydrivers\ drivers, we chose 19 as examples of a specific bus,
while the remaining 7 were chosen because we found frequent patches to
the driver and thus expected to find bugs.

%\fixme{Julia: why some from each kernel?  relevance of having the
%  hardware?}

All tests took place on a machine running Ubuntu 10.10 x64 equipped
with a quad-core Intel 2.50GHz Intel Q9300 CPU and 8GB of memory.  All
results are obtained while running \Arch\ in a single-threaded mode,
as \Arch\ does not presently work with \see's multicore support.
\DIFdelbegin \footnote{\DIFdel{This limitation is engineering-related, and
  currently prevents }%DIFDELCMD < \Arch\ %%%
\DIFdel{from exploring multiple paths
  simultaneously.  Because }%DIFDELCMD < \Arch\ %%%
\DIFdel{is often used for exploring a
  particular path deeply, this limitation is comparatively
  unimportant.}}
%DIFAUXCMD
\addtocounter{footnote}{-1}%DIFAUXCMD
\DIFdelend 

To test each driver, we carry out the following operations:

\begin{enumerate}
\item Run \ds\ over the driver and compile the output.
\item Define a virtual hardware device with the desired parameters and
  boot the \Arch\ virtual machine.
\item Load the driver with \codesm{insmod} and wait for initialization
  to complete successfully.  \DIFdelbegin \DIFdel{Completing this step entails executing at
  least one successful path and returning success, though it is likely
  that other failed paths also run and are subsequently discarded.
}%DIFDELCMD < \item %%%
\DIFdel{Execute a workload (optional).  }\DIFdelend We ensure all network drivers attempt to
  transmit and that sound drivers attempt to play a sound.
\item \DIFaddbegin \DIFadd{Execute a workload (optional).
}\item \DIFaddend Unload the driver.
\end{enumerate}

If \Arch\ reports warnings about too many paths, we annotate the
driver code and repeat the operations.  For most drivers, we run \ds\
over \DIFdelbegin \DIFdel{only }\DIFdelend \DIFaddbegin \DIFadd{just }\DIFaddend the driver code. For drivers that have fine-grained
interactions with a library, such as sound drivers and the pluto2
media driver, we run \ds\ over both the library and the driver
code. We \DIFdelbegin \DIFdel{annotated each driver at locations }%DIFDELCMD < \Arch\ %%%
\DIFdel{specified, and
}\DIFdelend tested each Linux driver with 49 checkers for a variety of
common bugs.  For FreeBSD drivers, we only used the operating system's
built-in test functionality.

\setlength{\tabcolsep}{5pt}
\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l|l||r|r|r|r|r}
\hline
% All annotations mentioned in comments are included
{\bf Driver} & {\bf Class} & {\bf Bugs} &{\bf LoC} & {\bf Ann} & {\bf Load} & {\bf Unld.} \\
\hline
\hline
\textit{akm8975}*  & Compass  & 4 &    629  & 0 &  0:22 & 0:08 \\
\textit{mmc31xx}*  & Compass  & 3 &    398  & 0 &  0:10 & 0:04 \\
tle62x0*           & Control  & 2 &    260  & 0 &  0:06 & 0:05 \\
me4000             & Data Ac. & 1 &  5,394  & 2 &  1:17 & 1:04 \\
phantom            & Haptic   & 0 &    436  & 0 &  0:16 & 0:13 \\
lp5523*            & LED Ctl. & 2 &    828  & 0 &  2:26 & 0:19 \\
apds9802*          & Light    & 0 &    256  & 1 &  0:31 & 0:21 \\
8139cp             & Net      & 0 &  1,610  & 1 &  1:51 & 0:37 \\
8139too            & Net      & 2 &  1,904  & 3 &  3:28 & 0:35 \\
be2net             & Net      & 7 &  3,352  & 2 &  4:49 & 1:39 \\
dl2k               & Net      & 1 &  1,985  & 5 &  2:52 & 0:35 \\
e1000              & Net      & 3 & 13,971  & 2 &  4:29 & 2:01 \\
et131x             & Net      & 2 &  8,122  & 7 &  6:14 & 0:47 \\
forcedeth          & Net      & 1 &  5,064  & 2 &  4:28 & 0:51 \\
ks8851*            & Net      & 3 &  1,229  & 0 &  2:05 & 0:13 \\
pcnet32            & Net      & 1 &  2,342  & 1 &  2:34 & 0:27 \\
\textit{smc91x}*   & Net      & 0 &  2,256  & 0 & 10:41 & 0:22 \\
pluto2             & Media    & 2 &   \DIFdelbeginFL \DIFdelFL{591  }\DIFdelendFL \DIFaddbeginFL \DIFaddFL{*591  }\DIFaddendFL & 3 &  1:45 & 1:01 \\
%DIF <  591 used to have asterisk
econet             & Proto.   & 2 &    818  & 0 &  0:11 & 0:11 \\
ens1371            & Sound    & 0 & \DIFdelbeginFL \DIFdelFL{2}\DIFdelendFL \DIFaddbeginFL \DIFaddFL{*2}\DIFaddendFL ,112  & 5 & 27:07 & 4:48 \\
%DIF <  2,112 used to have asterisk
\textit{a1026}*    & Voice    & 1 &  1,116  & 1 &  0:34 & 0:03 \\
\hline
ed                 & Net      & 0 &  5,014  & 0 &  0:49 & 0:13 \\
re                 & Net      & 0 &  3,440  & 3 & 16:11 & 0:21 \\
rl                 & Net      & 0 &  2,152  & 1 &  2:00 & 0:08 \\
es137x             & Sound    & 1 &  1,688  & 2 & 57:30 & 0:09 \\
maestro            & Sound    & 1 &  1,789  & 2 & 17:51 & 0:27 \\

% Ensure bugs column totals \howmanybugs

\end{tabular}
\DIFdelbeginFL %DIFDELCMD < \vspace{-0.1in}
%DIFDELCMD < %%%
\DIFdelendFL \caption{\small \bf Drivers tested.  Those in \textit{italics} run
  on Android-based phones, those followed by an asterisk are for
  embedded systems and do not use the PCI bus. Drivers above the line
  are for Linux and below the line are for FreeBSD.  Line counts come
  from  CLOC~\cite{clocutility}.  Times are in minute:second format, and are
  an average of three runs.}
\label{fig:table-drivers}
\DIFdelbeginFL %DIFDELCMD < \vspace{-0.1in}
%DIFDELCMD < %%%
\DIFdelendFL %DIF > \vspace{-0.2in}
\end{table}

\subsection{Bug Finding}


\begin{table}[t!]
\footnotesize
\centering
\begin{tabular}{l||r|r||r|r|r}
\hline
               &            & {\bf Kernel /} & {\bf Cross}  &             &            \\
{\bf Bug Type} & {\bf Bugs} & {\bf Checker}  & {\bf EntPt} & {\bf Paths} & {\bf Ptrs} \\
\hline
\hline
Hardware Dep.     &  7 &  6 /  1 &  4 &  6 &  6 \\
API Misuse        & 15 &  7 /  8 &  6 &  5 &  1 \\
Race              &  3 &  3 /  0 &  3 &  2 &  3 \\
Alloc. Mismatch   &  3 &  0 /  3 &  3 &  0 &  3 \\
Leak              &  7 &  0 /  7 &  6 &  1 &  7 \\
Driver Interface  &  3 &  0 /  3 &  0 &  2 &  0 \\
Bad pointer       &  1 &  1 /  0 &  0 &  0 &  1 \\
\hline
{\bf Totals}      & 39 & 17 / 22 & 22 & 16 & 21 \\ % \howmanybugs - ensure totals match
\end{tabular}
\DIFdelbeginFL %DIFDELCMD < \vspace{-0.1in}
%DIFDELCMD < %%%
\DIFdelendFL \caption{\small \bf Summary of bugs found. For each category, we
  present the number of bugs found by kernel crash/warning or a checker
  and the number that crossed driver entry points (``Cross EntPt''),
  occurred only on specific paths, or required tracking pointer
  usage.}
\label{fig:table-bug-summary}
\vspace{-0.2in}
\end{table}
\setlength{\tabcolsep}{6pt}

% \howmanybugs
% 17 + 22 = 39 (see table above)

Across the \howmanydrivers\ drivers listed in
Table~\ref{fig:table-drivers}, we found \howmanybugs\ distinct bugs
described in Table~\ref{fig:table-bug-summary}.  Of these bugs, \see\
detected 17 via a kernel warning or crash, and the checkers caught the
remaining 22. Although these bugs do not necessarily result in driver
crashes, they all represent issues that need addressing and are
difficult to find without visibility into driver/kernel interactions.

% \howmanybugs
% 22 / 39 = 56%
% 16 / 39 = 41%
% 21 / 39 = 54%

These results show the value of symbolic execution. Of the
\howmanybugs\ bugs, 56\% took place across driver entry points. For
example, the akm8975 compass driver calls \codesm{request\_irq} before
it is ready to service interrupts.  If a spurious interrupt occurs
immediately after this call, the driver will crash, since the
interrupt handler dereferences a pointer that is not yet
initialized. In addition, 41\% of the bugs occurred on a unique path
through a driver, and 54\% involved pointers and pointer
properties. These capabilities are all difficult to achieve with
static analysis.

%\fixme{Julia: why is [path sensitivity] a problem for static analysis}
%\fixme{Julia: hard to judge based on one example.  Ref. to results?}

\paragraph{Bug Validation.}
Of the \howmanybugs\ bugs found, at least 17 were fixed between the
2.6.29 and 3.1.1 kernels, which indicates they were significant enough
to be addressed. We were unable to establish the current status of 7
others because of significant driver changes.  We have submitted bug
reports for 5 unfixed bugs \DIFdelbegin \DIFdel{in }\DIFdelend \DIFaddbegin \DIFadd{from }\DIFaddend mainline Linux drivers, all of which
have been confirmed as genuine by kernel developers.  The remaining
bugs are from drivers outside the main Linux kernel that we have not
yet reported.

\subsection{Developer Effort}

One of the goals of \Arch\ is to minimize the effort to test a
driver. The effort of testing comes from three sources: (i) annotations to
prepare the driver for testing, (ii) testing time, and (iii) updating
code as kernel interfaces change.

As an example, we tested the \codesm{phantom} haptic driver from
scratch in 1h:45m, despite having no prior experience with the driver
and not having the hardware.  In this time, we configured the symbolic
hardware, wrote a user-mode test program that passes symbolic data to
the driver's entry points, and executed the driver four times in
different configurations. Of this time, overhead of \Arch\ compared to
testing with a real device was an additional pass during compilation to
run \ds, which takes less than a minute, and 38 minutes to execute.
\DIFdelbegin \DIFdel{Although not a large driver, this test demonstrates }%DIFDELCMD < \Arch%%%
\DIFdel{'s usability
from the developer's perspective.
}\DIFdelend 

\paragraph{Annotations.}
The only per-driver coding \Arch\ requires is annotations on loops
that slow testing and annotations that prioritize specific
paths. Table~\ref{fig:table-drivers} lists the number of annotation
sites for each driver. Of the \howmanydrivers\ drivers, only 6
required more than two annotations, and 9 required no annotations. In
all cases, \Arch\ printed a warning indicating where \DIFdelbegin \DIFdel{an annotation
would
benefit testing}\DIFdelend \DIFaddbegin \DIFadd{testing would
benefit from an annotation}\DIFaddend .

\paragraph{Testing time.}
Symbolic execution can be much slower than normal execution. Hence, we
expect it to be used near the end of development, before submitting a
patch, or on periodic scans through driver code.  We report the time
to load and initialize a driver in Table~\ref{fig:table-drivers}.  The
table also reports the time to unload the driver, which is necessary
to detect resource leaks. Initialization time is the minimum time for
testing, and thus presents a lower bound.

Overall, the time to initialize a driver is roughly proportional to
the size of the driver.  Most drivers initialize in 5 minutes or less,
although the ens1371 sound driver required 27 minutes, and the
corresponding FreeBSD es137x driver required 58 minutes.  These two
results stem from the large amount of device interaction these drivers
perform during initialization.  Excluding these results, execution is
fast enough to be performed for every patch, and with a cluster could
be performed on every driver affected by a collateral
evolution~\cite{padioleau:coccinelle:eurosys:2008}.


%\fixme{Julia: If a
%  maintainer receives 10 patches per day, then he may have to wait 5
%  hours?  If he did static analysis on the code affected by the
%  changes, would it take 5h to analyze the results?  (Admittedly this
%  is a worst case)}.

\paragraph{Kernel evolution.}
Near the end of development, we upgraded \Arch\ to support Linux 3.1.1
instead of 2.6.29. If much of the code in \Arch\ was specific to the
kernel interface, porting \Arch\ would be a large effort. However,
\Arch's use of static analysis and code generation minimized the
effort to maintain tests as the kernel evolves: the only changes
needed were to update a few checkers because their corresponding
kernel functions had changed. The remainder of the system, including
\ds\ and the \tf, were unchanged.
\DIFdelbegin \DIFdel{The number of lines of code changed
was less than 100.
}\DIFdelend 

Furthermore, porting \Arch\ to a new operating system is not
difficult.  We also ported the \Arch\ infrastructure, checkers
excluded, to FreeBSD 9.  The entire process took three person-weeks.
The FreeBSD implementation largely shares the same code base as the
Linux version, with just a few OS-specific sections.  This result
confirms that the techniques \Arch\ uses are compatible across
operating systems.


\subsection{Coverage}

% Basic block coverage
%8139too      & 80\% &
%a1026        & 76\% &
%apds9802     & 85\% &
%econet       & 36\% &
%ens1371      & 56\% &
%lp5523       & out of date &
%me4000       & 61\% &
%mmc31xx      & 83\% &
%phantom      & 81\% &
%pluto2       & 76\% &
%tle62x0      & out of date &

\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l||rr|rr}
\hline
                &  { \bf Touched} &                 & \multicolumn{2}{|c}{\bf Time} \\
{\bf Driver}    &  { \bf Funcs. } & {\bf Coverage}  & { \bf CPU } & { \bf Latency } \\
\hline
\hline
8139too         &  93\% & 83\% &   2h36m &   1h00m \\
a1026           &  95\% & 80\% &     15m &     13m \\
apds9802        &  85\% & 90\% &     14m &      7m \\
econet          &  51\% & 61\% &     42m &     26m \\
ens1371         &  74\% & 60\% &  *8h23m &  *2h16m \\
lp5523          &  95\% & 83\% &     21m &      5m \\
me4000          &  82\% & 68\% & *26h57m & *10h25m \\
mmc31xx         & 100\% & 83\% &     14m &     26m \\
phantom         &  86\% & 84\% &     38m &     32m \\
pluto2          &  78\% & 90\% &     19m &      6m \\
tle62x0         & 100\% & 85\% &     16m &     12m \\
\hline
es137x          &  97\% & 70\% &   1h22m &     58m \\
rl              &  84\% & 71\% &     13m &     10m \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Code coverage.}
\label{fig:table-drivers-coverage}
\vspace{-0.2in}
\end{table}

While \Arch\ primarily uses symbolic execution to simulate the device,
a second benefit is higher code coverage than standard
testing. Table~\ref{fig:table-drivers-coverage} shows coverage results
for one driver of each class, and gives the fraction of functions
executed (``Touched Funcs.'') and the fraction of basic blocks {\em
  within} those functions (``Coverage'').\footnote{* Drivers with an
  asterisk ran unattended, and their total execution time is not
  representative of the minimum.} In addition, the table gives the
total CPU time to run the tests on a single machine (CPU) and the
latency of the longest run if multiple machines are used (Latency). In
all cases, we ran drivers multiple times and merged the coverage
results. We terminated each run once it reached a steady state and
stopped testing the driver once coverage did not meaningfully improve
between runs.

Overall, \Arch\ executed a large majority (80\%) of driver functions
in most drivers, and had high coverage (80\% of basic blocks) in those
functions. These results are below 100\% for two reasons. First, we
could not invoke all entry points in some drivers. For example, econet
requires \DIFdelbegin \DIFdel{user-mode software to trigger additional driver entry points
that }%DIFDELCMD < \Arch\ %%%
\DIFdel{is unable to call on its own.  In other cases, we simply
did not spend enough time understanding how to invoke all of a
driver's code, as some functionality requires the driver to be in a
specific state that is difficult to realize, even with symbolic
execution}\DIFdelend \DIFaddbegin \DIFadd{additional software that we did not have, and other drivers
required kernel-mode tests for entry points not accessible via system
calls}\DIFaddend . Second, of the functions \Arch\ did execute, additional inputs
or symbolic data from the kernel \DIFdelbegin \DIFdel{were }\DIFdelend \DIFaddbegin \DIFadd{was }\DIFaddend needed to test all
paths. Following \see's relaxed consistency model, making more of the
kernel API symbolic could help improve coverage.

As a comparison, we tested the 8139too driver on a real network card
using \codesm{gcov} to measure coverage with the same set of tests.
We loaded and unloaded the driver, and ensured that transmit, receive,
and all ethtool functions executed.  Overall, these tests executed
77\% of driver functions, and covered 75\% of the lines in the
functions that were touched, as compared to 93\% of functions and 83\%
of code for \Arch.  Although not directly comparable to the other
coverage results \DIFaddbegin \DIFadd{in this section }\DIFaddend due to differing methodologies, this
\DIFdelbegin \DIFdel{result }\DIFdelend \DIFaddbegin \DIFadd{results }\DIFaddend shows that \Arch\ can provide coverage similar to \DIFaddbegin \DIFadd{or better
than that of }\DIFaddend running the driver on real hardware.

\subsection{Patch Testing}
The second major use of \Arch\ is to verify driver patches, similar to
a code reviewer. For this use, we seek high coverage in every function
modified by the patch in addition to the testing described
previously. We applied all the patches \DIFdelbegin \DIFdel{between }\DIFdelend \DIFaddbegin \DIFadd{since }\DIFaddend the 11/11/2011 3.1.1
\DIFdelbegin \DIFdel{and the 5/6/2012 3.4-rc6 kernel releases }\DIFdelend \DIFaddbegin \DIFadd{kernel release }\DIFaddend that applied to the 8139too, ks8851 and lp5523
drivers, of which there were 4, 2, and 6, respectively.  The other
drivers either lacked recent patches, included only trivial patches,
or required upgrading the kernel, so we do not consider them further.

In order to test the functions affected by a patch, we used
favor-success scheduling to fast-forward execution to a patched
function and then enabled high coverage mode.  The results in
Table~\ref{fig:table-patch-coverage} demonstrate that \Arch\ is able
to quickly test patches as they are applied to the kernel, by allowing
developers to test nearly all the code in a driver patch without any
device hardware. For all three drivers, \Arch\ was able to execute
100\% of the functions touched by all 12 patches and an average of
98\% of the code in each function touched by the patch. In addition,
tests took an average of only 12 minutes of CPU time to complete.

% 6m = (total run time / number of runs).  This number is less than
% parallel time since there were six runs in all.
% 98\% = (touched basic blocks in functions of interest) /
%        (bb's in functions of interest)

\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l||rr|rr}
\hline
                &  { \bf Touched} &                 & \multicolumn{2}{|c}{\bf Time} \\
{\bf Driver}    &  { \bf Funcs. } & {\bf Coverage}  & { \bf Serial } & { \bf Parallel } \\
\hline
\hline
8139too         &  100\% &  96\% &      \DIFdelbeginFL \DIFdelFL{9m }%DIFDELCMD < &      %%%
\DIFdelendFL 5m \DIFaddbeginFL &      \DIFaddFL{9m }\DIFaddendFL \\
ks8851          &  100\% & 100\% &     16m &      8m \\
lp5523          &  100\% &  97\% &     12m &     12m \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Patched code coverage.}
\label{fig:table-patch-coverage}
\vspace{-0.2in}
\end{table}

% We have been unable to author patches for all of the bugs as the
% solutions in some cases appear to be complex, and some of the bugs
% are from out-of-tree drivers without a clear patch submission
% process.  In the case of one bug, developers confirmed it as
% genuine, but were unable to suggest a proper patch.

\paragraph{Execution tracing.}
Execution tracing provides an alternate means to verify patches by
comparing the behavior of a driver before and after applying the
patch. We use tracing to verify that \Arch\ can distinguish between
patches that change the driver/device interactions and those that do
not, such as a collateral evolution.  We test five patches to the
8139too network driver that refactor the code, add a feature, or
change the driver's interaction with the hardware.  We execute the
original and patched drivers and record the hardware
interactions.  Comparing the traces of the before and after-patch
drivers, differing I/O operations clearly identify the patches that
added a feature or changed driver/device interactions, including which
functions changed. As expected, there were no differences in the
refactoring patches.

We also apply tracing to compare the behavior of drivers for the same
device across operating systems. Traces of the Linux 8139too driver
and the FreeBSD rl driver show differences in how these devices
interact with the same hardware that could lead to incorrect behavior.
In one case, the Linux \codesm{8139too} driver incorrectly treats one
register as 4 bytes instead of 1 byte, while in the other, the \codesm{rl}
FreeBSD driver uses incorrect register offsets for a particular
supported chipset.  Developers fixed the Linux bug independently after
we discovered it, and we validated the FreeBSD bug with a FreeBSD
kernel developer.  We do not include these bugs in the
previous results as they were not identified automatically by \Arch.

These bugs demonstrate a new capability to find hardware-specific bugs
by comparing independent driver implementations. While we manually
compared the traces, it may be possible to automate this
process.

\subsection{Comparison to other tools.}
We compare \Arch\ against other driver testing/bug-finding tools to
demonstrate its usefulness, simplicity, and efficiency.

\paragraph{\see.}
In order to demonstrate the value of \Arch's additions to \see, we
executed the 8139too driver with only annotations to the driver source
guiding path exploration but without the \tf\ or \ds\ to prioritize
relevant paths.  In this configuration, \see\ executes using
\textit{strict consistency}, wherein the only source of symbolic data
is the hardware, and \DIFdelbegin \DIFdel{maximizes }\DIFdelend \DIFaddbegin \DIFadd{it attempts to maximize }\DIFaddend coverage with the
MaxTbSearcher plugin.  \DIFdelbegin \DIFdel{This mode is the default when a developer does not write API-specific
plugins; results improve greatly when these plugins are
available~}%DIFDELCMD < \cite{ckc12}%%%
\DIFdel{.  We ran }%DIFDELCMD < \see\ %%%
\DIFdelend \DIFaddbegin \DIFadd{We ran it }\DIFaddend until it started thrashing the page
file\DIFaddbegin \DIFadd{, }\DIFaddend with a commensurate drop in CPU utilization, for \DIFaddbegin \DIFadd{a total of }\DIFaddend 23
minutes.

During this test, only 33\% of the total functions in the driver
executed at all, with an average coverage of 69\%.  In comparison,
\Arch\ executed 93\% of functions with an average coverage of 83\% in
2\textonehalf\ hours. With \see\ alone, the driver did not complete
initialization successfully and did not attempt to transmit packets.
In addition, \see's annotations could not be made on the driver
source, but must be made on the binary instead. Thus, annotations must
be regenerated every time a driver is compiled.

\DIFdelbegin \DIFdel{Adding more RAM and running the driver longer would likely have
allowed the driver to finish executing the initialization routine.
However, many uninteresting paths would remain, as }%DIFDELCMD < \see\ %%%
\DIFdel{has no
automatic way to prune them.  Thus, the developer would still have
considerable difficulty invoking other driver entry points, since
}%DIFDELCMD < \see\ %%%
\DIFdel{would continue executing failing execution paths.
}%DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend In order for \see\ to achieve higher coverage in this driver, we would
need a plugin to implement a relaxed consistency model.  However, the
8139too driver (v3.1.1) calls 73 distinct kernel functions, and many
of these would require corresponding functions in the plugin.


%DIF < Running
%DIF < \see\ without API-aware plugins is analogous to running \Arch\ with
%DIF < FreeBSD, since \Arch\ has no API-specific knowledge of FreeBSD's
%DIF < operation aside from the short list of kernel functions which return
%DIF < non-standard error values.
\DIFdelbegin %DIFDELCMD < 

%DIFDELCMD < %%%
\DIFdelend % Maybe in related work or separate ``limitations of static tools''
% section
\paragraph{Static-analysis tools.} Static analysis tools are able to
find many driver bugs, but require a large effort to implement a model
of operating system behavior. For example, Microsoft's Static Driver
Verifier (SDV) requires 39,170 lines of C code to implement an operating
system model~\cite{microsoft10}.  \Arch\ instead relies on models only
for I/O bus implementations, which together account for 715 lines of
code for 5 buses.  \Arch\ also supports FreeBSD with 491 lines
of OS-specific code, related primarily to the \tf, which still
provides the benefit of checking drivers against the debugging
facilities already included in the OS.  In addition, SDV achieves much
of its speed through simplifying its analysis, and consequently its
checkers are unable to represent arbitrary state. Thus, it is
difficult to check more complex properties such as whether a variable
has matched allocation/free calls across different entry points.

\paragraph{Kernel debug support.} Most kernels provide debugging to
aid kernel developers, such as tools to detect deadlock, track memory
leaks, or uncover memory corruption. Some of the \tf\ checkers are
similar to debug functionality built into Linux.  Compared to the
Linux leak checker, kmemleak, the \tf\ allows testing a single driver
for leaks, which can be drowned out when looking at a list of leaks
across the entire kernel. Furthermore, writing checkers for \Arch\ is
much simpler: the Linux 3.1.1 kmemleak module is 1,113 lines, while,
the \tf\ object tracker, including a complete hash table
implementation, is only 722 lines yet provides more precise results.

\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~\DIFdelbegin %DIFDELCMD < \cite{ckc11, ckc12, kcc10}%%%
\DIFdelend \DIFaddbegin \cite{ckc11, kcc10}\DIFaddend .  \Arch\ is built upon \see\ but
significantly extends its capabilities in \DIFdelbegin \DIFdel{three }\DIFdelend \DIFaddbegin \DIFadd{four }\DIFaddend ways by leveraging the
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\DIFdelbegin \DIFdel{, though
}%DIFDELCMD < \see\ %%%
\DIFdel{and }%DIFDELCMD < \Arch\ %%%
\DIFdel{both support re-using existing testing tools}\DIFdelend . 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}, which is similar to
\Arch's path pruning and prioritization.

Other systems combine static analysis with symbolic
execution~\DIFdelbegin %DIFDELCMD < \cite{cfb06, cbz11, ecch00, pyr11}%%%
\DIFdelend \DIFaddbegin \cite{cbz11, cfb06, ecch00, pyr11}\DIFaddend .  However, \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~\DIFdelbegin %DIFDELCMD < \cite{bbc+06,Ball:2011:DSM:1965724.1965743,br02,microsoft10,padioleau:coccinelle:eurosys:2008}
%DIFDELCMD < %%%
\DIFdelend \DIFaddbegin \cite{bbc+06,br02,padioleau:coccinelle:eurosys:2008,microsoft10,
  Ball:2011:DSM:1965724.1965743} \DIFaddend 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, to facilitate 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)~\DIFdelbegin %DIFDELCMD < \cite{windows-device-testing, microsoft05b} %%%
\DIFdelend \DIFaddbegin \cite{microsoft05b,windows-device-testing} \DIFaddend 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 (also used by
DDT), or in the case of LTP, as a test program.

\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 \DIFdelbegin \DIFdel{. argue }\DIFdelend \DIFaddbegin \DIFadd{argues }\DIFaddend 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.

\section{Conclusions}
\label{section:conclusions}
\Arch\ uses symbolic execution combined with a \tf\ and static
analysis to test Linux and FreeBSD driver code without access to the corresponding
device.  Our results show that \Arch\ can find bugs in mature driver
code of a variety of types, and allow developers to test driver
patches deeply.  Hopefully,
\Arch\ will enable more developers to patch driver code by lowering
the barriers to testing. In the future, we plan to implement an
automated testing service for driver patches that supplements manual
code reviews\DIFdelbegin \DIFdel{, and investigate applying
}%DIFDELCMD < \Arch%%%
\DIFdel{'s techniques to other kernel subsystems}\DIFdelend .

%\fixme{Julia:  still seems not completely trivial to
%  use.  Prhpas better to target maintainers for whom the work is quickly amortized}
\DIFdelbegin \section*{\DIFdel{Acknowledgments}}
%DIFAUXCMD
\DIFdel{This work is supported by the National Science Foundation grants
CNS-0745517 and CNS-0915363 and by a gift from Google. We would like
to thank the many reviewers who provided detailed feedback on our
work, and for early feedback from Gilles Muller and Julia Lawall. We
would also like to thank the }%DIFDELCMD < \see\ %%%
\DIFdel{developers, who provided us a great
platform to build on. Swift has a significant financial interest in
Microsoft.
}\DIFdelend 



%------------------------------------------------------------------------------
%                                  References.
%------------------------------------------------------------------------------
{\footnotesize
\bibliographystyle{abbrvurl3}
\bibliography{references,my-big,test}
} % small
\end{document}
