Documentation and Quick Start Guides for the S2E Symbolic Execution Platform
Switch branches/tags
Nothing to show
Clone or download

README.rst

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.

Getting started

  1. Creating analysis projects with s2e-env
  2. Building S2E without s2e-env
  3. Symbolic execution of Linux binaries
  4. Symbolic execution of arbitrary programs

Tutorials

  1. Automated proof of vulnerability generation with S2E
    1. The theory behind automated PoV generation using symbolic execution
    2. Using S2E to generate PoVs for Linux, Windows, and CGC binaries
  2. Combining Kaitai Struct and S2E for analyzing parsers (external link)
  3. Measuring code coverage with S2E
  4. Analysis of Linux binaries
    1. Using SystemTap with S2E
  5. Analysis of Windows binaries
    1. Analysis of Windows DLLs
    2. Testing error recovery code in Windows drivers with multi-path fault injection
  6. Customizing stock VM images
  7. Moving files between the guest and host
  8. Communicating between the guest and S2E plugins
  9. Running S2E on multiple cores
  10. Writing S2E plugins
  11. Using execution tracers
  12. Equivalence testing

Scaling symbolic execution

  1. Executing large programs with concolic execution
  2. Exponential analysis speedup with state merging
  3. Debugging path explosion with the fork profiler
  4. Frequently asked questions

S2E development

Plugin reference

OS 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.

Annotation plugins

These plugins allow the user to write plugins in Lua.

Miscellaneous plugins

  • FunctionMonitor provides client plugins with events triggered when the guest code invokes specified functions.
  • FunctionModels reduces path explosion by transforming common functions into symbolic expressions.
  • EdgeKiller kills execution paths that execute some sequence of instructions (e.g., polling loops).

Publications