SymDrive: Testing Drivers Without Devices UW--Madison Logo
Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift
Home | Downloads | Related Work | Results

Setup Introduction

Before attempting to install SymDrive, we recommend reading the paper so you have a better familiarity of how it works and what it's capable of doing. The paper is available here: SymDrive. These instructions are currently written with the assumption that you're interested in testing Linux drivers: if you'd like instructions for setting up the FreeBSD environment, feel free to email me (click Matt's name, above). We don't currently have instructions on using SymDrive with FreeBSD but can post them if the interest is there.

Please follow the instructions on S2E's page first: Building the S2E Platform. Once you can build S2E, it's much easier to compile SymDrive. The following instructions detail what to do once you can compile S2E.

Links to All Downloads

Directory Structure Overview

This guide will assume the following directory structure. Except where noted, the instructions on setting these directories up are available in subsequent sections -- this is just an overview of what things should look like in the end.

  1. ~/s2e: The main location for everything. You should be able to use any account name you want.
  2. ~/s2e/symdrive/cil: SymGen source code and compiled result. cil/obj/x86_LINUX/cilly.asm.exe must exist as this is the SymGen binary.
  3. ~/s2e/symdrive/debian32: The debian32 chroot jail. Set this up as per the S2E instructions above.
  4. ~/s2e/symdrive/gtf: The "generalized" test framework (includes support library + checkers).
  5. ~/s2e/symdrive/qemu: The location from which we launch S2E/SymDrive. This directory should contain a number of scripts:
    • backup_qemu.sh - Don't run this manually.
    • debian32.sh - Run this to enter the chroot environment.
    • qemu.sh - Described later. We use this script to execute S2E/SymDrive more easily.
    • sendkey.py - Don't run this manually.
    • telnet.sh - Don't run this manually.
  6. ~/s2e/symdrive/qemu/i386: The location of the VM disk image in which the driver runs. This disk image will likely be several GBs and should be named s2e_disk_linux.qcow2. You should also keep a backup disk image called s2e_disk_linux.qcow2.backup.
  7. ~/s2e/symdrive/test: The location of the drivers you want to test. This should contain a symlink to gtf as well as the lp5523 directory. lp5523 is a sample driver we discuss here.
  8. ~/s2e/s2e: S2E source code with the SymDrive patch applied. Ideally, keep a separate branch using GIT to track the upstream S2E repository. SymDrive does not have a public GIT repository at this time and is distributed as a patch to S2E.
  9. ~/s2e/build: S2E/SymDrive compiled binaries.

Setting up the Environment and S2E

In our SymDrive setup, we use Ubuntu 11.10 x64, and the instructions here assume you've already managed to compile S2E. Once you can compile S2E, these instructions should work. To be clear about the operating system, we installed from the disk image with the following properties: MD5=62fb5d750c30a27a26d01c5f3d8df459, SHA1=0d64f0532316a0a212c5916d997581e72c52ff02, Name=ubuntu-11.10-desktop-amd64.iso.

SymDrive uses a specific version of S2E. We would like to integrate as much as possible of SymDrive with S2E, but time constraints currently preclude this approach. In addition, SymDrive currently breaks some existing S2E functionality, which we would need to fix before being able to merge it. We hope to fix these problems in the future.

  1. In your home directory, create a subdirectory called s2e using mkdir s2e.
  2. Install git using sudo apt-get install git.
  3. Execute mkdir build to create a directory for the S2E binaries.
  4. Check out S2E using git clone git://github.com/dslab-epfl/s2e.git. Note that this repository used to exist at https://dslabgit.epfl.ch/git/s2e/s2e.git but has since moved.
  5. Once the clone is finished, be sure you've installed all the packages listed on the S2E site as necessary to build S2E. The list is here: Building S2E.
  6. At this point you have the full S2E source code. Next make a branch for SymDrive. From within the ~/s2e/s2e directory, where you've checked out the code, execute: git checkout -b SymDrive b5cfd33051c3be3ab254a5d3e9f4376861188c77. The idea is to get the repository into a state that lets you patch it. This specific commit is known to work with the SymDrive patch, so we create a branch from that commit. Use git branch -a to show all the branches. The current one should be SymDrive.
  7. Verify that the command git log shows commit b5cfd33051c3be3ab254a5d3e9f4376861188c77 as the first line. This step confirms that the repository is in the right state for patching.
  8. Now download the SymDrive patch from here: symdrive.patch and put the file in the S2E base directory.
  9. Run git apply symdrive.patch to apply this patch to the SymDrive branch. If this step fails, then verify your current branch ends with the right commit since the patch may become out-of-date as S2E evolves. You may see some warnings about trailing white space. The patch is not particularly "clean" in that respect but these warnings are harmless.
  10. Compile S2E with the integrated SymDrive patch per the instructions on their site. Note that to improve reliability, it may be worth using make JOBS=1; however, I've always had success with make JOBS=10 if I run it repeatedly. The Makefile seems to have a bug or two, so you may need to run "make" up to ~5 times before it completes successfully. It should not be necessary to change any source code.

