============================================== S2E: The Selective Symbolic Execution Platform ============================================== S2E is a platform for writing tools that analyze the properties and behavior of software systems. S2E comes as a modular library that gives virtual machines symbolic execution and program analysis capabilities. S2E 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. This documentation explains in details how to set up S2E, how to symbolically execute programs, and how to find vulnerabilities in them. S2E is pronounced *S two E*. .. toctree:: :caption: Getting Started :maxdepth: 1 Start here: setting up S2E BuildingS2E Tutorials/BasicLinuxSymbex/s2e.so Tutorials/BasicLinuxSymbex/SourceCode .. toctree:: :caption: Use Cases :maxdepth: 1 Tutorials/PoV/pov Tutorials/PoV/index Combining Kaitai Struct and S2E for analyzing parsers [external] Analyzing trigger-based malware with S2E [external] Solving CTF challenges with S2E [external] Tutorials/SystemTap/index.rst Tutorials/WindowsDLL/index.rst Tutorials/WindowsDrivers/FaultInjection.rst Tutorials/MSOffice/index.rst Tutorials/CFI/index.rst Tutorials/Revgen/Revgen.rst EquivalenceTesting .. toctree:: :caption: Howtos :maxdepth: 1 Howtos/Coverage/index.rst Communicating between the guest and S2E plugins MovingFiles Running S2E on multiple cores Using execution tracers ImageInstallation Writing S2E plugins Howtos/LuaInstrumentation .. toctree:: :caption: Scaling Symbolic Execution :maxdepth: 1 Howtos/Concolic StateMerging Tools/ForkProfiler FAQ .. toctree:: :caption: Development :maxdepth: 1 DesignAndImplementation/KvmInterface Contribute Profiling/ProfilingS2E DebuggingS2E Testsuite WindowsEnvSetup .. toctree:: :caption: Plugin Reference :maxdepth: 1 Plugins/Linux/LinuxMonitor Plugins/Windows/WindowsMonitor Plugins/RawMonitor Plugins/ModuleExecutionDetector ExecutionTracer Plugins/FunctionMonitor Plugins/Linux/FunctionModels Plugins/EdgeKiller Publications ============ * `S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems `_. Vitaly Chipounov. EPFL PhD Thesis, July 2014 * `The S2E Platform: Design, Implementation, and Applications `_. Vitaly Chipounov, Volodymyr Kuznetsov, George Candea. ACM Transactions on Computer Systems (TOCS), 30(1), Special issue: Best papers of ASPLOS, February 2012. * `Enabling Sophisticated Analysis of x86 Binaries with RevGen `_. Vitaly Chipounov and George Candea. 7th Workshop on Hot Topics in System Dependability (HotDep), Hong Kong, China, June 2011 * `S2E: A Platform for In Vivo Multi-Path Analysis of Software Systems `_. Vitaly Chipounov, Volodymyr Kuznetsov, George Candea. 16th Intl. Conference on Architectural Support for Programming Languages and Operating Systems (`ASPLOS `_), Newport Beach, CA, March 2011. * `Testing Closed-Source Binary Device Drivers with DDT `_. Volodymyr Kuznetsov, Vitaly Chipounov, George Candea. USENIX Annual Technical Conference (`USENIX `_), Boston, MA, June 2010. * `Reverse Engineering of Binary Device Drivers with RevNIC `_. Vitaly Chipounov and George Candea. 5th ACM SIGOPS/EuroSys European Conference on Computer Systems (`EuroSys `_), Paris, France, April 2010. * `Selective Symbolic Execution `_. Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, George Candea. Proc. 5th Workshop on Hot Topics in System Dependability, Lisbon, Portugal, June 2009