S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems
Speaker(s) : Vitaly Chipounov (EPFL) This talk presents S2E—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, S2E 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. S2E users can either combine existing analyzers to build custom analysis tools, or they can directly use S2E’s APIs.
S2E’s strength is the ability to scale to large systems, such as a full Windows stack, by augmenting a commodity virtual machine with 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 S2E 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.
Vitaly Chipounov is a Ph.D. student in Computer Science at EPFL, Switzerland, working at the Dependable Systems Laboratory led by Prof. George Candea. Vitaly's interest is to develop solutions for scalable analysis of software that allow developers to write more robust programs, while letting them continue using their existing languages, toolchains, and workflows. Before starting his Ph.D., Vitaly completed his Bachelor and Masters studies at EPFL, with a strong focus on low-level software and hardware development.
Gille.Muller (at) null