Static path conditions for Java

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Static path conditions for Java

Full text

Pdf (279 KB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security table of contents

Tucson, AZ, USA

SESSION: Software protection and verification table of contents

Pages 57-66

Year of Publication: 2008

ISBN:978-1-59593-936-4

Authors

Christian Hammer	Universität Karlsruhe (TH), Karlsruhe, Germany
Rüdiger Schaade	Universität Passau, Passau, Germany
Gregor Snelting	Universität Karlsruhe (TH), Karlsruhe, Germany

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 22, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	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/1375696.1375704 What is a DOI?

ABSTRACT

A static path condition is a precise necessary condition for information flow between two program points. Previous work defined path conditions for procedural languages. Object oriented languages offer additional constructs such as dynamic dispatch, instanceof and exceptions. In this paper, we present an analysis of these constructs, which leads to precise path conditions operating only on the program's variables. This yields a gain in precision, allowing leverage of automatic constraint solving. We present details of path condition generation for Java constructs, and discuss preliminary insight from our prototype implementation.

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	Quis custodiet. http://pp.info.uni-karlsruhe.de/project.php/id=31 funded by DFG Sn11/10-1.
	2	D. F. Bacon and P. F. Sweeney. Fast static analysis of c++ virtual function calls. In OOPSLA'96: Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 324--341, New York, NY, USA, 1996. ACM Press.
	3	G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld. Security of multithreaded programs by compilation. In European Symposium On Research In Computer Security (ESORICS'07), 2007.
	4	R. Bodík, R. Gupta, and M. L. Soffa. Refining data flow information using infeasible paths. In ESEC '97/FSE-5: Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, pages 361--377, New York, NY, USA, 1997. Springer-Verlag New York, Inc.
	5	G. Canfora, A. Cimitile, and A. D. Lucia. Conditioned program slicing. Information and Software Technology, 40(11-12): 595--607, Dec 1998. Special issue on Program Slicing.
	6	C. Chambers, I. Pechtchanski, V. Sarkar, M. J. Serrano, and H. Srinivasan. Dependence analysis for java. In Proceedings of the 12th International Workshop on Languages and Compilers for Parallel Computing, pages 35--52. Springer-Verlag, 1999.
	7	J. Dean, D. Grove, and C. Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In ECOOP'95: Proceedings of the 9th European Conference on Object-Oriented Programming, pages 77--101, London, UK, 1995. Springer-Verlag.
	8	X. Deng, Robby, and J. Hatcliff. Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs. In SEFM'07: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), pages 273--282, Washington, DC, USA, 2007. IEEE Computer Society.
	9	J. Field, G. Ramalingam, and F. Tip. Parametric program slicing. In POPL'95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 379--392, New York, NY, USA, 1995. ACM Press.
	10	C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for java. In PLDI'02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 234--245, New York, NY, USA, 2002. ACM.
	11	D. Giffhorn and C. Hammer. An evaluation of precise slicing algorithms for concurrent programs. In SCAM'07: Seventh IEEE International Working Conference on Source Code Analysis and Manipulation, pages 17--26, Paris, France, Sept. 2007.
	12	using infeasible paths. In ESEC '97/FSE--5: Proceedings of the
	13	C. Hammer, M. Grimme, and J. Krinke. Dynamic path conditions in dependence graphs. In PEPM'06: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, pages 58--67, New York, NY, USA, 2006. ACM Press.
	14	C. Hammer, J. Krinke, and F. Nodes. Intransitive noninterference in dependence graphs. In Proc. Second International Symposium on Leveraging Application of Formal Methods, Verification and Validation (ISoLA 2006), Paphos, Cyprus, Nov. 2006.
	15	C. Hammer, J. Krinke, and G. Snelting. Information flow control for java based on path conditions in dependence graphs. In Proc. IEEE International Symposium on Secure Software Engineering (ISSSE'06), Mar. 2006.
	16	C. Hammer and G. Snelting. An improved slicer for java. In PASTE'04: Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pages 17--22, New York, NY, USA, 2004. ACM Press.
	17	S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst., 12(1): 26--60, 1990.
	18	S. Hunt and D. Sands. On flow-sensitive security types. In POPL'06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 79--90, New York, NY, USA, 2006. ACM Press.
	19	R. Jhala and R. Majumdar. Path slicing. In PLDI'05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pages 38--47, New York, NY, USA, 2005. ACM Press.
	20	J. Krinke. Program slicing. In Handbook of Software Engineering and Knowledge Engineering, volume 3: Recent Advances. World Scientific Publishing, 2005.
	21	T. Lindholm and F. Yellin. The Java(TM) Virtual Machine Specification. Prentice Hall, 2nd edition, Apr. 1999.
	22	B. Livshits and M. S. Lam. Finding security vulnerabilities in Java applications with static analysis. In Proceedings of the Usenix Security Symposium, pages 271--286, Baltimore, Maryland, August 2005.
	23	B. Livshits, J. Whaley, and M. S. Lam. Reflection analysis for java. In Proceedings of the 3rd Asian Symposium (APLAS 2005), volume 3780 of LNCS, pages 139--160, Tsukuba, Japan, November 2005.
	24	A. Lochbihler and G. Snelting. On temporal path conditions in dependence graphs. In SCAM'07: Seventh IEEE International Working Conference on Source Code Analysis and Manipulation, pages 49--58, Paris, France, Sept. 2007.
	25	A. C. Myers. Jflow: practical mostly-static information flow control. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 228--241, New York, NY, USA, 1999. ACM Press.
	26	T. Robschink. Pfadbedingungen in Abhängigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik. PhD thesis, Universität Passau, January 2005.
	27	T. Robschink and G. Snelting. Efficient path conditions in dependence graphs. In ICSE '02: Proceedings of the 24th International Conference on Software Engineering, pages 478--488, New York, NY, USA, 2002. ACM Press.
	28	A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), January 2003.
	29	G. Smith and D. Volpano. Secure information flow in a multithreaded imperative language. In Proceedings of the Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 355--364, San Diego, CA, January 1998.
	30	G. Snelting. Combining slicing and constraint solving for validation of measurement software. In SAS'96: Proceedings of the Third International Symposium on Static Analysis, pages 332--348, London, UK, 1996. Springer-Verlag.
	31	G. Snelting, T. Robschink, and J. Krinke. Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol., 15(4):410--457, 2006.
	32	M. Sridharan, S. J. Fink, and R. Bodík. Thin slicing. In PLDI '07: Proceedings of the 2007 ACMSIGPLAN conference on Programming language design and implementation, pages 112--122, New York, NY, USA, 2007. ACM Press.
	33	F. Tip and J. Palsberg. Scalable propagation-based call graph construction algorithms. In OOPSLA '00: Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 281--293, New York, NY, USA, 2000. ACM Press.
	34	D. Wasserrab and A. Lochbihler. Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL. In Proceedings of the 21st International Conference of Theorem Proving in Higher Order Logics, Montréal, Québec, Canada, August 2008. Springer.