Now, if compilation fails, first try running make several times to ensure that the problem isn't a Makefile dependency issue. If make consistently fails, and you're sure you can compile S2E without the SymDrive patch, then contact me.

The chroot jail

The S2E website also includes information of setting up a 32-bit chroot jail. The purpose of this step is to simplify compilation of 32-bit kernel binaries on what is otherwise a 64-bit OS. SymDrive and S2E both work only with 32-bit guest operating systems, so to compile a driver for testing with SymDrive, the jail is necessary.

The steps we use to set up the jail are as follows. Note there are a few minor differences from those on S2E's site. We've copied the documentation they posted here and have changed the necessary steps:

  1. sudo apt-get install debootstrap.
  2. Create the directory with the chroot environment: mkdir ~/s2e/symdrive && mkdir ~/s2e/symdrive/debian32.
  3. Create the basic chroot environment. Pay attention to --arch i386! It is crucial for correct compilation. sudo debootstrap --arch i386 squeeze debian32/ http://mirror.switch.ch/ftp/mirror/debian/.
  4. At this point, you can try our debian32.sh script, which is available here: qemu.tbz. Download this file, and decompress it into ~/s2e/symdrive/qemu. The easiest approach is to decompress the tbz using tar xvjf qemu.tbz. At this point, you should have a debian32.sh script inside ~/s2e/symdrive/qemu, along with some other scripts whose functions we'll describe later.
  5. Execute ./debian32.sh from within the ~/s2e/symdrive/qemu directory. It will complain that some mount points are not available--these errors don't matter at this point.
  6. From within the jail, execute cd root, and then mkdir cil test gtf. The eventual approach we use is to make SymDrive code available inside and outside the jail simultaneously. These directories will serve as mount points for the code.
  7. Install build tools and developer's libraries for ncurses: apt-get install build-essential kernel-package locales libncurses-dev

At this point, your jail should contain several directories: /root, /root/cil, /root/test, and /root/gtf. You can exit the jail by logging out (CTRL-D), at which point the debian32.sh script will attempt to unmount some directories, and then return you to the normal command prompt.

Building the Linux 3.1.1 kernel

We modified the kernel to facilitate debugging. These changes are available as a patch. Currently, the patch includes considerable extra "junk" that kernel developers are not normally interested in, such as the .config file. We include this material to provide a more useful place to begin, since we used this kernel configuration while testing many of the drivers.

The steps are as follows:

  1. While in your chroot jail, create a directory called /root/kernel.
  2. Download the patch here, as well as some other possibly-helpful scripts: kernel_files.tbz. Put it in your /root/kernel directory, and extract it.
  3. Extract linux-3.1.1.tar.bz2 from here: kernel.org. Use tar xvjf linux-3.1.1.tar.bz2 to decompress it, and do this inside the /root/kernel directory.
  4. You should now have a /root/kernel/linux-3.1.1 directory. Make sure the patch is in /root/kernel and execute patch -p1 < ./linux_311.patch from the same directory (/root/kernel).
  5. Assuming that's successful, navigate to /root/kernel/linux-3.1.1. Run chmod +x *.sh to set up a couple of helpful scripts. Run ./1_menuconfig.sh and make sure things look sensible.
  6. Run ./2_make.sh to create the installation package.
  7. At this point you should have some *.deb files in the ~/kernel directory. You can use these files to install a new kernel in the test virtual machine.

At this point, the kernel is usable, and you can compile drivers with it. The one inside the virtual machine image should match the one created by this patch, so there is no need to reinstall the kernel inside the VM unless you want to.

The modifications made to this kernel are chiefly to make it easier to send information to S2E's log. S2E itself includes mechanisms for intercepting function calls; however, we found it easier to make modifications to the kernel itself.

