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.
Vitaly Chipounov announced the 2.0 release of S2E on the s2e-dev GoogleGroup, excerpts of announcement below.
S2E 2.0 is a complete redesign of the old version, focusing on ease of use and speed. The advanced Python tooling lets you setup analysis projects in seconds with minimum knowledge of S2E. Everything is automated, from building guest images to writing configuration files based on the type of your binary. And if you don’t want to build S2E, there is a ready-to-run docker image that demonstrates vulnerability finding in DARPA CGC binaries, the same (almost) that we used during the competition.
Some of the major features include:
– Up to 6x faster in concrete mode than S2E 1.0
– Z3 constraint solver
– Advanced OS support including Linux guests and Windows XP, 7, 8, 10.
– Complete set of plugins for vulnerability analysis
– Integration with fuzzing
– Static x86-to-LLVM translation with Revgen