article

Software validation via scalable path-sensitive value flow analysis

Authors:

Zhe YangAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 29, Issue 4

Pages 12 - 22

https://doi.org/10.1145/1013886.1007515

Published: 01 July 2004 Publication History

Abstract

In this paper, we present a new algorithm for tracking the flow of values through a program. Our algorithm represents a substantial improvement over the state of the art. Previously described value flow analyses that are control-flow sensitive do not scale well, nor do they eliminate value flow information from infeasible execution paths (i.e., they are path-insensitive). Our algorithm scales to large programs, and it is path-sensitive.The efficiency of our algorithm arises from three insights: The value flow problem can be "bit-vectorized" by tracking the flow of one value at a time; dataflow facts from different execution paths with the same value flow information can be merged; and information about complex aliasing that affects value flow can be plugged in from a different analysis.We have incorporated our analysis in ESP, a software validation tool. We have used ESP to validate the Windows operating system kernel (a million lines of code) against an important security property. This experience suggests that our algorithm scales to large programs, and is accurate enough to trace the flow of values in real code.

References

[1]

A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.]]

Digital Library

[2]

A. Aiken, J. S. Foster, J. Kodumal, and T. Terauchi. Checking and inferring local non-aliasing. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 129--140, 2003.]]

Digital Library

[3]

K. Ashcraft and D. Engler. Using Programmer-Written Compiler Extensions to Catch Security Holes. In Proceedings of the IEEE Symposium on Security and Privacy, 2002.]]

Digital Library

[4]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of SPIN '01, 8th Annual SPIN Workshop on Model Checking of Software, May 2001.]]

Digital Library

[5]

R. Bodik and S. Anik. Path-sensitive value-flow analysis. In Conference Record of the Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 237--251, 1998.]]

Digital Library

[6]

M. Bozga, R. Iosif, and Y. Laknech. Storeless semantics and alias logic. In Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 55--65, June 2003.]]

Digital Library

[7]

W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software - Practice and Experience, 30(7):775--802, 2000.]]

Digital Library

[8]

R. Chatterjee, B. G. Ryder, and W. Landi. Relevant context inference. In Conference Record of the Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 133--146, 1999.]]

Digital Library

[9]

M. Das. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, 2000.]]

Digital Library

[10]

M. Das, S. Lerner, and M. Seigle. ESP: Path-Sensitive Program Verification in Polynomial Time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]

Digital Library

[11]

M. Das, B. Liblit, M. Fähndrich, and J. Rehof. Estimating the Impact of Scalable Pointer Analysis on Optimization. In 8th International Symposium on Static Analysis, 2001.]]

Digital Library

[12]

R. Deline and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, 2001.]]

Digital Library

[13]

N. Dor, S. Adams, M. Das, and Z. Yang. Path sensitive value flow analysis on large programs. Technical Report MSR-TR-2003-58, Microsoft Research, 2003.]]

[14]

C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]

Digital Library

[15]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]

Digital Library

[16]

D. Gries. The Science of Programming. Springer-Verlag, 1987.]]

Digital Library

[17]

S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002.]]

Digital Library

[18]

N. Heintze and O. Tardieu. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 254--263, 2001.]]

Digital Library

[19]

M. Hind. Pointer analysis: Haven't we solved this problem yet? In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE'01), pages 54--61, 2001.]]

Digital Library

[20]

M. Hind and A. Pioli. Evaluating the effectiveness of pointer alias analyses. Science of Computer Programming, 39(1):31--55, Jan. 2001.]]

Digital Library

[21]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst., 12(1):26--60, January 1990.]]

Digital Library

[22]

N. D. Jones and S. S. Muchnick. Flow analysis and optimization of LISP-like structures. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 244--256, 1979.]]

Digital Library

[23]

U. P. Khedkar and D. M. Dhamdhere. A generalised theory of bit vector data flow analysis. ACM Trans. Program. Lang. Syst., 16(5):1472--1511, 1994.]]

Digital Library

[24]

J. Knoop and B. Steffen. Efficient and optimal bit-vector dataflow analyses: A uniform interprocedural framework. Technical Report Bericht Nr. 9309, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, Germany, 1993.]]

[25]

A. Milanova, A. Rountev, and B. G. Ryder. Precise and Efficient Call Graph Construction for C Programs with Function Pointers. Journal of Automated Software Engineering, 2004. To appear.]]

Digital Library

[26]

T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural data flow analysis via graph reachability. In Conference Record of the Twenty-Second ACM Symposium on Principles of Programming Languages, 1995.]]

Digital Library

[27]

M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Conference Record of the Twenty-Sixth ACM Symposium on Principles of Programming Languages, 1999.]]

Digital Library

[28]

M. Shapiro and S. Horwitz. The effects of the precision of pointer analysis. In LNCS 1302, 4th International Symposium on Static Analysis, Sept. 1997.]]

Digital Library

[29]

O. Shivers. Control-Flow Analysis Of Higher-Order Languages. PhD thesis, Carnegie Mellon University, May 1991.]]

Digital Library

[30]

B. Steensgaard. Points-to analysis in almost linear time. In Conference Record of the Twenty-Third ACM Symposium on Principles of Programming Languages, 1996.]]

