S²E: A Platform for In-Vivo Analysis of Software Systems

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

S²E is now commercially supported by Cyberhaven. It is free for non-commercial use. S²E was a research project of the Dependable Systems Lab at EPFL in Lausanne.
For academic projects, please contact DSLAB. For commercial use, contact Cyberhaven.

Find security vulnerabilities in binaries

  • Work at any level of the stack: applications, libraries, kernel drivers, and device firmware
  • Generate test cases to prove the existence of vulnerabilities, without false positives
  • Easy integration in your workflow with advanced support for Windows and Linux targets
  • Automatically run entire software stacks on hundreds of thousands of paths to find corner case vulnerabilities out of reach of traditional testing tools

Unprecedented modularity and flexibility

  • Your existing analysis tools get the power of multi-path analysis for free
  • S²E emulates the KVM interface, easily adaptable to any KVM-based virtualization solution
  • Composed of independent libraries with well-defined interfaces
  • Want to use S²E but don’t want the overhead of a VM? You can effortlessly integrate S²E into your binary analysis projects.

State-of-the-art program analysis techniques

  • Efficient navigation through large state spaces with concolic and symbolic execution, state merging, static analysis, function summaries, incremental constraint solving
  • Security checking, testing, verification, reverse engineering, performance profiling, etc.
  • Quickly prototype your research ideas by combining existing plugins or writing your own
  • Used by hundreds of researchers around the world

S²E competed in the finals of the DARPA Cyber Grand Challenge

  • The Cyber Grand Challenge is a competition where opponents are computers whose goal is to automatically find, exploit, and defend running services against vulnerabilities.
  • Cyberhaven built the Galactica system as part of the CodeJitsu team, together with UC Berkeley and Syracuse University
  • 2 teams out of 7 used S²E during the finals
  • First blood: S²E exploited 7 binaries before everyone else!
  • S²E launched 392 successful attacks, twice as much as Mayhem and Xandra

Want to run S²E on CGC binaries? Check out the tutorials!

S²E discovered CVE-2015-1536 in Android 5.0.2

  • Found 3 unknown bugs in < 5 minutes
  • Improper (un)marshalling of bitmaps triggered through the clipboard
  • Integer overflow and NULL pointer dereferencing
    • No permissions needed
    • Can read uninitialized memory
    • Can crash the system (soft reboot)
  • 2 x NULL pointer dereferencing that can crash the system

Live Demo

This demo shows S2E finding vulnerabilities in the CADET_00001 binary from the Cyber Grand Challenge. Run the command below in order to try it out on your machine. There is no need to do anything besides typing this command. Downloading and setting up the docker image should take 5-10 minutes depending on your network connection and take around 10GB of disk space.

$ docker run --rm -ti -w $(pwd) -v $HOME:$HOME cyberhaven/s2e-demo \
  /demo/run.sh $(id -u) $(id -g) /demo/CADET_00001

You will see a dashboard showing how many test cases S2E found. These test cases demonstrate a program crash or the presence of an actual vulnerability, for which S2E found program inputs that allow an attacker to control the program's memory and/or register contents (i.e., a proof of vulnerability, or PoV). After a while, stop the analysis. The analysis output is stored on your host machine and you will find the test cases in $(pwd)/s2e-demo/projects/CADET_00001/s2e-last/{*.c|*.xml} files. Their format follows the CGC specification and they can be run in a CGC VM.