S2E: a platform for in-vivo multi-path analysis of software systems

This paper presents S2E, a platform for analyzing the properties and behavior of software systems. We demonstrate S2E’s use in developing practical tools for comprehensive performance profiling, reverse engineering of proprietary software, and bug finding for both kernel-mode and user-mode binaries. Building these tools on top of S2E took less than 770 LOC and 40 person-hours each. S2E’s novelty consists of its ability to scale to large real systems, such as a full Windows stack. S2E is based on 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 relaxed execution consistency models, a way to make principled performance/accuracy trade-offs in complex analyses. 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—u...

• Type: Journal
• Year: 2011
• Where: ASPLOS
• Authors: Vitaly Chipounov, Volodymyr Kuznetsov, George Candea
• Keywords: ASPLOS 2011, Consistency Models, Programming Languages, Target Analysis, Windows Stack