Efficient path conditions in dependence graphs for software safety analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

Efficient path conditions in dependence graphs for software safety analysis

Full text

Pdf (602 KB)

Source

ACM Transactions on Software Engineering and Methodology (TOSEM) archive
Volume 15 , Issue 4 (October 2006) table of contents

Pages: 410 - 457

Year of Publication: 2006

ISSN:1049-331X

Authors

Gregor Snelting	Universität Passau, Passau, Germany
Torsten Robschink	Universität Passau, Passau, Germany
Jens Krinke	Universität Passau, Passau, Germany

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 157, Citation Count: 12

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1178625.1178628 What is a DOI?

ABSTRACT

A new method for software safety analysis is presented which uses program slicing and constraint solving to construct and analyze path conditions, conditions defined on a program's input variables which must hold for information flow between two points in a program. Path conditions are constructed from subgraphs of a program's dependence graph, specifically, slices and chops. The article describes how constraint solvers can be used to determine if a path condition is satisfiable and, if so, to construct a witness for a safety violation, such as an information flow from a program point at one security level to another program point at a different security level. Such a witness can prove useful in legal matters.The article reviews previous research on path conditions in program dependence graphs; presents new extensions of path conditions for arrays, pointers, abstract data types, and multithreaded programs; presents new decomposition formulae for path conditions; demonstrates how interval analysis and BDDs (binary decision diagrams) can be used to reduce the scalability problem for path conditions; and presents case studies illustrating the use of path conditions in safety analysis. Applying interval analysis and BDDs is shown to overcome the combinatorial explosion that can occur in constructing path conditions. Case studies and empirical data demonstrate the usefulness of path conditions for analyzing practical programs, in particular, how illegal influences on safety-critical programs can be discovered and analyzed.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Hiralal Agrawal , Richard A. DeMillo , Eugene H. Spafford, Dynamic slicing in the presence of unconstrained pointers, Proceedings of the symposium on Testing, analysis, and verification, p.60-73, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120813]
	2	Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
	3	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
	4	Bell, D. and La Padula, L. 1973. Secure computer systems: Mathematical foundations. MITRE Tech. rep. 2547.
	5	Frédéric Benhamou , Alain Colmerauer, Constraint logic programming: selected research, MIT Press, Cambridge, MA, 1993
	6	Bent, L., Atkinson, D. C., and Griswold, W. G. 2000. A comparative study of two whole program slicers for C. Tech. rep. CS2000-0643, Department of Computer Science and Engineering. University of California, San Diego, CA.
	7	J. A. Bergstra , Jan Heering , Paul Klint, Algebraic specification, ACM Press, New York, NY, 1989
	8	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	9	Burke, M., Carini, P., Choi, J.-D., and Hind, M. 1995. Flow-insensitive interprocedural alias analysis in the presence of pointers. Lecture Notes in Computer Science, vol. 892, D. Gelertner, A. Nicolau, and D. Padua, Eds. Springer-Verlag, Berlin, Germany.
	10	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]
	11	Canfora, G., Cimitile, A., a. De Lucia, and Lucca, G. 1998. Conditioned program slicing. Inform. Softw. Techn. 40, (Special Issue on Program Slicing). 595--607.
	12	Common Criteria Project Sponsoring Organizations. 2004. Common criteria for information technology security evaluation. CCIMB-2004-01-001, Version 2.2, Revision 2561 (Jan.).
	13	James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
	14	Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
	15	Richard A. DeMillo , A. Jefferson Offutt, Constraint-Based Automatic Test Data Generation, IEEE Transactions on Software Engineering, v.17 n.9, p.900-910, September 1991 [doi>10.1109/32.92910]
	16	Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
	17	Andreas Dolzmann , Thomas Sturn, REDLOG: computer algebra meets computer logic, ACM SIGSAM Bulletin, v.31 n.2, p.2-9, June 1997 [doi>10.1145/261320.261324]
	18	Jeanne Ferrante , Karl J. Ottenstein , Joe D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.319-349, July 1987 [doi>10.1145/24039.24041]
	19	John Field , G. Ramalingam , Frank Tip, Parametric program slicing, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.379-392, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199534]
	20	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	21	Goguen, J. and Meseguer, J. 1984. Interference control and unwinding. In Proceedings of the Symposium on Security and Privacy. IEEE, 75--86.
	22	Allen Goldberg , T. C. Wang , David Zimmerman, Applications of feasible path analysis to program testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.80-94, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.186523]
	23	Arnaud Gotlieb , Bernard Botella , Michel Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.53-62, March 02-04, 1998, Clearwater Beach, Florida, United States
	24	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
	25	Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
	26	Jens Knoop , Bernhard Steffen , Jürgen Vollmer, Parallelism for free: efficient and optimal bitvector analyses for parallel programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.268-299, May 1996 [doi>10.1145/229542.229545]
	27	Jens Krinke, Static slicing of threaded programs, Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.35-42, June 16-16, 1998, Montreal, Quebec, Canada
	28	Evaluating Context-Sensitive Slicing and Chopping, Proceedings of the International Conference on Software Maintenance (ICSM'02), p.22, October 03-06, 2002
	29	Krinke, J. 2003a. Advanced slicing of sequential and concurrent programs. Ph.D. thesis, Universität Passau.
	30	Jens Krinke, Context-sensitive slicing of concurrent programs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
	31	Jens Krinke, Slicing, Chopping, and Path Conditions with Barriers, Software Quality Control, v.12 n.4, p.339-360, December 2004 [doi>10.1023/B:SQJO.0000039792.93414.a5]
	32	Krinke, J. and Snelting, G. 1998. Validation of measurement software as an application of slicing and constraint solving. Infor. Softw. Techn. (Special issue on Program Slicing). 661--675.
	33	Thomas Lengauer , Robert Endre Tarjan, A fast algorithm for finding dominators in a flowgraph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.121-141, July 1979 [doi>10.1145/357062.357071]
	34	Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
	35	Lind-Nielsen, J. 2001. BuDDy---A binary decision diagram package. Tech. rep., University of Copenhagen. http://www.itu.dk/reserach/buddy.
	36	Mantel, H., Stephan, W., Ullmann, M., and Vogt, R. 2000. Leitfaden für die Erstellung und Prüfung formaler Sicherheitsmodelle im Rahmen von ITSEC und Common Criteria. Tech. rep., Bundesamt für Sicherheit in der Informationstechnik und Deutsches Forschungszentrum für Künstliche Intelligenz. Version 0.8.
	37	Marriott, K. and Stuckey, P. 1998. Programming with Constraints. MIT Press, Cambridge, MA.
	38	Martin, F. 1998. PAG---An efficient program analyzer generator. Int. J. Softw. Tools Techn. Transfer 2, 1, 46--67.
	39	Charles E. McDowell , David P. Helmbold, Debugging concurrent programs, ACM Computing Surveys (CSUR), v.21 n.4, p.593-622, Dec. 1989 [doi>10.1145/76894.76897]
	40	Daniel Le Métayer , David Schmidt, Structural operational semantics as a basis for static program analysis, ACM Computing Surveys (CSUR), v.28 n.2, p.340-343, June 1996 [doi>10.1145/234528.234744]
	41	Gleb Naumovich , George S. Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.24-34, November 01-05, 1998, Lake Buena Vista, Florida, United States
	42	Karl J. Ottenstein , Linda M. Ottenstein, The program dependence graph in a software development environment, Proceedings of the first ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.177-184, April 1984
	43	William Pugh , David Wonnacott, Constraint-based array dependence analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.3, p.635-678, May 1998 [doi>10.1145/291889.291900]
	44	Quine, W. 1955. A way to simplify truth functions. Amer. Mathemat. Soc. 62, 627--631.
	45	G. Ramalingam, Identifying loops in almost linear time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.175-188, March 1999 [doi>10.1145/316686.316687]
	46	Reps, T. 1998. Program analysis via graph reachability. Inform. Softw. Techn. (Special issue on program slicing). 701--726.
	47	Thomas Reps, Undecidability of context-sensitive data-independence analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.162-186, Jan. 2000 [doi>10.1145/345099.345137]
	48	Thomas Reps , Susan Horwitz , Mooly Sagiv , Genevieve Rosay, Speeding up slicing, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.11-20, December 06-09, 1994, New Orleans, Louisiana, United States
	49	Thomas Reps , Genevieve Rosay, Precise interprocedural chopping, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.41-52, October 12-15, 1995, Washington, D.C., United States
	50	Robschink, T. 2005. Pfadbedingungen in Abhängigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik. Ph.D. thesis, Universität Passau.
	51	Torsten Robschink , Gregor Snelting, Efficient path conditions in dependence graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581398]
	52	K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
	53	Sabelfeld, A. and Myers, A. 2003. Language-based information-flow security. IEEE J. Select. Areas Comm 21, 1 (Jan.).
	54	Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
	55	Gregor Snelting, Combining Slicing and Constraint Solving for Validation of Measurement Software, Proceedings of the Third International Symposium on Static Analysis, p.332-348, September 24-26, 1996
	56	Vugranam C. Sreedhar , Guang R. Gao , Yong-Fong Lee, Identifying loops using DJ graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.6, p.649-658, Nov. 1996 [doi>10.1145/236114.236115]
	57	Thomas Sturm , Volker Weispfenning, Computational Geometry Problems in REDLOG, Selected Papers from the International Workshop on Automated Deduction in Geometry, p.58-86, September 27-29, 1996
	58	Tarjan, R. E. 1974. Testing flow graph reducibility. J. Comput. Syst. Science 9, 355--365.
	59	Teitelbaum, T. 2001. Code surfer user guide and reference. Tech. rep., Gramma Tech Product Documentation. http://www.grammatech.com/csurf-doc/manual.html.
	60	Tip, F. 1995. A survey of program slicing techniques. J. Program. Lang. 3, 3 (Sept.) 121--189.
	61	Weiser, M. 1984. Program slicing. IEEE Trans. Softw. Eng. 10, 4 (July), 352--357. (Republished in Berzins 1995).
	62	Volker Weispfenning, Simulation and optimization by quantifier elimination, Journal of Symbolic Computation, v.24 n.2, p.189-208, August 1997 [doi>10.1006/jsco.1997.0122]
	63	Volker Weispfenning, Mixed real-integre linear quantifier elimination, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.129-136, July 28-31, 1999, Vancouver, British Columbia, Canada [doi>10.1145/309831.309888]
	64	Stephen Wolfram, The Mathematica book (4th edition), Cambridge University Press, New York, NY, 1999

