Christian Hammer
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.
- Quis custodiet. http://pp.info.uni-karlsruhe.de/project.php/id=31 funded by DFG Sn11/10-1.]]Google Scholar
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- using infeasible paths. In ESEC '97/FSE--5: Proceedings of the]]Google Scholar
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]] Google ScholarDigital Library
- S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst., 12(1): 26--60, 1990.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- J. Krinke. Program slicing. In Handbook of Software Engineering and Knowledge Engineering, volume 3: Recent Advances. World Scientific Publishing, 2005.]]Google ScholarDigital Library
- T. Lindholm and F. Yellin. The Java(TM) Virtual Machine Specification. Prentice Hall, 2nd edition, Apr. 1999.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- T. Robschink. Pfadbedingungen in Abhängigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik. PhD thesis, Universität Passau, January 2005.]]Google Scholar
- 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.]] Google ScholarDigital Library
- A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), January 2003.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
Index Terms
- Static path conditions for Java
Recommendations
Dynamic path conditions in dependence graphs
PEPM '06: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulationWe present a new approach combining dynamic slicing with path conditions in dependence graphs enhanced by dynamic information collected in a program trace. While dynamic slicing can only reveal that certain dependences have been holding during program ...
Efficient path conditions in dependence graphs for software safety analysis
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 ...
On temporal path conditions in dependence graphs
Program dependence graphs are a well-established device to represent possible information flow in a program. Path conditions in dependence graphs have been proposed to express more detailed circumstances of a particular flow; they provide precise ...
Comments