research-article

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

Authors:

Vitaly Chipounov,

Volodymyr Kuznetsov,

George CandeaAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 3

Pages 265 - 278

https://doi.org/10.1145/1961296.1950396

Published: 05 March 2011 Publication History

Abstract

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--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.

Conceptually, S2E is an automated path explorer with modular path analyzers: the explorer drives the target system down all execution paths of interest, while analyzers check properties of each such path (e.g., to look for bugs) or simply collect information (e.g., count page faults). Desired paths can be specified in multiple ways, and S2E users can either combine existing analyzers to build a custom analysis tool, or write new analyzers using the S2E API.

References

[1]

J. Anderson, L. Berc, J. Dean, S. Ghemawat, M. Henzinger, S.-T. Leung, D. Sites, M. Vandevoorde, C. A. Waldspurger, and W. E. Weihl. Continuous profiling: Where have all the cycles gone? In Symp. on Operating Systems Principles, 1997.

Digital Library

[2]

T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner. Thorough static analysis of device drivers. In ACM SIGOPS/EuroSys European Conf. on Computer Systems, 2006.

Digital Library

[3]

T. Ball, E. Bounimova, V. Levin, R. Kumar, and J. Lichtenberg. The static driver verifier research platform. In Intl. Conf. on Computer Aided Verification, 2010.

Digital Library

[4]

F. Bellard. QEMU, a fast and portable dynamic translator. In USENIX Annual Technical Conf., 2005.

Digital Library

[5]

A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM, 53(2), 2010.

Digital Library

[6]

Bochs IA-32 Emulator. http://bochs.sourceforge.net/.

[7]

P. Boonstoppel, C. Cadar, and D. R. Engler. RWset: Attacking path explosion in constraint-based test generation. In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2008.

Digital Library

[8]

D. Brumley, C. Hartwig, M. G. Kang, Z. L. J. Newsome, P. Poosankam, D. Song, and H. Yin. BitScope: Automatically dissecting malicious binaries. Technical Report Carnegie Mellon University-CS-07-133, Carnegie Mellon University, 2007.

[9]

P. P. Bungale and C.-K. Luk. PinOS: a programmable framework for whole-system dynamic instrumentation. In Intl. Conf. on Virtual Execution Environments, 2007.

Digital Library

[10]

M. Burrows, U. Erlingson, S.-T. Leung, M. T. Vandevoorde, C. A. Waldspurger, K. Walker, and W. E. Weihl. Efficient and flexible value sampling. In Intl. Conf. on Architectural Support for Programming Languages and Operating Systems, 2000.

Digital Library

[11]

C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Symp. on Operating Systems Design and Implementation, 2008.

Digital Library

[12]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In Conf. on Computer and Communication Security, 2006.

Digital Library

[13]

V. Chipounov and G. Candea. Reverse engineering of binary device drivers with RevNIC. In ACM SIGOPS/EuroSys European Conf. on Computer Systems, 2010.

Digital Library

[14]

I. Dillig, T. Dillig, and A. Aiken. Sound, complete and scalable path-sensitive analysis. In Conf. on Programming Language Design and Implementation, 2008.

Digital Library

[15]

Dtrace. http://www.sun.com/bigadmin/content/dtrace/index.jsp.

[16]

P. Godefroid. Model checking for programming languages using Verisoft. In Symp. on Principles of Programming Languages, 1997.

Digital Library

[17]

P. Godefroid. Compositional dynamic test generation. In Symp. on Principles of Programming Languages, 2007. Extended abstract.

Digital Library

[18]

P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Conf. on Programming Language Design and Implementation, 2005.

Digital Library

[19]

P. Godefroid, M. Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In Network and Distributed System Security Symp., 2008.

[20]

IEEE. Standard 1666: SystemC language reference manual, 2005. http://standards.ieee.org/getieee/1666/.

[21]

Java PathFinder. http://javapathfinder.sourceforge.net, 2007.

[22]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 1976.

Digital Library

[23]

V. Kuznetsov, V. Chipounov, and G. Candea. Testing closed-source binary device drivers with DDT. In USENIX Annual Technical Conf., 2010.

Digital Library

[24]

M. S. Lam, J. Whaley, V. B. Livshits, M. C. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive program analysis as database queries. In Symp. on Principles of Database Systems, 2005.

Digital Library

[25]

C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In Intl. Symp. on Code Generation and Optimization, 2004.

Digital Library

[26]

Lua: A lightweight embeddable scripting language. http://www.lua.org/, 2010.

[27]

C.-K. Luk, R. Cohn, R. Muth, H. Patil, A. Klauser, G. Lowney, S. Wallace, V. J. Reddi, and K. Hazelwood. PIN: building customized program analysis tools with dynamic instrumentation. In Conf. on Programming Language Design and Implementation, 2005.

Digital Library

[28]

C. Murphy, G. Kaiser, I. Vo, and M. Chu. Quality assurance of software applications using the in vivo testing approach. In Intl. Conf. on Software Testing Verification and Validation, 2009.

Digital Library

[29]

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Symp. on Operating Systems Design and Implementation, 2008.

Digital Library

[30]

Oprofile. http://oprofile.sourceforge.net.

[31]

A. Pesterev, N. Zeldovich, and R. T. Morris. Locating cache performance bottlenecks using data profiling. In ACM SIGOPS/EuroSys European Conf. on Computer Systems, 2010.

Digital Library

[32]

C. Păasăreanu, P. Mehlitz, D. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In Intl. Symp. on Software Testing and Analysis, 2008.

Digital Library

[33]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4), 1997.

Digital Library

