Related Work

SymDrive would not be possible without the technology provided by the following pieces of software.

S2E. S2E can execute a complete x86 virtual machine using symbolic execution. With S2E, it is possible to examine runtime properties along many possible execution paths. SymDrive includes extensions to S2E related to path selection and prioritization, tracing, and symbolic hardware.

KLEE. S2E builds upon KLEE's symbolic execution capability. By itself, KLEE can execute re-compiled user-mode applications symbolically.

QEMU. QEMU provides the virtual machine support that S2E uses.

LLVM. S2E uses LLVM to recompile x86 binary code on-the-fly, so that it can execute symbolically using KLEE.

CIL. CIL is a static source code analysis and code generation tool for C code. SymGen, the CIL-based code generation tool that SymDrive uses, is based on CIL. SymGen statically modifies the code of the device driver under test so that it communicates relevant source-level information to the underlying SymDrive runtime, such as where loops are and when individual driver functions execute.

Decaf Drivers. SymGen is based on a simplified version of DriverSlicer, a key component of Decaf Drivers.

For additional related research projects, please see the references provided in the paper.