S2E

Getting Started

  • Start here: setting up S2E
    • Installing s2e-env
    • Using s2e-env
      • Creating a new environment
        • s2e_activate
      • Building S2E
      • Updating the source code
      • Building an image
        • Windows images
      • Creating a new analysis project
      • Target program arguments
      • Using seed files
      • Running your analysis
      • Parsing an execution trace
      • Importing and exporting projects
    • Next steps
  • Building the S2E platform manually
    • Building using Docker
    • Building S2E manually
      • Required packages
      • Checking out S2E
      • Building
      • Updating
      • Building the documentation
  • Symbolic Execution of Linux Binaries
    • Getting started
    • Using s2e.so
    • What about other symbolic input?
    • Configuring S2E for use with s2e.so
    • Modifying and building s2e.so
  • Instrumenting Program Source Code for S2E
    • Introduction
    • Compiling and running
    • Preparing the program for symbolic execution
    • Running the program in S2E
    • Terminating execution paths

Use Cases

  • Automated Generation of Proofs of Vulnerability with S2E
    • Understanding the Execution of a Vulnerable Program
      • Using Symbolic Execution to Generate PoVs
    • Identifying Advanced Vulnerability Patterns with S2E
      • Function Pointer Overwrite
      • Arbitrary Writes
      • Arbitrary Reads
      • Function Calls with Symbolic Parameters
    • Generating Replayable PoVs
    • Conclusion
  • Using S2E to generate PoVs for Linux, Windows, and CGC binaries
    • Quickstart on Windows and Linux
    • Understanding recipes
    • PoVs for DARPA Decree/CGC binaries
    • Understanding CGC-style PoVs
    • Plugin architecture overview
    • Plugins involved in PoV generation
    • The bootstrap script
  • Combining Kaitai Struct and S2E for analyzing parsers [external]
  • Analyzing trigger-based malware with S2E [external]
  • Solving CTF challenges with S2E [external]
  • Using SystemTap with S2E
    • Building and running SystemTap in S2E
    • Creating a simple SystemTap script for symbolic execution
    • Running the script in S2E
  • Analysis of Windows DLLs
    • Preparing the test environment
    • Generate basic block coverage
  • Testing Error Recovery Code in Windows Drivers with Multi-Path Fault Injection
    • Setting up S2E
    • Setting up the Windows Environment
    • Building the Sample Driver
    • Creating an S2E Driver Project
    • Customizing the Driver Project
    • Running the Driver
    • Getting Code Coverage Reports
    • Testing Error Recovery Code
    • Generating Crash Dumps
    • Understanding S2E Logs and Test Cases
    • Customizing Fault Injection
    • Debugging Tips
  • Analyzing Microsoft Office Documents
    • Building a Microsoft Office image
    • 2. Creating a test document
    • 3. Creating an analysis project
    • 4. Running the project
    • 5. Exercises
    • 6. Conclusion
  • Control Flow Integrity Checking with S2E
    • Setting up Microsoft Office
    • Running the CFI checker
    • Analyzing a malicious document
      • Locating CFI violations
      • Setting up WinDbg for analysis
      • Tracing the exploit
    • Design and implementation
    • Limitations
    • Conclusion
  • Translating binaries to LLVM with Revgen
    • Using Revgen
      • 1. Prerequisites
      • 2. Build the CGC binaries
      • 3. Translating a binary
      • 4. Running a translated CGC binary
    • Design and implementation
      • Translating basic blocks to LLVM
      • Stitching basic blocks into functions
      • Assumptions
      • Running translated binaries
    • Evaluation
  • Equivalence Testing
    • Program to Test
    • Configuring S2E
    • Running the Program in S2E
    • Interpreting the Results

