skip to main content
10.1145/1108792.1108808acmconferencesArticle/Chapter ViewAbstractPublication PagespasteConference Proceedingsconference-collections
Article

Symbolic path simulation in path-sensitive dataflow analysis

Published: 05 September 2005 Publication History

Abstract

Symbolic path simulation is becoming an increasingly important component in many static analysis tasks. The emergence of inter-procedural path-sensitive dataflow algorithms has both raised the demands and posed new challenges for effective techniques in path feasibility analysis.This paper develops a general-purpose path simulator and applies it to support path-sensitive dataflow analysis. The core component of the path simulator is a simulation engine that supports a wide variety of programming language features. This simulation engine can be "wrapped" with an interface layer to support a given client application.As a concrete case study, we discuss the experiences gained in integrating the path simulator with ESP, a software validation tool for C/C++ programs. We apply ESP to validate a future version of Windows against critical security properties. Our results show that the global path simulation mechanism is both critical in improving precision and scalable enough to be of practical use.

References

[1]
William R. Bush, Jonathan D. Pincus, and David J. Sielaff. A static analyzer for finding dynamic programming errors. Software - Practice and Experience, 30(7):775--802, 2000.]]
[2]
Thomas Ball and Sriram Rajamani. The SLAM project: debugging system software via static analysis. In the ACM Symposium on Principles of Programming Languages, 2002.]]
[3]
T. Henzinger, R. Jhala, R. Majumdar, and K. McMillan. Abstractions from proofs. In the ACM Symposium on Principles of Programming Languages, 2004.]]
[4]
Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]
[5]
Nurit Dor, Stephen Adams, Manuvir Das, and Zhe Yang. Software validation via scalable path-sensitive value flow analysis. In Proceedings of the International Symposium on Software Testing and Analysis, 2004.]]
[6]
R. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157--171, 1986.]]
[7]
Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural data flow analysis via graph reachability. In the ACM Symposium on Principles of Programming Languages, 1995.]]
[8]
Manuvir Das, Ben Liblit, Manuel Fähndrich, and Jakob Rehof. Estimating the Impact of Scalable Pointer Analysis on Optimization. In 8th International Symposium on Static Analysis, 2001.]]
[9]
Alberto Coen-Porisini, Giovanni Denaro, Carlo Ghezzi, and Mauro Pezze. Using symbolic execution for verifying safety-critical systems. In Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2001.]]
[10]
N Gupta, A Mathur, and M Soffa. Automated test data generation using an iterative relaxation method. In Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1998.]]
[11]
E Gunter and D Peled. Path exploration tool. In TACAS, 1999.]]
[12]
Jian Zhang. Symbolic execution of program paths involving pointer and structure vairalbes. In the Fourth International Conference on Quality Software, 2004.]]
[13]
Yanhong Liu, Tom Rothamel, Fuxiang Yu, Scott Stoller, and Nanjun Hu. Parametric regular path queries. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004.]]
[14]
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]
[15]
Roman Manevich, Manu Sridharan, Stephen Adams, Manuvir Das, and Zhe Yang. PSE: Explaining program failures via postmortem static analysis. In Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2004.]]
[16]
Dinakar Dhurjati, Manuvir Das, and Yue Yang. Path-sensitive dataflow analysis with iterative refinement. Technical Report MSR-TR-2005-108, Microsoft Corporation, 2005.]]

Cited By

View all
  • (2017)NIVAnalyzer: A Tool for Automatically Detecting and Verifying Next-Intent Vulnerabilities in Android Apps2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.56(492-499)Online publication date: Mar-2017
  • (2010)A memory model for static analysis of C programsProceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part I10.5555/1939281.1939332(535-548)Online publication date: 18-Oct-2010
  • (2010)A Memory Model for Static Analysis of C ProgramsLeveraging Applications of Formal Methods, Verification, and Validation10.1007/978-3-642-16558-0_44(535-548)Online publication date: 2010
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering
September 2005
118 pages
ISBN:1595932399
DOI:10.1145/1108792
  • cover image ACM SIGSOFT Software Engineering Notes
    ACM SIGSOFT Software Engineering Notes  Volume 31, Issue 1
    January 2006
    203 pages
    ISSN:0163-5948
    DOI:10.1145/1108768
    Issue’s Table of Contents
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. dataflow analysis
  2. path feasibility
  3. symbolic simulation

Qualifiers

  • Article

Conference

PASTE05

Acceptance Rates

Overall Acceptance Rate 57 of 159 submissions, 36%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)10
  • Downloads (Last 6 weeks)2
Reflects downloads up to 17 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2017)NIVAnalyzer: A Tool for Automatically Detecting and Verifying Next-Intent Vulnerabilities in Android Apps2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.56(492-499)Online publication date: Mar-2017
  • (2010)A memory model for static analysis of C programsProceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part I10.5555/1939281.1939332(535-548)Online publication date: 18-Oct-2010
  • (2010)A Memory Model for Static Analysis of C ProgramsLeveraging Applications of Formal Methods, Verification, and Validation10.1007/978-3-642-16558-0_44(535-548)Online publication date: 2010
  • (2009)A Memory Model for Symbolic ExecutionProceedings of the 2009 International Forum on Computer Science-Technology and Applications - Volume 0110.1109/IFCSTA.2009.11(20-24)Online publication date: 25-Dec-2009
  • (2009)A plethora of paths2009 IEEE 17th International Conference on Program Comprehension10.1109/ICPC.2009.5090026(40-49)Online publication date: May-2009
  • (2009)On temporal path conditions in dependence graphsAutomated Software Engineering10.1007/s10515-009-0050-316:2(263-290)Online publication date: 1-Jun-2009
  • (2008)Static Program Analysis for Java Card AppletsProceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications10.1007/978-3-540-85893-5_2(17-31)Online publication date: 8-Sep-2008
  • (2007)Fast Approximate Matching of Programs for Protecting Libre/Open Source Software by Using Spatial IndexesProceedings of the Seventh IEEE International Working Conference on Source Code Analysis and Manipulation10.1109/SCAM.2007.10(111-122)Online publication date: 30-Sep-2007
  • (2006)Path-Sensitive dataflow analysis with iterative refinementProceedings of the 13th international conference on Static Analysis10.1007/11823230_27(425-442)Online publication date: 29-Aug-2006
  • (2006)Beyond iteration vectorsProceedings of the 13th international conference on Static Analysis10.1007/11823230_11(161-180)Online publication date: 29-Aug-2006
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media