We also have a much smaller version of the patch available that doesn't include extra junk here: linux_311_small.patch. Use this if you'd rather start with your config file and build settings, or would just like to look at what we really changed.

The patch adds a copy of s2e.h to the kernel source. In our copy of the kernel, this file is instead a symbolic link to /root/test/common/s2e.h. The fact that it shows up in the patch "inlined" is simply an artifact of the patch creation process. This point does not matter from a correctness perspective, but it's worth keeping in mind that having multiple copies of s2e.h can easily lead to problems if you're not careful. Feel free to use symbolic links if you wish.

Finally, the patch also adds a new kernel symbol called uprintk. The motivation was to distinguish print statements that should go to the S2E log from those in the kernel. In the end, we found it easiest simply to send all printk messages to S2E, so that's what we ended up doing. The uprintk symbol remains in the kernel patch, but it's not clear that maintaining it is worthwhile.

Setting up SymGen

The steps are as follows:

  1. First, download the code, here: cil.tbz. SymGen is based on CIL (available here: SourceForge, documentation here) and includes a complete copy of that tool.
  2. Decompress SymGen in to ~/s2e/symdrive/cil. Don't decompress it within the jail. To do this, run tar xvjf ./cil.tbz from ~/s2e/symdrive, which will create a directory called cil with the SymGen source code in it.
  3. SymGen is written using CIL, which uses OCaml. The package linked here includes CIL, but you will need to install the OCaml compiler. In your chroot jail, install OCaml using aptitude search ocaml to find the package, and then assuming entries are listed, use apt-get install ocaml. You can test that it works using ocamlc --version.
  4. You also need autoconf: run apt-get install autoconf from inside the jail.
  5. Now, if you've done these steps sequentially, first exit any open jail using CTRL-D. Then re-start the jail by re-running debian32.sh. This time, the cil directory should mount automatically. Change your current directory in the jail to /root/cil and see if the files are listed. If they're not, verify that you decompressed them outside the jail into the directory listed previously, and that the debian32.sh script is mounting the directory properly.
  6. Now that OCaml is installed, try to compile SymGen. First run make configure, then ./configure and then make.
  7. Still in the chroot jail, add /root/cil/bin to your PATH so that you can run SymGen using the cilly command.
  8. Verify SymGen works by typing cilly --help and search for the line --dodrivers Enable device-driver analysis. If this line is not present, then SymGen or CIL is not set up correctly, and you can contact us for feedback.

Setting up Drivers