Howtos

  • Measuring code coverage with S2E
    • Line coverage for Linux binaries
      • Building Coreutils
      • Running Coreutils concretely in S2E
      • Generating line coverage
    • Line coverage for shared libraries
    • Basic block coverage
    • Code coverage during symbolic execution
    • How does S2E record and compute coverage?
    • Line coverage for the Linux kernel
    • Line coverage for Windows binaries
    • Debugging code coverage
  • Communicating between the guest and S2E plugins
  • Copying files between the host and the guest
    • s2ecmd get
    • s2ecmd put
    • Setting up the HostFiles Plugin
  • Running S2E on multiple cores
    • Handling execution traces
    • Limitations
  • Using execution tracers
    • 1. Recording basic traces
    • 2. Analyzing traces
    • 3. Recording memory traces
    • 4. Trace format reference
  • Customizing stock VM images
    • Image creation overview
    • Building Linux images
    • Building Windows images
    • When should I install my software?
    • The S2E VM image format
    • General guidelines for VM images
  • Writing S2E plugins
    • Starting with an empty plugin
    • Reading configuration parameters
    • Instrumenting instructions
    • Counting instructions
    • Exporting events
    • Guest-plugin communication
  • Instrumenting guest code with Lua
    • Instrumenting function calls and returns
    • Instrumenting instructions
    • API Reference
      • LuaS2EExecutionState
      • LuaS2EExecutionStateMemory
      • LuaS2EExecutionStateRegisters
      • LuaFunctionInstrumentationState
      • LuaInstructionInstrumentationState
      • LuaExpression
      • The g_s2e object

Scaling Symbolic Execution

  • Analyzing large programs using concolic execution
    • Executing programs in concolic mode
    • FAQ
  • Exponential Analysis Speedup with State Merging
    • Using State Merging in S2E
    • State Merging API
    • Limitations
  • Debugging path explosion with the fork profiler
    • Using the fork profile to debug path explosion
  • Frequently Asked Questions (FAQ)
    • How do I know what S2E is doing?
    • Execution seems stuck/slow. What to do?
    • How do I deal with path explosion?
    • How to keep memory usage low?
    • How much time is the constraint solver taking to solve constraints?
    • What do the various fields in stats.csv mean?

Development

  • Symbolic Execution Extensions for KVM
    • Kernel-based Virtual Machine (KVM)
    • Emulating the KVM interface
      • Using system call hooks for emulation
      • Differences between actual KVM and KVM emulation
      • Summary
    • Adding symbolic execution capabilities to KVM
      • Multi-path execution
      • Handling symbolic data
    • Reference
      • Dynamic binary translation
      • Registering memory regions
      • Accessing guest memory
      • Interrupting execution
      • Virtual disk I/O
      • Saving/restoring device snapshots
      • Setting the clock scale pointer
      • KVM_RUN exit codes
  • Contributing to S2E
  • Profiling S2E
    • Profiling memory usage
    • Profiling CPU performance
  • Debugging S2E
    • The obvious checks
    • Record-replay
    • Valgrind
    • Debugging with gdb
    • S2E kernel debugging
    • S2E debug functions
  • S2E Testsuite
    • Building the testsuite
    • Running the testsuite
    • Adding your own tests
    • Test configuration reference
  • Setting up a Windows development environment
    • 1. Provisioning a Windows development VM
    • 2. Building Visual Studio projects remotely
    • 3. Use case: building and running a Windows device driver

Plugin Reference

  • LinuxMonitor
    • Options
    • Required Plugins
  • WindowsMonitor
    • Options
  • RawMonitor
    • Custom Instruction
    • Options
    • Configuration Sample
  • ModuleExecutionDetector
    • Configuration Sample
  • ExecutionTracer
    • ExecutionTracer
    • ModuleTracer
    • TestCaseGenerator
    • MemoryTracer
    • TranslationBlockTracer
    • InstructionCounter
    • Filtering Plugins
      • ProcessExecutionDetector
      • ThreadExecutionDetector
      • ModuleExecutionDetector
  • FunctionMonitor
  • FunctionModels
    • Testing
    • Options
  • EdgeKiller
    • Options
    • Required Plugins
    • Configuration Sample
S2E
  • Search

© Copyright 2018-2020, Cyberhaven.

Built with Sphinx using a theme provided by Read the Docs.