Symbolic path simulation in path-sensitive dataflow analysis

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 , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 4: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 5: Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 6: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 7: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 8: Manuvir Das , Ben Liblit , Manuel Fähndrich , Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, Proceedings of the 8th International Symposium on Static Analysis, p.260-278, July 16-18, 2001
• 9: Alberto Coen-Porisini , Giovanni Denaro , Carlo Ghezzi , Mauro Pezzé, Using symbolic execution for verifying safety-critical systems, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 10: Neelam Gupta , Aditya P. Mathur , Mary Lou Soffa, Automated test data generation using an iterative relaxation method, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.231-244, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 11: Elsa L. Gunter , Doron Peled, Path Exploration Tool, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.405-419, March 22-28, 1999
• 12: Jian Zhang, Symbolic Execution of Program Paths Involving Pointer and Structure Variables, Proceedings of the Quality Software, Fourth International Conference on (QSIC'04), p.87-92, September 08-10, 2004 [doi>10.1109/QSIC.2004.32]
• 13: Yanhong A. Liu , Tom Rothamel , Fuxiang Yu , Scott D. Stoller , Nanjun Hu, Parametric regular path queries, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 14: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: Roman Manevich , Manu Sridharan , Stephen Adams , Manuvir Das , Zhe Yang, PSE: explaining program failures via postmortem static analysis, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 16: Dinakar Dhurjati, Manuvir Das, and Yue Yang. Path-sensitive dataflow analysis with iterative refinement. Technical Report MSR-TR-2005-108, Microsoft Corporation, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Verification

Keywords:
dataflow analysis, path feasibility, symbolic simulation