The Selective Symbolic Execution (S²E) Platform

Contents

• The Selective Symbolic Execution (S²E) Platform
• S²E Documentation
  • Getting Started
  • Analyzing Windows Device Drivers
  • Analyzing the Linux Kernel
  • Howtos
  • S2E Tools
  • FAQ
• 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 the S²E Platform
• 2. Preparing VM Images for S²E
• 3. S²E Workflow
• 4. Quickly Uploading Programs to the Guest with s2eget
• 5. Testing a Simple Program with S2E
• 6. How to symbolically execute Linux binaries?
• 7. Analyzing Large Programs Using Concolic Execution
• 8. Equivalence Testing

Analyzing Windows Device Drivers

• 1. Analyzing Windows Drivers: Step-by-Step Tutorial
• 2. Setting Up the Checked Build of Windows

Analyzing the Linux Kernel

• 1. Compiling the Linux Kernel
• 2. Using SystemTap with S2E

Howtos

• 1. How to Use Execution Tracers?
• 2. How to Write an S2E plugin?
• 3. Parallel S2E
• 4. Debugging Guest Code

S2E Tools

1. Available Tools

   • 1. Fork Profiler
   • 2. Trace Printer
   • 3. Execution Profiler
   • 4. Coverage Generator

2. Supported Debug Information

FAQ

• 1. Frequently Asked Questions (FAQ)
  • 1.1. S2E
    • 1.1.1. How do I know what S2E is doing?
    • 1.1.2. Execution seems stuck/slow. What to do?
    • 1.1.3. How do I deal with path explosion?
    • 1.1.4. How to keep memory usage low?
    • 1.1.5. How much time is the constraint solver taking to solve constraints?
    • 1.1.6. What do the various fields in run.stats mean?

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