% This paragraph addresses some points raised by an ASPLOS reviewer, but I was
% not sure where to include them.  Perhaps in the testing section?
The \tf, therefore, guarantees that a large subset of the driver's
implementation is correct, but is not a complete solution in itself.  To a large
extent, driver correctness is independent from the hardware for which it is
designed, thus necessitating a \tf.  Conversely, a driver that executes
flawlessly with the \tf\ may still interact with the hardware innapproriately,
and thus fail to work.

(from end of testing.tex)

\subsection{Limitations}

Despite the flexibility of \Arch's \sef\ and \tf, testing device
drivers with \Arch\ can still result in false positives and negatives.
False positives stem from incorrect application of symbolic execution.
For example, executing a kernel function using the \textit{symbolic
  only} mode discussed previously results in unconstrained symbolic
data being returned, and this data could force the driver to take a
path that would never occur on a real kernel.  The result would be a
false positive bug report, including an explanation of what the kernel
could return to cause the crash.  This information might still be
helpful to developers if they wish to harden drivers against possible
future kernel revisions, but most driver developers would likely
ignore such false positive reports.

False negatives, in contrast, occur because of limitations of symbolic
execution and the \tf.  After the developer unloads the driver, and
completes a single execution path, \Arch\ only executes other paths
through driver functions until they return to the kernel.  \Arch\
takes this approach to prevent the kernel from entering an
inconsistent state.  Thus, \Arch\ will miss some inter-procedural bugs
that only occur as a result of a sequence of calls into the driver.


\subsubsection{Driver initialization}

\begin{figure}[t!]
%\fvset{fontfamily=courier, fontsize=\footnotesize,xleftmargin=-5mm}
%\LVerbatimInput{code/8139too_dfs.c}
\begin{center}
\includegraphics[keepaspectratio=true,width=3in]{figures/e1000_state_explosion.pdf}
\end{center}
%\vspace{-0.2in}
\caption{\small \bf State space explosion with symbolic
execution. Each if-statement forks a new path of execution since
\codesm{ret\_val} is symbolic.}
\label{fig:symexplosion}
%\vspace{-0.1in}
\end{figure}

Unlike the libraries used in user-mode applications, which generally
have relatively little initialization code, device drivers need to
initialize a great deal of state before the device is operational.
This abundant initialization code identifies the precise chip used by
the device, as a given driver often supports dozens of chips.  Then,
contingent on the chip, the initialization carries out a series of
operations to initialize the device.  As each device has unique
quirks, the initialization code is routinely branch-heavy.
Initializing a sound driver, for example, requires branching roughly
1,000 times depending on hardware-specific details.  This excessive
branching is known as \textit{state explosion}.

State explosion arises when symbolic values used in conditional
statements cause execution to fork repeatedly, once for each path
through the code.  Each path results in a new symbolic execution
state.  Figure~\ref{fig:symexplosion} shows a piece of driver code in
which each conditional forks execution.  Too many states cause
symbolic execution to either take a long time to complete, or to stop
testing some states.  The problem is particularly acute for drivers
that contain many conditional statements for checking device response
status bits and chipset identifiers, especially in initialization
code.  Drivers often support many specific devices, and routinely
contain extensive branching logic to implement this support.

To mitigate this problem, \Arch\ uses an improved path selection
algorithm that prioritizes execution of paths that exit loops.
\Arch\ also favors paths that execute successfully, since developers
are often interested in executing parts of the driver other than
initialization.  \Arch's goal is to force execution down successful
paths, so developers can see how their code behaves while the driver
is operational.  This strategy allows developers to initialize complex
drivers quickly, and be returned to a command prompt with the driver
in a state useful for further testing.  This feature is essential to
testing device drivers more broadly, as it allows developers without
any access to the relevant hardware to initialize a driver and execute
tests of interest.

