index.rst

The Selective Symbolic Execution (S²E) Platform

Contents

• S²E Documentation
• S²E Plugin Reference
  • OS Event Monitors
  • Execution Tracers
  • Selection Plugins
  • Analysis Plugins
  • Miscellaneous Plugins
• S²E Development
• S²E Publications

Do not forget the FAQ if you have questions.

S²E Documentation

• Getting Started
  1. Building S2E
  2. Preparing a VM image for S2E
  3. Quickly uploading programs to the guest with s2eget
  4. Testing a simple program
  5. Testing Linux binaries
  6. Analyzing large programs using concolic execution
  7. Equivalence testing
• Analyzing Windows Device Drivers
  1. Step-by-step tutorial
  2. Setting up the checked build of Windows
• Analyzing the Linux Kernel
  1. Building the Linux kernel
  2. Using SystemTap with S2E
• Howtos
  1. How to use execution tracers?
  2. How to write an S2E plugin?
  3. How to run S2E on multiple cores?
  4. How to debug guest code?
• S2E Tools
  1. Available Tools
     1. Fork profiler
     2. Trace printer
     3. Execution profiler
     4. Coverage generator
  2. Supported debug information
• 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.

• 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

• 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 Development

• Contributing to S2E
• Profiling S2E

S²E 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