==============================================================================
Testing Error Recovery Code in Windows Drivers with Multi-Path Fault Injection
==============================================================================
Drivers often run in kernel mode, which makes them particularly susceptible to
bringing down the entire system should they contain even the slightest bug.
There are many approaches that attempt to solve or mitigate this problem, such as running drivers
in user space, synthesizing correct-by-construction drivers, using formal verification,
writing them in memory-safe languages, testing, etc.
Drivers (and software in general) often contain error recovery code in order to deal with system errors.
For example, a driver could gracefully shut down if a memory allocation API returns a null pointer.
Sometimes, recovering from the error involves complex steps. In the case of a driver,
this may involve rolling back and deallocating all the internal state. This may be non-trivial,
and unusual error scenarios may trigger untested execution paths, resulting in system crashes.
Error recovery code can be tested using fault injection. A fault injection tool typically
intercepts API calls made by a driver, and instead
of calling the original API, may decide to return an error code that the API call would have made
had it encountered, say, a memory shortage. Whether or not to inject a fault is decided by
a fault scenario. A fault scenario may focus on failing memory allocations, thread creation, various
communication APIs, etc. Fault injection can also go beyond failing APIs, e.g., by corrupting memory with bit flips.
There is a large body of literature that investigates most effective fault scenarios depending on the program under test.
In this tutorial, we will focus on testing error recovery code in Windows drivers using
S2E and symbolic execution. A commonly used tool for fault injection in drivers is Microsoft Driver Verifier.
This tools performs fault injection probabilistically and requires rerunning the driver over and over again
in order to eventually cover all APIs. In contrast, S2E systematically tests every API call, allows
custom fault scenarios, and does not require rerunning the tested driver many times in order to reach full coverage.
After completing this tutorial, you will know:
* How to setup an S2E project to test Windows drivers
* How to get line coverage for Windows drivers
* How symbolic execution can be leveraged for quick and efficient fault injection
* How to add new kernel APIs to the fault injection framework
Before starting, **read the entire tutorial first** in order to get a better overview of the various tasks
and how they connect to each other.
.. contents:: Table of Contents
Setting up S2E
==============
For this tutorial, you will need:
* a Linux environment with S2E installed and running
* a Windows 7 guest image
* a Windows environment to build the driver (see `here <../../WindowsEnvSetup.rst>`__ for details on how to set it up)
* up to 110GB of disk space. The Windows 7 image alone will take 25GB and the Windows 10 build VM up to 60 GB.
Please refer to `Creating analysis projects with s2e-env <../../s2e-env.rst>`__ for more details.
Here is a summary of the commands to run:
.. code-block:: console
# Initialize the S2E environment
mkdir -p $(HOME)/s2e
s2e init $HOME/s2e/env
cd $HOME/s2e/env
# Build S2E binaries
s2e build
# Create a Windows 7 VM image to run the driver
# Get the ISO of the required image on MSDN
s2e image_build --iso-dir /path/to/isos windows-7sp1ent-x86_64
Setting up the Windows Environment
==================================
In order to build Windows drivers, you need the following:
1. A Windows environment (can be a VM)
2. `Microsoft Visual Studio `__ 2015 or 2017
3. `Windows Driver Kit `__ (the latest version supported by your Visual Studio version)
Please refer to the Microsoft's documentation on how to set up and build drivers.
You will also need MSYS2 in order to run LCOV for code coverage:
1. Download the MSYS-GIT SDK from `here `__
2. Launch ``C:\git-sdk-32\msys2.exe`` and type the following commands:
.. code-block:: console
# Install the environment
pacman -Syy gcc python2-setuptools
easy_install-2.7 pip virtualenv
# Check out the S2E repository. Guest tools are in the guest directory.
# They contain the s2e.sys guest driver that you will need to use later.
git clone https://github.com/S2E/s2e.git
# LCOV will be used to display code coverage
git clone https://github.com/linux-test-project/lcov
Please refer to the ``guest-tools`` `readme `__
for more details.
Building the Sample Driver
==========================
This tutorial will use the scanner file system filter driver from the Windows Driver Kit samples repository.
You may want to have a look at its source code and readme to see what it does. This is however not required to
complete this tutorial.
In the MSYS environment, run:
.. code-block:: console
git clone https://github.com/Microsoft/Windows-driver-samples.git
Open the ``filesys/miniFilter/scanner/scanner.sln`` solution in Visual Studio and do the following:
1. Change the driver target version to **Windows 7** and platform to **Desktop**.
Failing to do so will result in a kernel crash if the driver is loaded on Windows 7 or earlier.
The following image shows where to find this setting. Make sure to select
**All Configurations** and **All Platforms** first.
.. image:: drvsettings.png
2. Select **Debug** mode and **x64** architecture. A debug build will give better code coverage information.
.. image:: arch.png
3. Build the driver. You should have the following files:
.. code-block:: console
scanner.inf
filter/x64/Debug/scanner.sys
user/x64/Debug/scanuser.exe
Copy these 3 files into your Linux environment where S2E can find them. It is important that the three files be
in the same folder. You can modify the build settings of the Visual Studio project to put them in the same folder.
You can also use a shared folder to avoid copying them to the VM.
Creating an S2E Driver Project
==============================
In your S2E environment folder, run the following command:
.. code-block:: console
s2e new_project /path/to/scanner.inf
A successful run looks as follows:
.. code-block:: console
(venv) user@linux:~/s2e/env$ s2e new_project /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.inf
INFO: [new_project] Detected Windows INF file, attempting to create device driver project...
INFO: [infparser] /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.inf
INFO: [infparser] class: ContentScreener catalog: scanner.cat
INFO: [new_project] Driver files:
INFO: [new_project] /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.sys
INFO: [new_project] /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanuser.exe
WARNING: [new_project] Catalog file /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.cat is missing
INFO: [new_project] No image was specified (-i option). Attempting to guess a suitable image for a x86_64 binary
WARNING: [new_project] Found windows-7sp1ent-x86_64, which looks suitable for this binary. Please use -i if you want to use another image
INFO: [new_project] Creating a symlink to /home/user/s2e/env/install/bin/guest-tools64
INFO: [new_project] Creating a symlink to /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.inf
INFO: [new_project] Creating a symlink to /home/user/s2e/env/images/windows-7sp1ent-x86_64/guestfs
INFO: [new_project] Creating launch script
INFO: [new_project] Creating S2E configuration
INFO: [new_project] Creating S2E bootstrap script
INFO: [new_project] Creating JSON description
This creates a folder ``projects/scanner`` that should contain the following files:
.. code-block:: console
(venv) user@linux:~/s2e/env$ ls -l projects/scanner/
total 48
-rw-rw-r-- 1 user user 5472 Jan 13 22:00 bootstrap.sh
lrwxrwxrwx 1 user user 58 Jan 13 22:00 guestfs -> /home/user/s2e/env/images/windows-7sp1ent-x86_64/guestfs
lrwxrwxrwx 1 user user 46 Jan 13 22:00 guest-tools -> /home/user/s2e/env/install/bin/guest-tools64
-rwxrw-r-- 1 user user 1832 Jan 13 22:00 launch-s2e.sh
-rw-rw-r-- 1 user user 2898 Jan 13 22:00 library.lua
-rw-rw-r-- 1 user user 983 Jan 13 22:00 models.lua
-rw-rw-r-- 1 user user 1659 Jan 13 22:00 project.json
-rw-rw-r-- 1 user user 10050 Jan 13 22:00 s2e-config.lua
lrwxrwxrwx 1 user user 90 Jan 13 22:00 scanner.inf -> /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.inf
lrwxrwxrwx 1 user user 90 Jan 13 22:00 scanner.sys -> /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.sys
lrwxrwxrwx 1 user user 91 Jan 13 22:00 scanuser.exe -> /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanuser.exe
You can find mode information about the content of these files and folders in the documentation. To summarize,
``bootstrap.sh`` contains a script that will run in the S2E VM to fetch the driver files, load, and run them.
``s2e-config.lua`` contains the S2E configuration, and ``launch-s2e.sh`` is the script that you will run next to launch
S2E.
Customizing the Driver Project
==============================
The S2E project configurator makes its best effort to guess the type of binaries you want to analyze and create
the appropriate S2E configuration. In this case, it figures out that you want to test a driver. However, it does not
know how to run the driver. For example, although S2E detected that the driver has the ``scanuser.exe`` binary,
it does not know how to launch it in order to exercise the driver.
This section shows how to customize the ``bootstrap.sh`` script in order to properly load and run drivers.
Locate the following code in ``bootstrap.sh``:
.. code-block:: console
function execute_target {
# Activate fault injection right before loading the driver
./drvctl.exe set_config FaultInjectionActive 1
# Set this to 1 if you would like more aggressive fault injection, to help harden your driver
# against arbitrary API call errors. This may add false positives.
./drvctl.exe set_config FaultInjectionOverapproximate 1
# Ask windows to load the driver
install_driver "$(win_path "$1")"
# TODO: you may need to manually start the driver using sc
# sc start my_driver_service
# TODO: you may want to download additional binaries with s2eget.exe (e.g., a test harness)
# $S2EGET TestHarness.exe
# Give some time for the driver to load.
# You do not need this if your test harness knows when the driver is done loading.
sleep 30
}
Modify it as follows:
.. code-block:: console
function execute_target {
install_driver "$(win_path "$1")"
sc start scanner
# Give some time for the driver to load
sleep 30
}
You may also want to have a look at ``scanuser.exe`` to see how it works and invoke it from the ``bootstrap.sh`` script.
This is however not required for this tutorial.
Running the Driver
==================
Once you are done customizing the project, launch S2E:
.. code-block:: console
(venv) user@linux:~/s2e/env/projects/scanner$ ./launch-s2e.sh
You will see a lot of output in the console. Most of this output is generated by the ``WindowsMonitor`` plugin and shows
various events that occur in the guest, e.g., module loads, process and thread creation, etc. ``WindowsMonitor``
gets this information from the ``s2e.sys`` guest driver, which is part of the ``guest-tools`` repository that you
cloned earlier. We will see later in this tutorial how ``s2e.sys`` works and how you can extend it for your needs.
After about a minute, S2E should terminate. The ``s2e-last`` folder should contain the ``tbcoverage-0.json`` file.
Check that it is not empty, i.e., that it contains at least a few program counters:
.. code-block:: console
{"scanner.sys": [[5368714608, 5368714650, 48], [5368714656, 5368714665, 11], ... }
We will use this file in order to generate line coverage information for the driver. If you do not see any
program counters in the file, something went wrong. In that case, go to the debugging tips section at the end of this
tutorial.
**Note:** ``s2e-last`` is a symbolic link to the folder that contains the data of the latest analysis run. S2E does not
delete previous runs, so that you can reuse their output if needed. Analysis runs are located in ``s2e-out-xxx`` folders.
Getting Code Coverage Reports
=============================
S2E can generate various types of code coverage. In this section, you will learn how to get line coverage information
when source code is available.
- Build the ``guest-tools/windows/s2e.ln`` solution in Visual Studio in release mode and x64 architecture.
This solution is located in the ``guest-tools`` repository that you cloned earlier in this tutorial.
It contains a number of tools to test Windows binaries. If you would like to learn more about it, please refer to
its `readme `__.
- Extract line information from the driver's PDB file using `pdbparser.exe` as follows:
.. code-block:: console
guest-tools/windows/x64/Release/pdbparser.exe -l scanner.sys scanner.pdb > scanner.sys.lines
The ``scanner.sys.lines`` file contains line information in JSON format. Make sure that this file is in the same folder
as all the other driver files.
**Note:** Binaries produced by Microsoft tools contain line information in PDB files. These files have a proprietary
format and are not readable by Linux tools. We need therefore a Windows tool to extract information from them.
- Run ``s2e coverage lcov scanner``. This should produce the ``scanner.sys.info`` file, which contains
LCOV coverage info. You should see something like this:
.. code-block:: console
(venv) user@linux:~/s2e/env$ s2e coverage lcov scanner
INFO: [lcov] Generating translation block coverage information
ERROR: [line_info] Could not read DWARF information from /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.sys: Magic number does not match
INFO: [jsoninfo] Using /mnt/Windows-driver-samples/filesys/miniFilter/scanner/scanner.sys.lines as source of line information
INFO: [lcov] Writing line coverage to /home/user/s2e/env/projects/scanner/s2e-last/scanner.sys.info
INFO: [lcov] Line coverage saved to /home/user/s2e/env/projects/scanner/s2e-last/scanner.sys.info
- If you want to generate LCOV files on windows, proceed as follows. Run the following command in MSYS after
installing LCOV from `this repository `__:
.. code-block:: console
genhtml --ignore-errors source -p "c:/" -p "d:/" -o coverage_report scanner.sys.info
**Note:** it is important to strip all the drive prefixes (`-p` option) so that ``genhtml`` does not attempt
to write HTML files all over the file system. The command also ignores sources files that cannot be opened, e.g.,
those from the standard library, which are typically unavailable.
- You can also generate the LCOV files on Linux using `s2e-env` directly. This however requires that you have
the source code available on the Linux environment and specify a path to it, like this. Please adapt the path to
the driver directory accordingly.
.. code-block:: console
s2e coverage --sympath /mnt/Windows-driver-samples/filesys/miniFilter/scanner lcov --html scanner
You should see a report like this. Note that the LCOV data generated by S2E does not have function information yet,
so function coverage will be empty.
.. image:: cov1.png
Here are the details for the main driver file:
.. image:: cov2.png
Testing Error Recovery Code
===========================
In the coverage report that you generated previously, you can observe that the error recovery code for
``ZwQueryValueKey`` and ``ExAllocatePoolWithTag`` has not been exercised. In this section, you will learn how
to inject errors in these calls in order to check that the error recovery code behaves properly.
First of all, enable fault injection by setting ``FaultInjectionActive`` to ``1`` in ``bootstrap.sh``:
.. code-block:: console
function execute_target {
./drvctl.exe set_config FaultInjectionActive 1
install_driver "$(win_path "$1")"
sc start scanner
# Give some time for the driver to load
sleep 30
}
After you have done so, rerun S2E and re-generate coverage files.
**Tip:** S2E can test multiple fault scenarios in parallel and complete testing quicker. For this, in the ``launch-s2e.sh``
file, set the ``S2E_MAX_PROCESSES`` variable to the number of threads you wish to use and make sure that
``GRAPHICS=-nographics`` variable is set, as S2E does not support graphics output when running in parallel mode.
You will need about 3-3.5GB of RAM per thread, which is about 32GB of memory for 8 threads. The output will be stored in
``s2e-last/xxx/...`` folders, where ``xxx`` is the S2E instance identifier.
You should now see that the error recovery code is exercised:
.. image:: fi_cov1.png
.. image:: fi_cov2.png
Generating Crash Dumps
======================
In this section, we will introduce a bug in the error recovery code and use fault injection in order to find it.
First, insert the following line in the error recovery code at line 404 of ``scanner.c``.
.. code-block:: c
*(PUINT32*)0x123 = 0x1234;
Then, configure S2E so that it produces crash dumps that can be opened with WinDbg.
S2E does not generate them by default because they can be very large, and depending on how many states crash,
fill up the disk very quickly (a crash dump is as large as the guest physical memory when uncompressed).
To enable crash dumps, open ``s2e-config.lua`` and locate the following section:
.. code-block:: lua
pluginsConfig.WindowsCrashMonitor = {
terminateOnCrash = true,
-- Make this true if you want crashes.
-- Note that crashes may be very large (100s of MBs)
generateCrashDump = false,
-- Limit number of crashes we generate
maxCrashDumps = 10,
-- Uncompressed dumps have the same size as guest memory (e.g., 2GB),
-- you almost always want to compress them.
compressDumps = true
}
Set ``generateCrashDump`` to true and rerun the analysis. When the analysis completes, locate the crash dump with the
following command, then copy it to your Windows environment, decompress it, and open it in WinDbg.
.. code-block:: console
(venv) user@linux:~/s2e/env/projects/scanner$ find s2e-last/ -name *dmp*
s2e-last/dump3.dmp.gz
.. image:: windbg.png
Understanding S2E Logs and Test Cases
=====================================
You may have noticed that S2E generated a lot of output in ``debug.txt`` files. In this section, we will explain
the general structure of these logs and focus on the aspects relevant to fault injection.
Using the analysis results of the previous section, grep for BSOD (blue screen of death) in the S2E logs:
.. code-block:: console
(venv) user@linux:~/s2e/env/projects/scanner$ grep -ri bsod s2e-last/*
s2e-last/debug.txt:25 [State 0] BaseInstructions: Message from guest (0xfffff88002f961a0): s2e.sys: S2EBSODHook is at FFFFF880028D46C4
s2e-last/debug.txt:80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95320): s2e.sys: Invoked S2EBSODHook
s2e-last/debug.txt:80 [State 3] BaseInstructions: Message from guest (0xfffff88002f952e0): s2e.sys: S2EBSODHook: crash dump header of size 0x2000
s2e-last/debug.txt:80 [State 3] Terminating state early: BSOD: code=0x7e param1=0xffffffffc0000005 param2=0xfffff88002923316 param3=0xfffff88002f965c8 param4=0xfffff88002f95e20
In this example, we see that execution path 3 (aka state 3) has crashed. To see why, open ``s2e-last/debug.txt``
(replace the file name by the one you get for your run).
.. code-block:: console
80 [State 3] BlueScreenInterceptor: caught blue screen
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95320): s2e.sys: Invoked S2EBSODHook
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: Backtrace (items: 12)
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF880028D6DCF s2e.sys:000000013FAD3DCF
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF880028D4708 s2e.sys:000000013FAD1708
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF800026D5FC4 ntoskrnl.exe:0000000140074FC4
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF80002A48614 ntoskrnl.exe:00000001403E7614
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF80002A03231 ntoskrnl.exe:00000001403A2231
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF80002701C4C ntoskrnl.exe:00000001400A0C4C
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF800027016CD ntoskrnl.exe:00000001400A06CD
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF800027004A5 ntoskrnl.exe:000000014009F4A5
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF80002711431 ntoskrnl.exe:00000001400B0431
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF800026D5542 ntoskrnl.exe:0000000140074542
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF800026D40BA ntoskrnl.exe:00000001400730BA
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f95140): s2e.sys: FFFFF88002923316 scanner.sys:0000000140007316
80 [State 3] BaseInstructions: Message from guest (0xfffff88002f952e0): s2e.sys: S2EBSODHook: crash dump header of size 0x2000
80 [State 3] Terminating state early: BSOD: code=0x7e param1=0xffffffffc0000005 param2=0xfffff88002923316 param3=0xfffff88002f965c8 param4=0xfffff88002f95e20
80 [State 3] TestCaseGenerator: generating test case at address 0xfffff880028d84ed
80 [State 3] TestCaseGenerator:
v0_FaultInjInvokeOrig_FltRegisterFilter__s2e_sys_13fb22717_scanner_sys_14000707e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_0 = {0xff}; (string) "."
v1_FaultInjInvokeOrig_ZwOpenKey__s2e_sys_13fb23e9f_scanner_sys_14000720d_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_1 = {0xff}; (string) "."
v2_FaultInjInvokeOrig_ZwQueryValueKey__s2e_sys_13fb23efa_scanner_sys_14000724e_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_2 = {0xff}; (string) "."
v3_FaultInjInvokeOrig_ExAllocatePoolWithTag__s2e_sys_13fb2195e_scanner_sys_14000727b_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_3 = {0x0}; (string) "."
Each line of the S2E debug log is composed of several fields:
1. The first column is the elapsed time in seconds since S2E started (here 80 seconds)
2. The second column indicates which execution path generated the log, and if applicable, on which S2E instance
(when running S2E in parallel mode).
3. The third column indicates which plugin output the message. In this case, the ``BlueScreenDetector`` plugin
caught the crash, then called ``s2e.sys`` in the guest to display the backtrace. ``s2e.sys`` used a special
x86 instruction to call the S2E plugin ``BaseInstructions`` in order to print the backtrace.
4. Finally, the blue screen interceptor terminated the execution path (*terminated state early* message)
causing the test case generator to output the concrete test case.
The logs above display two important pieces of information: the backtrace of the bug check and the sequence of faults
that led to the error. In this example, the crash occurred in ``scanner.sys`` at address ``0x140007316``.
The sequence of API calls that led to this bug is ``FltRegisterFilter``, ``ZwOpenKey``, ``ZwQueryValueKey``, and ``ExAllocatePoolWithTag``.
S2E injected a fault only on the last invocation. Note that S2E only supports a subset of kernel APIs, the driver
might have called other APIs that do not appear here.
Let us now explain in more detail how S2E encodes test cases:
.. code-block:: console
v0_FaultInjInvokeOrig_FltRegisterFilter__s2e_sys_13fb22717_scanner_sys_14000707e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_0 = {0xff}; (string) "."
v1_FaultInjInvokeOrig_ZwOpenKey__s2e_sys_13fb23e9f_scanner_sys_14000720d_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_1 = {0xff}; (string) "."
v2_FaultInjInvokeOrig_ZwQueryValueKey__s2e_sys_13fb23efa_scanner_sys_14000724e_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_2 = {0xff}; (string) "."
v3_FaultInjInvokeOrig_ExAllocatePoolWithTag__s2e_sys_13fb2195e_scanner_sys_14000727b_14000708e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6_3 = {0x0}; (string) "."
What you see above is a concrete test case of the crash. A concrete test case consists of an assignment of concrete
values to symbolic variables. The variable names are on the left hand side and the concrete values are on the right
hand side, encoded as C arrays of bytes. In this example, each variable is one byte in size. A non-zero value means
that S2E did not inject a fault (i.e., it invoked the original function, hence ``"InvokeOrig" == true``). A value of 0 means
that S2E skipped the function call and returned a fault instead (hence ``"InvokeOrig" == false``).
So where do these symbolic variables come from? In order to understand this, consider the following pseudo-code example.
This represents a typical pattern of intercepting API calls and injecting faults. It is implemented
in the ``s2e.sys`` driver.
.. code-block:: c
VOID S2EHook_ExAllocatePoolWithTag(...) {
STRING VarName = CreateVariableName(...); // FaultInjInvokeOrig_scanner_sys_...
CHAR C = CreateSymbolicValue(VarName);
if (C) {
return ExAllocatePoolWithTag(...);
} else {
return NULL;
}
}
First, the driver asks S2E to create a variable name that encodes useful information
(e.g., the name of the called API and the address of the call site). Second, it asks S2E to create a symbolic value
with that name. When execution reaches the if statement, S2E sees that it depends on a symbolic variable, determines that
both branches are feasible, and splits the execution path in two. In the first path, the original API is called,
and in the second, the API is skipped and replaced by an error code (here a null pointer). S2E implements path splitting by forking the
entire state of the virtual machine. Each forked state is completely independent from the other states and
can run on its own. This forking process is recursive: when ``s2e.sys``
encounters the next API call, it forks again, eventually forming an execution tree of all possible API failures.
When an execution path terminates (i.e., ``bootstrap.sh`` calls ``s2ecmd.exe kill``), S2E invokes a constraint solver
(currently `Z3 `__), in order to compute concrete assignments to symbolic variable.
Let us know look at all the components of a symbolic variable name. They will be very useful to locate the source of
the bug. They have five components:
.. code-block:: console
1. v0
2. FaultInjInvokeOrig
3. FltRegisterFilter
4. s2e_sys_13fb22717_scanner_sys_14000707e_ntoskrnl_exe_140461c37_140462035_14007ea95_140313b8a_1400668e6
5. 0
1. This is the constraint identifier, a number relative to the current state. This allows
to easily figure out the order in which the faults have been injected.
2. The fault injection library identifier. This string indicates that the variable was created by the fault injection
library when deciding whether or not to inject a fault. This is useful to distinguish fault injector variables
from other kinds of variables introduced by other components.
3. The API function that was intercepted by the fault injection system.
4. The callstack at the location of fault. This is in practice the most useful information. When you get a crash,
look at all variables set to 0 (i.e., fault has been injected), and you will immediately know the location of the fault
in your code. The callstack encoding omits the module name for consecutive addresses that belong to the same module.
This helps keep the variable names shorter. In the example above, the callstack is the following:
.. code-block:: console
s2e.sys: 13fb22717
scanner.sys: 14000707e
ntoskrnl.exe: 140461c37
ntoskrnl.sys: 140462035
ntoskrnl.sys: 14007ea95
ntoskrnl.sys: 140313b8a
ntoskrnl.sys: 1400668e6
You may pretty-print the addresses using ``pdbparser.exe`` from the ``guest-tools`` repository. Please refer
to the ``guest-tools`` `readme `__ for more details
about how to use ``pdbparser.exe``.
5. Global variable identifier. This integer suffix ensures that the variable name is globally unique.
Also, note that S2E replaces any special characters in the variable name
by underscores, in order to make sure that the names are valid for the solver.
Customizing Fault Injection
===========================
In the previous sections, you have learnt how to use S2E to test error recovery code. In this section, we will show
how you can extend S2E's fault injection capabilities, e.g., by adding support for new APIs.
This process is very simple:
1. Look at the code coverage and locate API calls that were not exercised
2. For each API call, determine its error codes and pick one for injection (typically ``STATUS_INSUFFICIENT_RESOURCES``
will do).
3. Create and register a hook function that will intercept the original call and inject the fault.
Just copy/paste existing examples in ``guest-tools/windows/driver/src/faultinj``.
4. Rebuild the driver and place it in the ``guest-tools`` folder of your S2E project.
**Note:**
* In general, a concrete error code is sufficient. You may also want to create a symbolic value instead, constrained
to the set of errors that the original API might return.
Debugging Tips
==============
* Make sure that you have the latest ``s2e.sys`` binary. We provide a binary version of this file on GitHub, which should
be fetched by the S2E build system. This file may sometimes be outdated. In case of doubt, rebuild the ``s2e.sln``
solution, then run ``makedist.bat``, and copy the driver files in ``guest-tools/windows/dist`` to the ``guest-tools``
directory of your project.
Refer to this `readme `__ for more information about
how to build ``s2e.sys``.
* If you do not see any output at all and execution terminates in a few seconds, check that ``s2e.sys`` got loaded
properly. If you see output form ``s2e.sys`` but the coverage file is empty, check that the tested driver loaded properly.
The ``serial.txt`` file contains the console output. If ``sc.exe`` fails for whatever reason, you will see why.
If you see something like *This driver has been blocked from loading*, make sure you did not copy the 32-bit build
by mistake (or the 64-bit build if you use a 32-bit guest).
* If the console shows something that looks like a kernel crash and a backtrace of the driver very early on,
check that you changed the target platform to Windows 7. Running a driver compiled for Windows 8 and later will crash
on Windows 7 because that OS does not support stack cookies.
* Enable graphics output in ``launch-s2e.sh``. This way, you will see the guest's GUI and will be able to run
additional Windows tools (e.g., looking at the event viewer). The VM contains the Sysinternals tools in
``c:\sysinternals`` which may help with debugging.
* Coverage information is by default written when an execution path terminates. It may not be written if you terminate S2E by
killing it or closing its window. If the path seems to have run for a long time, open a terminal in the guest
and run ``c:\s2e\s2ecmd.exe kill 0 0``. Alternatively, you can use the ``writeCoveragePeriod`` option of the
``TranslationBlockCoverage`` plugin in order to periodically dump coverage of the currently running state.
* It may happen that the coverage report shows that some error recovery code is not exercised from one run to the next.
S2E does not seem to terminate properly, some ``debug.txt`` logs are truncated. This is most likely due to an
out-of-memory error. Make sure you have enough memory to run S2E, especially if you run in parallel mode.
You may also need to run ``sudo sysctl -w vm.max_map_count=655350`` in order to increase the number of permitted memory
allocations.