CITED BY 12

	Sigmund Cherem , Lonnie Princehouse , Radu Rugina, Practical memory leak detection using guarded value-flow analysis, ACM SIGPLAN Notices, v.42 n.6, June 2007
	M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
	Andrea Lanzi , Lorenzo Martignoni , Mattia Monga , Roberto Paleari, A Smart Fuzzer for x86 Executables, Proceedings of the Third International Workshop on Software Engineering for Secure Systems, p.7, May 20-26, 2007
	Salvador Cavadini, Secure slices of insecure programs, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan
	Christian Hammer , Rüdiger Schaade , Gregor Snelting, Static path conditions for Java, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	David Binkley , Mark Harman , Jens Krinke, Empirical study of optimization techniques for massive slicing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.1, p.3-es, November 2007
	Andreas Lochbihler , Gregor Snelting, On temporal path conditions in dependence graphs, Automated Software Engineering, v.16 n.2, p.263-290, June 2009
	Omer Tripp , Marco Pistoia , Stephen J. Fink , Manu Sridharan , Omri Weisman, TAJ: effective taint analysis of web applications, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Daniel Wasserrab , Denis Lohner , Gregor Snelting, On PDG-based noninterference and its modular proof, Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, June 15-21, 2009, Dublin, Ireland
	Colin J. Fidge , Diane Corney, Integrating hardware and software information flow analyses, ACM SIGPLAN Notices, v.44 n.7, July 2009
	Srihari Sukumaran , Ashok Sreenivas , Ravindra Metta, The dependence condition graph: Precise conditions for dependence between program points, Computer Languages, Systems and Structures, v.36 n.1, p.96-121, April, 2010
	Bernhard Scholz , Chenyi Zhang , Cristina Cifuentes, User-input dependence analysis via graph reachability, Sun Microsystems, Inc., Mountain View, CA, 2008