This section discusses how to set up a new driver to test with SymDrive. The idea is to compile the driver first with SymGen, and then copy it into your S2E-enabled virtual machine so that we can run it with SymDrive. The steps for compiling the driver are as follows:

  1. Download the test framework and support library from here: gtf.tbz. Place it in ~/s2e/symdrive/ and decompress it. gtf means "Generalized Test Framework" which simply refers to the fact that it compiles/runs on both Linux and FreeBSD. It's the same Test Framework as described in the paper, and contains the support library as well as all the checkers. After this step, you should have the directory ~/s2e/symdrive/gtf filled with files from the archive.
  2. Download a sample driver directory hierarchy from here: test.tbz. Place it in ~/s2e/symdrive and decompress it. This file contains a single driver that we've already set up for use with SymDrive, namely the lp5523 Linux driver. This driver controls a chip that operates LEDs on embedded devices. After this step, you should have the directory ~/s2e/symdrive/test. The ~/s2e/symdrive/test/lp5523 directory contains a sample driver from Linux.
  3. Start the chroot jail. You should notice when doing so that all three mount commands complete successfully now.

    Executing mount -o bind /home/public/s2e/symdrive/cil /home/public/s2e/symdrive/debian32/root/cil
    Executing mount -o bind /home/public/s2e/symdrive/test /home/public/s2e/symdrive/debian32/root/test
    Executing mount -o bind /home/public/s2e/symdrive/gtf /home/public/s2e/symdrive/debian32/root/gtf

  4. Change into the /root/test directory and ensure that test_framework is a symbolic link pointing to ../gtf. The reason for this complexity is that gtf supports Linux and FreeBSD whereas the test directory is for Linux only. If you wanted FreeBSD, you could have, e.g. test_freebsd, with corresponding drivers, and then link to the same gtf.
  5. Verify that /root/cil, /root/gtf, and /root/test all contain the files that you extracted outside the chroot environment. If they don't, the directories are not being mounted in the jail properly and you should examine the debian32.sh script.
  6. Run ./make.sh lp5523 from within /root/test. Odds are this will fail for some reason, but if you're lucky and things are set up correctly, then it will succeed. Contact us if it fails and you can't resolve the problem and we can help. The last two lines of output (saved to output.txt) should read:
    • cat lp5523/output.txt | grep undefined
    • make: [lp5523.ko] Error 1 (ignored)
    If you're seeing failures here, examine /root/test/lp5523/output.txt to see if that log sheds any light on it. The last line of this file should be "All done" but if things aren't working it may not be. Search the file for "error" and see if it becomes clear that way. Contact us if it's not working and you can't figure it out.
  7. To ensure things are working, the next thing to check for after compiling is the test framework. Output for the test framework compilation appears in /root/test/output.txt. The test framework is in /root/test/test_framework_lp5523, where lp5523 is the name of whatever driver you're testing. The test_framework_lp5523 directory should contain test_framework_lp5523.ko, which is the actual kernel module.

    SymDrive compiles a special test framework for each driver, since when testing existing kernel drivers, we found it easiest/most reliable to disable the checks that were failing on a per-driver basis. In the real world, this feature makes less sense, because the developer would usually instead fix the bug, or the checker may be faulty and need tweaking.

  8. If things are working, this is what you should see in /root/test/lp5523:
    • output.txt: Compilation output. Use this to diagnose compile-time or SymGen problems.
    • lp5523.merged.c: An automatically-generated CIL intermediate file that should be identical to the original driver in terms of functionality, but is rewritten into a single "merged" file. This file does not contain instrumentation and is included only for debugging.
    • lp5523.sym.c: The main instrumented driver source file. This file contains the automatically-added SymDrive source annotations such as s2e_loop_before. When SymDrive executes, it occasionally prints out line numbers. These line numbers refer to the lines in this file, which can be confusing.
    • lp5523-stub.ko: Most importantly, there should be a kernel object file. This is the instrumented driver that you'll actually load in the S2E virtual machine. If things are working, you must have a *-stub.ko file.

Getting the Disk Image

S2E runs a complete VM symbolically, so to test drivers, you'll need a VM image. This section outlines the necessary steps to getting the disk image we use with Linux 3.1.1.

  1. cd ~/s2e/symdrive/qemu
  2. Download the image from here: i386.tbz into the qemu directory. For reference, the username and password to use are root and rootme, respectively.
  3. From the qemu directory, execute tar xvjf ./i386.tbz. Ensure the file s2e_disk_linux.qcow2 is created afterwards.
  4. cd ~/s2e/symdrive/qemu.
  5. Execute ./qemu.sh 14159265358979323846. This command creates a backup of the s2e_disk_linux.qcow2 file. Check the i386 directory afterward to verify the backup is present.
  6. At this point, you can use qemu.sh 4982 to replace the current image with the one from the backup at any time. The first time you do, it will take a while. However, this command starts a background rsync process that makes a second backup, so in the future, if you need to replace the current image with the backup, there will be a copy available and the operation is immediate. For full details, please examine the file itself qemu.sh. If you have problems with this feature (./qemu.sh 4982 and ./qemu.sh 14159265358979323846), just don't use it. We've found it completely reliable and always use it, but don't blame us if you have problems with it.
  7. We used the long string 14159265358979323846 to avoid accidentally running this command.

Running a Driver

