README.rst

S2E: The Selective Symbolic Execution Platform

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

This documentation explains in details how to set up S2E, how to symbolically execute programs, and how to find vulnerabilities in them.

Documentation

• 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. DARPA Cyber Grand Challenge
  2. Coreutils
  3. Windows DLL
  4. Combining Kaitai Struct and S2E for analyzing parsers (external link)
  5. Testing Error Recovery Code in Windows Drivers with Multi-Path Fault Injection
• Howtos
  1. Preparing a VM image for S2E
  2. Moving files between the guest and host
  3. Using execution tracers
  4. Running S2E on multiple cores
  5. Writing S2E plugins
  6. Writing S2E plugins in Python
  7. Communicating between the guest and S2E plugins
• Advanced topics
  1. Equivalence testing
  2. Exponential analysis speedup with state merging
  3. How to debug guest code?
  4. Executing large programs with concolic execution
• Analyzing the Linux Kernel
  1. Building the Linux kernel
  2. Using SystemTap with S2E
• S2E Tools
  1. Fork profiler
  2. Trace printer
  3. Execution profiler
• Frequently Asked Questions

S2E Development

• Contributing to S2E
• Profiling S2E
• Debugging S2E
• Python plugin architecture

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

• LinuxMonitor
• WindowsMonitor
• RawMonitor
• ModuleExecutionDetector

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.

• ExecutionTracer
• ModuleTracer
• TestCaseGenerator
• TranslationBlockTracer
• InstructionCounter

Selection Plugins

These plugins allow you to specify which paths to execute and where to inject symbolic values.

• EdgeKiller kills execution paths that execute some sequence of instructions (e.g., polling loops).

Annotation Plugins

These plugins allow the user to write plugins in Lua.

• Function and Instruction Annotations

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.

S2E Publications

• 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