In this tutorial, we explain how to symbolically execute the AMD PCnet driver in S2E. We discuss the preparation of the RAW image in vanilla QEMU, how to write an S2E configuration file for this purpose, how to launch symbolic execution, and finally how to interpret the results.
Contents
We want to analyze a PCI device driver, and for this we need an automated way of loading it, exercising its entry points, then unloading it when we are done. This can be done manually via the Windows device manager, but can be automated via the devcon.exe utility. You can find this utility on the Internet. devcon.exe is a command line program that allows enumerating device drivers, loading, and unloading them.
First, boot the vanilla QEMU with the following arguments:
$./i386-softmmu/qemu -fake-pci-name pcnetf -fake-pci-vendor-id 0x1022 -fake-pci-device-id 0x2000 \
-fake-pci-class-code 2 -fake-pci-revision-id 0x7 -fake-pci-resource-io 0x20 -fake-pci-resource-mem 0x20 \
-rtc clock=vm -net user -net nic,model=ne2k_pci -monitor telnet:localhost:4444,server,nowait \
-hda /home/s2e/vm/windows_pcntpci5.sys.raw -s
Here is an explanation of the command line.
Copy the devcon.exe utility in the Windows image. Then, copy the following script into c:\s2e\pcnet.bat (or to any location you wish) in the guest OS. You may beed to setup and ftp server on your host machine to do the file transfer. The NE2K card we set up previously should have an address obtained by DHCP. The gateway should be 10.0.2.2. Refer to the QEMU documentation for more details.
devcon enable @"*VEN_1022&DEV_2000*"
arp -s 192.168.111.1 00-aa-00-62-c6-09
ping -n 4 -l 999 192.168.111.1
devcon disable @"*VEN_1022&DEV_2000*"
Launch this script to check whether everything is fine. devcon enable and devcon disable should not produce errors. Of course, ping will fail because the NIC is fake.
The PCnet driver has a wealth of configuration settings. In this section, we will assign bogus values to them. Note that it is important to explicitly set all settings to something, otherwise Windows will fail the NdisReadConfiguration call in the driver. The NDIS plugin relies on a successful return of that API call to overwrite the settings with symbolic values. If the call fails, no symbolic values will be injected, and some paths may be disabled.
The registry key containing the settings is the following:
HKEY_LOCAL_MACHINE\SYSTEM\CurrentControlSet\Control\Class\{4d36e972-e325-11ce-bfc1-02002be10318}\xxxx
where xxxx is an integer that can vary from system to system. Select the key that has a value containing “AMD PCNET Family PCI Ethernet Adapter”.
The following table lists all the settings that must be set/added.
| Name | Type | Value |
|---|---|---|
| BUS_TO_SCAN | REG_SZ | ALL |
| BusNumber | REG_SZ | 0 |
| BUSTIMER | REG_SZ | 0 |
| BusType | REG_SZ | 5 |
| EXTPHY | REG_SZ | 0 |
| FDUP | REG_SZ | 0 |
| LED0 | REG_SZ | 10000 |
| LED1 | REG_SZ | 10000 |
| LED2 | REG_SZ | 10000 |
| LED3 | REG_SZ | 10000 |
| MPMODE | REG_SZ | 0 |
| NetworkAddress | REG_SZ | 001122334455 |
| Priority8021p | REG_SZ | 0 |
| SlotNumber | REG_SZ | 0 |
| TcpIpOffload | REG_SZ | 0 |
| TP | REG_SZ | 1 |
Once you have set registry settings, make sure the adapter is disabled, then shutdown the guest OS.
Save a copy of the RAW image
Convert the *RAW* image to *S2E* by renaming (or makeing a symlink) the image file.
cp /home/s2e/vm/windows_pcntpci5.sys.raw /home/s2e/vm/windows_pcntpci5.sys.raw.s2e
In this step, we will show how to save a snapshot of the guest OS right before it invokes the very first instruction of the driver. We will use the remote target feature of GDB to connect to the guest OS, set a breakpoint in the kernel, and save a snapshot when a breakpoint is hit.
Boot the image using the previous command line.
$./i386-softmmu/qemu -fake-pci-name pcnetf -fake-pci-vendor-id 0x1022 -fake-pci-device-id 0x2000 \\
-fake-pci-class-code 2 -fake-pci-revision-id 0x7 -fake-pci-resource-io 0x20 -fake-pci-resource-mem 0x20 \\
-rtc clock=vm -net user -net nic,model=ne2k_pci -monitor telnet:localhost:4444,server,nowait \\
-hda /home/s2e/vm/windows_pcntpci5.sys.raw.s2e -s
Once the image is booted, open the command prompt, go to c:\s2e and type pcnet.bat, without hitting enter yet.
On the host OS, open a terminal, launch telnet, and save a first snapshot.
$ telnet localhost 4444
Trying 127.0.0.1...
Connected to localhost.
Escape character is '^]'.
QEMU 0.12.2 monitor - type 'help' for more information
(qemu) savevm ready
You can use this snapshot to make quick modifications to the VM, without rebooting the guest
Now, open GDB, attach to the remote QEMU guest, set a breakpoint in the kernel, then resume execution. In this example, we assume that you have installed the checked build of Windows XP SP3 without any update installed. If you have a free build of Windows XP SP3 (as it comes on the distribution CD), use 0x805A399A instead of 0x80b3f5d6. This number if the program counter of the call instruction that invokes the entry point of the driver.
$ gdb
(gdb) target remote localhost:1234
Remote debugging using localhost:1234
0xfc54dd3e in ?? ()
(gdb) b *0x80B3F5D6
Breakpoint 1 at 0x80b3f5d6
(gdb) c
Continuing.
Return to the guest, and hit ENTER to start executing the pcnet.bat script.
When GDB hits the breakpoint, go to the telnet console, and save the new snapshot under the name go.
(qemu) savevm go
Close QEMU with the quit command.
At this point, you have two snapshots: /home/s2e/vm/windows_pcntpci5.sys.raw.s2e.ready and /home/s2e/vm/windows_pcntpci5.sys.raw.s2e.go:
At this point, we have an image ready to be symbolically executed. In this section, we will explain how to write an S2E configuration file that controls the behavior of the symbolic execution process. This file specifies what module to symbolically execute, what parts should be symbolically executed, where to inject symbolic values, and how to kill states.
Before proceeding further, create a file called pcntpci5.sys.lua. S2E uses LUA as an interpreter for configuration files. As such, these files are fully scriptable and can interact with the symbolic execution engine. In this tutorial, we cover the basic steps of creating such a file.
The top level section of the configuration file is s2e. We start by configuring KLEE, using the kleeArgs subsection. Refer to the corresponding section of the documentation for more information about each setting.
s2e = {
kleeArgs = {
"--use-batching-search",
"--use-random-path",
--Optimizations for faster execution
"--state-shared-memory",
"--flush-tbs-on-state-switch=false",
--Concolic mode for hardware is not supported yet
"--use-concolic-execution=false",
"--use-fast-helpers=false"
}
}
S2E provides the core symbolic execution engine. All the analysis is done by various plugins. In this step, we will select the plugins required for analyzing Windows device drivers. Paste the following snippet right after the previous one. In the following parts of the tutorial, we briefly present each of the plugins.
plugins = {
"WindowsMonitor",
"ModuleExecutionDetector",
"FunctionMonitor",
"SymbolicHardware",
"EdgeKiller",
"ExecutionTracer",
"ModuleTracer",
"TranslationBlockTracer",
"WindowsDriverExerciser",
"ConsistencyModels",
"NtoskrnlHandlers",
"NdisHandlers",
"BlueScreenInterceptor",
"WindowsCrashDumpGenerator",
}
The WindowsMonitor plugins monitors Windows events and catches module loads and unloads. The ModuleExecutionDetector plugin listens to events exported by WindowsMonitor and reacts when it detects specific modules.
Configure WindowsMonitor as follows:
pluginsConfig = {}
pluginsConfig.WindowsMonitor = {
version="XPSP3",
userMode=true,
kernelMode=true,
checked=false,
monitorModuleLoad=true,
monitorModuleUnload=true,
monitorProcessUnload=true
}
This configuration assumes that you run the free build version of Windows XP Service Pack 3.
Now, configure ModuleExecutionDetector as follows to track loads and unloads of pcntpci5.sys.
pluginsConfig.ModuleExecutionDetector = {
pcntpci5_sys_1 = {
moduleName = "pcntpci5.sys",
kernelMode = true,
},
}
The annotation for NDIS drivers implement the over-approximate, local, strict, and over-constrained models. In this tutorial, we show how to set the strict model, in which the only symbolic input comes from the hardware. Feel free to experiment with other models.
The configuration section looks as follows:
pluginsConfig.ConsistencyModels = {
model="strict"
}
pluginsConfig.WindowsDriverExerciser = {
moduleIds = {"pcntpci5_sys_1"},
unloadAction = "kill"
}
pluginsConfig.NdisHandlers = {
moduleIds = {"pcntpci5_sys_1"},
hwId = "pcnetf",
}
pluginsConfig.NtoskrnlHandlers = {
-- It is also possible to have a different consistency
-- for specific API functions
functionConsistencies = {
f1 = {"RtlAbsoluteToSelfRelativeSD", "strict"},
f2 = {"RtlSetDaclSecurityDescriptor", "strict"},
f3 = {"RtlCreateSecurityDescriptor", "strict"},
f4 = {"RtlAddAccessAllowedAce", "strict"},
}
}
The SymbolicHardware plugin creates fake PCI (or ISA) devices, which are detected by the OS. All reads from such devices are symbolic and writes are discarded. Symbolic devices can also generate interrupts and handle DMA.
The following configuration is specific to the AMD PCNet NIC device.
pluginsConfig.SymbolicHardware = {
pcntpci5f = {
id="pcnetf",
type="pci",
vid=0x1022,
pid=0x2000,
classCode=2,
revisionId=0x7,
interruptPin=1,
resources={
r0 = { isIo=true, size=0x20, isPrefetchatchable=false},
r1 = { isIo=false, size=0x20, isPrefetchable=false}
}
},
}
Drivers often use polling loops to check the status of registers. Polling loops cause the number of states to explode. The EdgeKiller plugin relies on the user to specify the location of each of these loops and kills the states whenever it detects such loops. Each configuration entry for this plugin takes a pair of addresses specifying an edge in the control flow graph of the binary. The plugin kills the state whenever it detects the execution of such an edge.
For the pcntpci5.sys driver, use the following settings:
pluginsConfig.EdgeKiller = {
pcntpci5_sys_1 = {
l1 = {0x14040, 0x1401d},
l2 = {0x139c2, 0x13993},
l3 = {0x14c84, 0x14c5e}
}
}
Remark: Some of these edges kill the failure path of the configuration parsing section. Make sure that you specified all configuration options in the registry, otherwise execution might terminate with just one path.
S2E comes with a powerful Annotation plugin that allows users to control the behavior of symbolic execution. Each annotation comes in the form of a LUA function taking as parameters the current execution state and the instance of the annotation plugin. Such annotation can be used to inject symbolic values, monitor the execution, trim useless states, etc.
In the following sample, we write an annotation annotation_example that gets called when the instruction at address 0x169c9 is executed. 0x169c9 is relative to the native load base of the driver.
function annotation_example(state, plg)
-- Write custom Lua code here (e.g., to inject symbolic values)
end
pluginsConfig.Annotation =
{
init1 = {
active=true,
module="pcntpci5_sys_1",
address=0x169c9,
instructionAnnotation="annotation_example"
}
}
All output is generated by specialized plugins. S2E does not generate any output by itself, except debugging logs.
In this part of the tutorial, we present three tracing plugins to record module loads/unloads as well as all executed translation blocks. This can be useful, e.g., to generate coverage reports. Analyzing traces is covered in a different tutorial.
These plugins have no configurable options. Hence, they do not require configuration sections.
The StateManager plugins periodically chooses one successful state at random and kills the remaining states. The NdisHandlers plugin uses the StateManager plugin to suspend all paths that successfully returned from the entry points (e.g., a successful initialization). Whenever no more new translation blocks are covered during a timeout interval, the StateManager plugin kills all remaining states but one successful, and lets symbolic execution continue from the remaining state. This copes with the state explosion problem.
pluginsConfig.StateManager = {
timeout=60
}
Note: StateManager is being phased out and replaced by concolic execution. Updates soon. If you would like to use it, e.g., to reproduce the DDT experiments from the TOCS paper, checkout an S2E version from early August 2011.
The BlueScreenInterceptor and WindowsCrashDumpGenerator turn S2E into a basic bug finder. The BSOD detector kills all the states that crashes, while the crash dump generator produces dumps that can be opened and analyzed in WinDbg.
Dump files are as large as the physical memory and take some time to generate, hence the BlueScreenInterceptor plugin options specify whether to generate a crash dump, and the maximum number of such dumps.
pluginsConfig.BlueScreenInterceptor = {
generateCrashDump = false,
maxDumpCount = 2
}
Now that the configuration file is ready, it is time to launch S2E. Notice that we use the S2E-enabled QEMU in the i386-s2e-softmmu folder.
$./i386-s2e-softmmu/qemu -rtc clock=vm -net user -net nic,model=ne2k_pci -hda pcntpci5.sys.raw.s2e -s2e-config-file pcntpci5.sys.lua -loadvm go
This command will create an s2e-out-??? folder, where ??? is the sequence number of the run. s2e-last is a symbolic link that points to the latest run.
The folder contains various files generated by S2E or plugins. Here is a short list: