The S2E Platform

TLDR

The article introduces S 2 E, a platform for analyzing software systems, aimed at performance profiling, reverse engineering, and automated testing of kernel‑ and user‑mode binaries. S 2 E functions as an automated path explorer that drives symbolic execution across all relevant paths, with modular analyzers that measure properties, and scales to large systems through selective symbolic execution and execution‑consistency models. These techniques enable S 2 E to simultaneously analyze entire families of execution paths, perform in‑vivo analyses within real software stacks, and operate directly on binaries, including proprietary ones.

Abstract

This article presents S 2 E, a platform for analyzing the properties and behavior of software systems, along with its use in developing tools for comprehensive performance profiling, reverse engineering of proprietary software, and automated testing of kernel-mode and user-mode binaries. Conceptually, S 2 E is an automated path explorer with modular path analyzers: the explorer uses a symbolic execution engine to drive the target system down all execution paths of interest, while analyzers measure and/or check properties of each such path. S 2 E users can either combine existing analyzers to build custom analysis tools, or they can directly use S 2 E’s APIs. S 2 E’s strength is the ability to scale to large systems, such as a full Windows stack, using two new ideas: selective symbolic execution , a way to automatically minimize the amount of code that has to be executed symbolically given a target analysis, and execution consistency models , a way to make principled performance/accuracy trade-offs during analysis. These techniques give S 2 E three key abilities: to simultaneously analyze entire families of execution paths instead of just one execution at a time; to perform the analyses in-vivo within a real software stack---user programs, libraries, kernel, drivers, etc.---instead of using abstract models of these layers; and to operate directly on binaries, thus being able to analyze even proprietary software.