The Selective Symbolic Execution (S²E) Platform
Do not forget the FAQ if you have questions.
- Getting Started
- Analyzing Windows Device Drivers
- Analyzing the Linux Kernel
- S2E Tools
- Frequently Asked Questions
S²E Plugin Reference
OS Event Monitors
To implement selectivity, S2E relies on several OS-specific plugins to detect module loads/unloads and execution of modules of interest.
These plugins record various types of multi-path information during execution. This information can be processed by offline analysis tools. Refer to the How to use execution tracers? tutorial to understand how to combine these tracers.
These plugins allow you to specify which paths to execute and where to inject symbolic values
- StateManager helps exploring library entry points more efficiently.
- EdgeKiller kills execution paths that execute some sequence of instructions (e.g., polling loops).
- BaseInstructions implements various custom instructions to control symbolic execution from the guest.
- SymbolicHardware implements symbolic PCI and ISA devices as well as symbolic interrupts and DMA. Refer to the Windows driver testing tutorial for usage instructions.
- CodeSelector disables forking outside of the modules of interest
- Annotation plugin lets you intercept arbitrary instructions and function calls/returns and write Lua scripts to manipulate the execution state, kill paths, etc.
- CacheSim implements a multi-path cache profiler.
- 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