Once everything is compiled, the next step is to run it, and maybe find some bugs. In this section, all steps take place outside the virtual chroot environment and we'll assume you already have the test_framework_drivername.ko and the driver-stub.ko object files.

  1. It's first necessary to copy the object files to the virtual machine. Using the qemu.sh script, run ./qemu.sh 4982 drivernumber 10, where drivernumber is the value set up in the script for the driver. Run qemu.sh to see a list of all options. In this case, the number for lp5523 is 44.
  2. The qemu.sh script is designed to run QEMU from the console. All manual I/O takes place via VNC. If you're running everything with an X-server you may find it easier to disable VNC, in which case you can use the command ./qemu.sh 4982 98 44 10. You can edit the qemu.sh script if you wish to make this change permanent. We use VNC to view the QEMU VM instead, but either approach works. The QEMU process itself runs the VNC server on port 5902, so to connect, you'll want to use X.X.X.X:5902 in your VNC setup, where X.X.X.X is the address of the machine that you ran the "qemu.sh" command on.
  3. Open a new terminal, and use debian32.sh to start the chroot jail. Leave this terminal open for now.
  4. After QEMU boots and you see the login prompt, in a third terminal, execute ./qemu.sh 1000 from the ~/s2e/symdrive/qemu directory. This command should login to the VM automatically and change to the appropriate directory. It should then copy the necessary files into the VM automatically, and save the VM state. After this command finishes the VM will exit automatically. The password is rootme if you're prompted.
  5. After saving the VM state in a snapshot using the script, restart it with ./qemu.sh drivernumber 11 where drivernumber is the same as in the last step. The purpose of this command is to re-start the VM using the symbolic-execution-enabled S2E runtime. Add 98 to the command if you want to disable VNC, so if you're using lp5523, the modified command line would look like this: ./qemu.sh 98 44 11. If you're leaving VNC enabled (the default), then you may need to reconnect your VNC client.
  6. At this point, you should have a running VM again -- it should have resumed the one you saved previously. To test the driver, execute the following commands:
    1. modprobe spi-bitbang # This could be compiled into the kernel
    2. insmod ./test_framework.ko g_i2c_enable=1 g_i2c_chip_addr=0x30 g_i2c_names=lp5523
    3. insmod ./lp5523-stub.ko
    To simplify these steps, we use scripts for loading/unloading modules with various parameters.
  7. In the case of this specific driver, the lp5523, the driver should load and return to the command prompt. While the driver loads, you're going to get a huge amount of output. SymDrive prints a great deal of information to the console to make it obvious at any point where execution is. You can test other entry points by running cd /sys/devices/i2c-1/1-0030, followed by ls -la inside the VM. This driver exports a variety of interfaces via the sysfs file system.
  8. The driver included in the download includes two annotations that correct bugs we found. You can search the leds-lp5523.c for ENABLE_MJR_SYMDRIVE to find the loacations that we modified. The driver is otherwise identical to the one distributed in Linux 3.1.1.
  9. This driver represents a straightforward demonstration of what SymDrive can do: it allows developers to load drivers successfully, and then test individual entry points on a per-driver or per-driver-class basis.

qemu.sh

Run qemu.sh to see a list of options. The purpose of this script is to automate as much of the mechanical work as possible to make it easier to focus on getting results. The general idea is that you can provide the various options on the command line, and they're read from first to last. So, the last command is usually "run S2E," and the preceding options will control what happens when you do. This script is entirely optional, and you can instead run the S2E VM manually as described on the S2E website.

We strongly recommend against running this script with options until you've read and understand both the material below and the script. This script was designed for us to make our lives simpler and it may not work well in other environments. Some of the commands in it involve creating/deleting the VM disk image: do not use those commands unless you're sure they do the right thing. Now, all that said, we expect this script will serve as a useful guide for how to run drivers with SymDrive, which is why we've released it.

The qemu.shscript does do some special things if the current user's name is mjr or kadav, so be advised. This extra functionality only applies in our environment, and we included it in the script largely for our convenience.

To reiterate, this script is provided only because we found it helpful--don't blame us if you have problems. That said, please do report issues with it and we'll try to get it fixed.

LP5523 Notes

Since posting this demo, it has come to light that there may be a bug that prevents SymDrive from unloading the LP5523 driver. Because of time constraints, we've not yet isolated the problem. Be advised the executing rmmod lp5523-stub will fail deterministically. It is nevertheless possible to load the driver and test its entry points. We apologize for the error.

If you'd like to reproduce one of the two bugs we found, make the following changes to the instructions:

  1. Replace the leds-lp5523.c file in test/lp5523 directory with the original, unmodified copy from the 3.1.1 kernel, which is located at kernel_root/drivers/leds.
  2. Once replaced, recompile the driver using make.sh and then proceed as described.
  3. These two steps are necessary because the version of the driver distributed here includes fixes for the bugs we found.
  4. Inside the virtual machine, use insmod ./test_framework.ko g_sym_starting_fn=lp5523_probe g_i2c_enable=1 g_i2c_chip_addr=0x30 g_i2c_names=lp5523 when loading the test_framework. The key difference relative to the command line used originally is the g_sym_starting_fn directive, which instructs SymDrive to activate high-coverage mode in the probe function.

Limitations

SymDrive cannot magically work with all drivers. It uses heuristics that may fail. This section outlines how to work around these limitations.

License

Copyright (c) 2012, Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.