[34]

B. Schwarz, S. Debray, and G. Andrews. Disassembly of executable code revisited. In Working Conf. on Reverse Engineering, 2002.

Digital Library

[35]

K. Sen. Concolic testing. In Intl. Conf. on Automated Software Engineering, 2007.

Digital Library

[36]

K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In Symp. on the Foundations of Software Eng., 2005.

Digital Library

[37]

D. Song, D. Brumley, H. Yin, J. Caballero, I. Jager, M. G. Kang, Z. Liang, J. Newsome, P. Poosankam, and P. Saxena. Bitblaze: A new approach to computer security via binary analysis. In Intl. Conf. on Information Systems Security, 2008.

Digital Library

[38]

Valgrind. http://valgrind.org/.

[39]

D. Wheeler. SLOCCount. http://www.dwheeler.com/sloccount/, 2010.

[40]

J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou. MoDist: Transparent model checking of unmodified distributed systems. In Symp. on Networked Systems Design and Implementation, 2009.

Digital Library

[41]

J. Yang, C. Sar, and D. Engler. EXPLODE: a lightweight, general system for finding serious storage system errors. In Symp. on Operating Systems Design and Implementation, 2006.

Digital Library

[42]

M. T. Yourst. PTLsim: A cycle accurate full system x86-64 microarchitectural simulator. In IEEE Intl. Symp. on Performance Analysis of Systems and Software, 2007.

Cited By

Vouvoutsis VCasino FPatsakis C(2025)Beyond the sandbox: Leveraging symbolic execution for evasive malware classificationComputers & Security10.1016/j.cose.2024.104193149(104193)Online publication date: Feb-2025
https://doi.org/10.1016/j.cose.2024.104193
Yi XLi GLi JDing A(2024)RepFTI: Representation-Fused Function-Type Inference for Vehicular Secure Software SystemsApplied Sciences10.3390/app1411450214:11(4502)Online publication date: 24-May-2024
https://doi.org/10.3390/app14114502
Shen QMeng GChen K(2024)Revealing the exploitability of heap overflow through PoC analysisCybersecurity10.1186/s42400-024-00244-67:1Online publication date: 18-Jul-2024
https://doi.org/10.1186/s42400-024-00244-6
Show More Cited By

Index Terms

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

Recommendations

The S2E Platform: Design, Implementation, and Applications
Special Issue APLOS 2011

This article presents S²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 ...
S2E: a platform for in-vivo multi-path analysis of software systems
ASPLOS '11

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 ...
S2E: a platform for in-vivo multi-path analysis of software systems
ASPLOS XVI: Proceedings of the sixteenth international conference on Architectural support for programming languages and operating 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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 3

ASPLOS '11

March 2011

407 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1961296

Issue’s Table of Contents

ASPLOS XVI: Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems
March 2011
432 pages
ISBN:9781450302661
DOI:10.1145/1950365
General Chair:
Rajiv Gupta
University of California, Riverside
,
Program Chair:
Todd C. Mowry
Carnegie Mellon University

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 March 2011

Published in SIGPLAN Volume 46, Issue 3

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

456
Total Citations
View Citations
2,484
Total Downloads

Downloads (Last 12 months)147
Downloads (Last 6 weeks)22

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vouvoutsis VCasino FPatsakis C(2025)Beyond the sandbox: Leveraging symbolic execution for evasive malware classificationComputers & Security10.1016/j.cose.2024.104193149(104193)Online publication date: Feb-2025
https://doi.org/10.1016/j.cose.2024.104193
Yi XLi GLi JDing A(2024)RepFTI: Representation-Fused Function-Type Inference for Vehicular Secure Software SystemsApplied Sciences10.3390/app1411450214:11(4502)Online publication date: 24-May-2024
https://doi.org/10.3390/app14114502
Shen QMeng GChen K(2024)Revealing the exploitability of heap overflow through PoC analysisCybersecurity10.1186/s42400-024-00244-67:1Online publication date: 18-Jul-2024
https://doi.org/10.1186/s42400-024-00244-6
Li TBai JSui YHu S(2024)SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate AnalysisACM Transactions on Computer Systems10.1145/369525042:3-4(1-40)Online publication date: 6-Sep-2024
https://dl.acm.org/doi/10.1145/3695250
Jain RTihanyi NNdhlovu MFerrag MCordeiro Ld'Amorim M(2024)Rapid Taint Assisted Concolic Execution (TACE)Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663812(627-631)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663812
Feng ZMa JShrivastava ASui Y(2024)TWFuzz: Fuzzing Embedded Systems with Three WiresProceedings of the 25th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3652032.3657568(107-118)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652032.3657568
Zhang BChen WYao PWang CTang WZhang CTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)SIRO: Empowering Version Compatibility in Intermediate Representations via Program SynthesisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651366(882-899)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651366
Hu JDuan YYin HRoychoudhury APaiva AAbreu RStorey M(2024)Marco: A Stochastic Asynchronous Concolic ExplorerProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3623301(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3623301
Jiang MZheng XChang RZhou YLuo X(2024)Examiner-Pro: Testing Arm Emulators Across Different PrivilegesIEEE Transactions on Software Engineering10.1109/TSE.2024.340690050:11(2786-2806)Online publication date: Nov-2024
https://doi.org/10.1109/TSE.2024.3406900
Tu HJiang LHong JDing XJiang H(2024)Concretely Mapped Symbolic Memory Locations for Memory Error DetectionIEEE Transactions on Software Engineering10.1109/TSE.2024.339541250:7(1747-1767)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1109/TSE.2024.3395412
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents