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

\Arch\ detects driver/kernel interface violations with checkers, which
are functions interposing on control transfer between the driver and
kernel that verify and validate 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.  Since checkers run in the VM alongside the symbolically
executing driver, they can verify runtime properties along each tested
path.

The checkers use a {\em support library} that simplifies their
development by providing much of their functionality. The library
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.

We next describe a few of the 49 checkers we have implemented with
\Arch.

\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 in 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.  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.}
Collateral evolutions occur when a small change to a kernel interface
necessitates changes in many drivers simultaneously.  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.

\Arch\ can also ensure that the desired {\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 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 writing checkers for additional allocators
down to 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

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