\begin{figure}[t!]
%\fvset{fontfamily=courier, fontsize=\footnotesize,xleftmargin=-5mm}
%\LVerbatimInput{code/e1000_checksum.c}
\begin{center}
\includegraphics[keepaspectratio=true,width=3in]{figures/e1000_checksum.pdf}
\end{center}
%\vspace{-0.2in}
\caption{\small \bf Symbolic execution is not appropriate for checksum
  calculations, since performance would be poor and the developer would gain
  little insight into the driver's behavior.}
\label{fig:eeprom}
%\vspace{-0.1in}
\end{figure}




The second task is to generate a stub for each kernel function.  Each
stub contains code that analyzes the parameters being passed into the
kernel.  Any function pointers, either passed directly or within a
structure, are passed to the test framework, as well as information on
the containing structure.  This information is necessary for the
\tf\ to map driver functions such as \codesm{e1000\_probe} to
corresponding \tf\ checkers such as
\codesm{pci\_driver\_probe\_check}.  As above, \ds\ pessimistically
assumes that any function pointer passed from the driver into the
kernel could have an associated \tf\ checker, and thus has an
associated call to establish the mapping.

As in the case of the driver function stubs, the stub then conducts a
dynamic lookup to find any associated \tf\ function.  For example, the
\codesm{pci\_register\_driver} function has a \tf\ checker called
\codesm{pci\_register\_driver\_check}.  The stub caches the result of
this lookup, and then invokes the checker, if available.  Next, the
stub invokes the desired kernel function, the post-condition checker,
and includes code to invoke any driver interrupt handlers.

The third task of \ds\ is to provide the \tf\ with a mapping between
driver functions, and their associated pre- and post condition stubs.
This mapping is necessary because it simplifies the process of looking
up \tf\ checkers.


\subsection{\see\ Plugins and Consistency}
\see\ uses plugins within the hypervisor to define different
consistency models.  One of \see's strengths is its support for many
models, such as ``local consistency,'' ``CFG consistency,'' and so
forth.  However, implementing these other models requires many lines
of hypervisor code, and \see\ provides strong support only for ``local
consistency'' with Windows NDIS drivers.  Local consistency entails
replacing concrete values returned from kernel functions with symbolic
values, with the expectation that this replacement will increase code
coverage.  Local consistency produces no false positives, since the
symbolic values it uses are constrained to match the interface
specification, but requires considerable effort to set up in the form
of plugin code for kernel functions.

Implementing local consistency for a single kernel function with an
\see\ plugin requires a developer to specify the range of possible
return values from the function, and fork execution of the current
path for each possible return value.  Local consistency also entails
specifying any out-parameters, and converting their values to symbolic
memory with a full set of constraints as specified in the interface.
These plugins, running inside the hypervisor, do not provide direct
access to kernel variables or data structures.  Thus, they require the
developer to use a variety of utility functions to access parameters,
return values, and the currently executing module state.  However,
these utility functions do not use the names of parameters; instead,
they only operate on stack offsets.  Finally, \see\ plguins
occasionally necessitate manipulation of the stack pointer.  For
example, returning different values in different paths requires this
approach.

%
% Example of reading parameters:
% 521     ok &= readConcreteParameter(state, 1, &plgState->val3); //Length
% 522     ok &= readConcreteParameter(state, 3, &plgState->val1); //VirtualAddress
% 523     ok &= readConcreteParameter(state, 4, &plgState->val2); //PhysicalAddress
%

In contrast, \Arch\ employs a modified version of ``strict
consistency,'' by sacrificing code coverage in favor of simplicity,
while maintaining accuracy.  The primary benefit is that \Arch\ does
not require any driver or kernel annotations except those for complex
loops.  In particular, \Arch\ does not require a specification of the
kernel's behavior, such as the possible return values from a given
function, since this specification is necessary to implement local
consistency.

%% From intro

Making the situation worse, individual drivers routinely support
dozens of distinct pieces of hardware. For example, the Intel E1000
driver in the Linux 2.6.29 kernel supports over 60 distinct
network-processing chips.  Some chips have limitations that the driver
must work around, while others are of newer designs that employ
different I/O protocols from earlier implementations.  Support for
many chips complicates testing: to test a driver thoroughly a
developer may need not just one device, but rather one of each
supported devices.


%% from implementation stubs


Each stub is approximately 20-40 lines long, and has a highly regular
structure.  Stubs for kernel functions that include parameters with
many function pointers can be longer: up to several hundred lines.  A
driver developer never needs to look at this code, and their presence
does not change the driver's behavior.



\begin{table*}[t!]
\small
\begin{tabular}{l|l}
Test Category & Assertion \\
\hline

Memory leak  & The driver frees all allocated SKBs and those passed to the
\codesm{start\_xmit} routine.  \\

Network \codesm{probe} & The \codesm{probe} functions in network drivers 
invoke \codesm{register\_netdev} if they return success.  \\

PCI device state & Calls to \codesm{pci\_enable\_device} (or
\codesm{pci\_enable\_device\_mem}) and \codesm{pci\_disable\_device} 
match. \\

PCI driver state & Calls to \codesm{pci\_register\_driver} and
\codesm{pci\_unregister\_driver} match. \\

Function ordering & PCI network drivers call \codesm{pci\_disable\_device}
after calling \codesm{unregister\_netdev}.  \\

Function ordering & Network drivers finish \codesm{probe} successfully
before the kernel invokes the \codesm{ndo\_open} function. \\

Function ordering & Network driver \codesm{ndo\_open} functions called only
once. \\

Return values & During the network \codesm{ndo\_open} call, the driver only
calls \codesm{netif\_start\_queue} if open is successful. \\

Return values & If the network \codesm{ndo\_open} call is not successful,
the driver calls \codesm{netif\_start\_queue}. \\

Return values & The driver's \codesm{ndo\_stop} function calls
\codesm{netif\_stop\_queue}. \\

Return values & If \codesm{register\_netdev} fails, or if the driver does not
call it, then the \codesm{probe} function returns failure. \\

\end{tabular}
%\vspace{-0.1in}
\caption{\small \bf Sample of \Arch's kernel API checkers.}
\label{fig:table-kernel-api}
%\vspace{-0.2in}
\end{table*}

%% From examples

\paragraph{Memory Leaks}
Memory leaks are a pernicious problem in drivers, and it is
particularly difficult to find small leaks among the sea of other
allocations.  \Arch\ provides an object tracker, implemented as a
simple hash table, that stores memory address, length, object state,
and a description of the object's origin.  With the tracker, a checker
can record object allocation and deallocation, and detect even small
memory leaks.  We have implemented checkers to verify allocation and
free requests from 12 pairs of functions, as well as other special
cases, such as SKBs passed into a network driver's
\codesm{start\_xmit} function that the driver is then responsible for
freeing.

The API library simplifies adding support for additional allocation and
deallocation routines down to adding a one-line call into the API.
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.

\Arch's object tracker provides considerably more flexibility than the
Linux kernel's memory leak detector,
\codesm{kmemleak}~\cite{kmemleak}. The kernel's detector provides a
global view of all memory allocations, which aids in finding repeated
leaks but is less suitable for finding small leaks in a specific
driver.

% Mike - Here's a comment from me about the S2E memory checker.  This
% paragraph could be cut down:

Similarly, \see's own leak detector supports only Windows NDIS
drivers, rather than all kernel memory allocation and deallocation
routines.  The existing implementation also includes eight comments
relating to known issues, and additional logic for keeping memory
allocations from each state independent from each other.  Finally, the
\see\ implementation requires customized code to extract the memory
addresses and sizes from the current state for each allocation
function, whereas the \tf\ implementation can refer to parameters and
return values directly and requires only a call to the
\codesm{generic\_allocator} \tf\ function.  The \Arch\ \tf\ also needs
no additional logic for keeping the objects allocated in each state
independent, since its memory leak checking all runs within the VM.

% More comment:
%
% Seven comments in their memory checker actually say, ``// XXX: ugh,
% this is really ugly!''  However, to their credit, they are checking
% some additional properties that we don't, though we could.  I think
% the larger issue is the code in S2E that adds/removes allocated regions,
% since that requires jumping through hoops to extract the
% address/size of the allocated memory, whereas we just reference the
% parameter/return value directly.
