S²E is a platform for writing tools that analyze the properties and behavior of software systems. S²E comes as a modular library that gives virtual machines symbolic execution and program analysis capabilities. S²E runs unmodified x86, x86-64, or ARM software stacks, including programs, libraries, the kernel, and drivers. Symbolic execution then automatically explores hundreds of thousands of paths through the system, while analyzers check that the desired properties hold on these paths and selectors focus path exploration on components of interest. S²E is now commercially supported by Cyberhaven. It is free for non-commercial use. S²E was a research project of the Dependable Systems Lab at EPFL in Lausanne.
http://s2e.systems/docs/DesignAndImplementation/KvmInterface.html
Firmware Security 