Digital Library

[31]

R. P. Wilson and M. Lam. Efficient context-sensitive pointer analysis for C programs. In Proceedings of the ACM SIGPLAN 95 Conference on Programming Language Design and Implementation, 1995.]]

Digital Library

Cited By

Yang X(2025)Boosting static bug detection via demand-driven points-to analysisThird International Conference on Communications, Information System, and Data Science (CISDS 2024)10.1117/12.3057629(3)Online publication date: 4-Jan-2025
https://doi.org/10.1117/12.3057629
Pathade KKhedker U(2023)Computing maximum fixed point solutions over feasible paths in data flow analysesScience of Computer Programming10.1016/j.scico.2023.102944228(102944)Online publication date: Jun-2023
https://doi.org/10.1016/j.scico.2023.102944
Zuo ZWang KHussain ASani AZhang YLu SDou WWang LLi XWang CXu G(2021)Systemizing Interprocedural Static Analysis of Large-scale Systems Code with GraspanACM Transactions on Computer Systems10.1145/346682038:1-2(1-39)Online publication date: 29-Jul-2021
https://dl.acm.org/doi/10.1145/3466820
Show More Cited By

Index Terms

Software validation via scalable path-sensitive value flow analysis

Recommendations

Software validation via scalable path-sensitive value flow analysis
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis

In this paper, we present a new algorithm for tracking the flow of values through a program. Our algorithm represents a substantial improvement over the state of the art. Previously described value flow analyses that are control-flow sensitive do not ...
Semi-sparse flow-sensitive pointer analysis
POPL '09

Pointer analysis is a prerequisite for many program analyses, and the effectiveness of these analyses depends on the precision of the pointer information they receive. Two major axes of pointer analysis precision are flow-sensitivity and context-...
Semi-sparse flow-sensitive pointer analysis
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pointer analysis is a prerequisite for many program analyses, and the effectiveness of these analyses depends on the precision of the pointer information they receive. Two major axes of pointer analysis precision are flow-sensitivity and context-...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 29, Issue 4

July 2004

284 pages

ISSN:0163-5948

DOI:10.1145/1013886

Issue’s Table of Contents

ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis
July 2004
294 pages
ISBN:1581138202
DOI:10.1145/1007512
General Chair:
George Avrunin
University of Massachusetts, USA
,
Program Chair:
Gregg Rothermel
University of Nebraska -- Lincoln, USA

Copyright © 2004 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: 01 July 2004

Published in SIGSOFT Volume 29, Issue 4

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

54
Total Citations
View Citations
1,122
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yang X(2025)Boosting static bug detection via demand-driven points-to analysisThird International Conference on Communications, Information System, and Data Science (CISDS 2024)10.1117/12.3057629(3)Online publication date: 4-Jan-2025
https://doi.org/10.1117/12.3057629
Pathade KKhedker U(2023)Computing maximum fixed point solutions over feasible paths in data flow analysesScience of Computer Programming10.1016/j.scico.2023.102944228(102944)Online publication date: Jun-2023
https://doi.org/10.1016/j.scico.2023.102944
Zuo ZWang KHussain ASani AZhang YLu SDou WWang LLi XWang CXu G(2021)Systemizing Interprocedural Static Analysis of Large-scale Systems Code with GraspanACM Transactions on Computer Systems10.1145/346682038:1-2(1-39)Online publication date: 29-Jul-2021
https://dl.acm.org/doi/10.1145/3466820
Pathade KKhedker UAmaral JKulkarni M(2019)Path sensitive MFP solutions in presence of intersecting infeasible control flow path segmentsProceedings of the 28th International Conference on Compiler Construction10.1145/3302516.3307349(159-169)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.1145/3302516.3307349
Xu XSui YYan HXue JAtlee JBultan TWhittle J(2019)VFixProceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00063(512-523)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICSE.2019.00063
Pathade KKhedker UDubach CXue J(2018)Computing partially path-sensitive MFP solutions in data flow analysesProceedings of the 27th International Conference on Compiler Construction10.1145/3178372.3179497(37-47)Online publication date: 24-Feb-2018
https://dl.acm.org/doi/10.1145/3178372.3179497
Wang KHussain AZuo ZXu GAmiri Sani AChen YTemam OCarter J(2017)GraspanProceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3037697.3037744(389-404)Online publication date: 4-Apr-2017
https://dl.acm.org/doi/10.1145/3037697.3037744
Valdiviezo MCifuentes CKrishnan P(2014)A Method for Scalable and Precise Bug Finding Using Program Analysis and Model CheckingProgramming Languages and Systems10.1007/978-3-319-12736-1_11(196-215)Online publication date: 2014
https://doi.org/10.1007/978-3-319-12736-1_11
Ding STan H(2013)Detection of Infeasible Paths: Approaches and ChallengesEvaluation of Novel Approaches to Software Engineering10.1007/978-3-642-45422-6_5(64-78)Online publication date: 2013
https://doi.org/10.1007/978-3-642-45422-6_5
Cai YYao PYe CZhang CCalandrino JTroncoso C(2023)Place your locks wellProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620446(3727-3744)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620446
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.

Figures

Tables

Media

View Issue’s Table of Contents