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. Researchers have used S²E to develop performance profilers, reverse engineering tools for proprietary software, vulnerability finding tools for both kernel-mode and user-mode binaries, scalable file system checkers, symbolic execution engines for interpreted languages, tools for finding trojan messages in distributed systems, verifying software routers, testing embedded systems, and more.

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 released under the MIT license and supported by the community. S²E was a research project of the Dependable Systems Lab at EPFL in Lausanne. For academic projects, please contact DSLAB.

Finding security vulnerabilities in binaries

Security researchers around the world use S²E to find critical vulnerabilities in all kinds of software. Here is a sample of some of the CVEs:

CVE-2017-15102, CVE-2016-5400: several vulnerabilities in Linux USB drivers that caused denial of service and complete system compromise.
CVE-2016-7219: information disclosure in a cryptography driver that affected all versions of Windows from Vista to 10.
CVE-2016-0040, CVE-2015-6098: buffer overflows in kernel components leading to local privilege escalation on various versions of Windows.
CVE-2015-1536: improper (un)marshalling of bitmaps triggered through the Android clipboard, integer overflow, and null pointer dereferencing that can crash the system, no permissions needed.

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 is powerful

  • It works at any level of the stack: applications, libraries, kernel drivers, and device firmware.
  • It generates test cases to prove the existence of vulnerabilities, without false positives.
  • It has advanced support for Windows and Linux targets with built-in support for execution tracing, code coverage, and profiling.
  • It automatically runs entire software stacks on hundreds of thousands of paths to find corner case vulnerabilities out of reach of traditional testing tools.

S²E is modular and flexible

  • You can run your existing analysis tools such as fuzzers or sanitizers on top of S²E to get the power of multi-path analysis for free.
  • Even if you don't need symbolic execution, you can still use S²E as a powerful single-path instrumentation platform.
  • Do you want to use S²E but don’t want the overhead of a VM? S²E emulates the KVM interface, which makes it easy to integrate into custom binary analysis projects.

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

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.