The Selective Symbolic Execution (S²E) Platform

Do not forget the FAQ if you have 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.

Execution Tracers

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.

Selection Plugins

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.

Analysis Plugins

  • CacheSim implements a multi-path cache profiler.

Miscellaneous Plugins

  • FunctionMonitor provides client plugins with events triggered when the guest code invokes specified functions.
  • HostFiles allows to quickly upload files to the guest.

S²E Publications