Static analysis for inference of explicit information flow

ABSTRACT

This paper proposes a new static analysis for inference of explicit information flow. The analysis is context-sensitive, cubic, and works both on complete programs and software components. We perform experiments on several Java components which show that the analysis is precise and practical. Thus, the analysis can be incorporated in program understanding and verification tools and help verify security properties in a light-weight, practical manner.

REFERENCES

• 1: T. Amtoft and A. Banerjee. Information flow analysis in logical form. In Proceedings of Static Analysis Symposium, pages 100--115, 2004.
• 2: Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
• 3: Jean-Pierre Banâtre , Ciarán Bryce , Daniel Le Métayer, Compile-Time Detection of Information Flow in Sequential Programs, Proceedings of the Third European Symposium on Research in Computer Security, p.55-73, November 07-09, 1994
• 4: A. Banerjee and D. Naumann. Using access control for secure information flow in a Java-like language. In IEEE Computer Security Foundations Workshop, pages 155--169, 2003.
• 5: Chiara Bodei , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static Analysis for Secrecy and Non-interference in Networks of Processes, Proceedings of the 6th International Conference on Parallel Computing Technologies, p.27-41, September 03-07, 2001
• 6: Jim Chow , Ben Pfaff , Tal Garfinkel , Kevin Christopher , Mendel Rosenblum, Understanding data lifetime via whole system simulation, Proceedings of the 13th conference on USENIX Security Symposium, p.22-22, August 09-13, 2004, San Diego, CA
• 7: D. Clark, C. Hankin, and S. Hunt. Information flow for Algol-like languages. Computer Languages, Systems and Structures, 28(1):3--28, 2002.
• 8: James Clause , Wanchun Li , Alessandro Orso, Dytan: a generic dynamic taint analysis framework, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273490]
• 9: A. Darvas, R. Hahnle, and D. Sands. A theorem proving approach to analysis of secure information flow. In International Conference on Security in Pervasive Computing, pages 193--209, 2005.
• 10: 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]
• 11: E. Ferrari , P. Samarati , E. Bertino , S. Jajodia, Providing flexibility in information flow control for object oriented systems, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.130, May 04-07, 1997
• 12: S. Genaim and F. Spoto. Information flow analysis for Java bytecode. In International Conference on Verification, Model Checking and Abstract Interpretation, pages 346--362, 2005.
• 13: V. Haldar, D. Chandra, and M. Franz. Practical, dynamic information flow for virtual machines. In International Workshop on Programming Language Interference and Dependence, 2005.
• 14: William G. J. Halfond , Alessandro Orso , Panagiotis Manolios, Using positive tainting and syntax-aware evaluation to counter SQL injection attacks, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181797]
• 15: Rajeev Joshi , K. Rustan M. Leino, A semantic approach to secure information flow, Science of Computer Programming, v.37 n.1-3, p.113-138, May 2000 [doi>10.1016/S0167-6423(99)00024-6]
• 16: Vladimir Kiriansky , Derek Bruening , Saman P. Amarasinghe, Secure Execution via Program Shepherding, Proceedings of the 11th USENIX Security Symposium, p.191-206, August 05-09, 2002
• 17: Monica S. Lam , Michael Martin , Benjamin Livshits , John Whaley, Securing web applications with static and dynamic information flow tracking, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.3-12, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328410]
• 18: O. Lhotak and L. Hendren. Scaling Java points-to analysis using Spark. In International Conference on Compiler Construction, pages 153--169, 2003.
• 19: Peng Li , Steve Zdancewic, Encoding Information Flow in Haskell, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.16, July 05-07, 2006 [doi>10.1109/CSFW.2006.13]
• 20: Y. Liu and A. Milanova. Static information flow analysis for Java. Technical Report 08-06, Rensselaer Polytechnic Institute, May 2008.
• 21: V. Benjamin Livshits , Monica S. Lam, Finding security vulnerabilities in java applications with static analysis, Proceedings of the 14th conference on USENIX Security Symposium, p.18-18, July 31-August 05, 2005, Baltimore, MD
• 22: Stephen McCamant , Michael D. Ernst, Quantitative information flow as network flow capacity, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 23: Ana Milanova, Precise identification of composition relationships for UML class diagrams, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101922]
• 24: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 25: J. Newsome and D. Song. Dynamic taint analysis: Automatic detection, analysis, and signature generation of exploit attacks on commodity software. In ACM Network and Distributed System Security Symposium, 2005.
• 26: A. Nguyen-Tuong, S. Guarnieri, D. Greene, J. Shirley, and D. Evans. Automatically hardening web applications using precise tainting. In IFIP International Information Security Conference, pages 295--307, 2005.
• 27: Feng Qin , Cheng Wang , Zhenmin Li , Ho-seop Kim , Yuanyuan Zhou , Youfeng Wu, LIFT: A Low-Overhead Practical Information Flow Tracking System for Detecting Security Attacks, Proceedings of the 39th Annual IEEE/ACM International Symposium on Microarchitecture, p.135-148, December 09-13, 2006 [doi>10.1109/MICRO.2006.29]
• 28: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 29: 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]
• 30: 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]
• 31: Atanas Rountev , Ana Milanova , Barbara G. Ryder, Points-to analysis for Java using annotated constraints, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.43-55, October 14-18, 2001, Tampa Bay, FL, USA
• 32: Fragment Class Analysis for Testing of Polymorphism in Java Software, IEEE Transactions on Software Engineering, v.30 n.6, p.372-387, June 2004 [doi>10.1109/TSE.2004.20]
• 33: A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.
• 34: Umesh Shankar , Kunal Talwar , Jeffrey S. Foster , David Wagner, Detecting format string vulnerabilities with type qaualifiers, Proceedings of the 10th conference on USENIX Security Symposium, p.16-16, August 13-17, 2001, Washington, D.C.
• 35: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, pages 189--234. Prentice Hall, 1981.
• 36: V. Simonet. Flow caml in a nutshell. In Applied Semantics II Workshop, pages 152--165, 2003.
• 37: Q. Sun, A. Banerjee, and D. Naumann. Modular and constraint-based information flow inference for an object-oriented language. In Static Analysis Symposium, pages 84--99, 2004.
• 38: Neil Vachharajani , Matthew J. Bridges , Jonathan Chang , Ram Rangan , Guilherme Ottoni , Jason A. Blome , George A. Reis , Manish Vachharajani , David I. August, RIFLE: An Architectural Framework for User-Centric Information-Flow Security, Proceedings of the 37th annual IEEE/ACM International Symposium on Microarchitecture, p.243-254, December 04-08, 2004, Portland, Oregon [doi>10.1109/MICRO.2004.31]
• 39: Raja Vallée-Rai , Etienne Gagnon , Laurie J. Hendren , Patrick Lam , Patrice Pominville , Vijay Sundaresan, Optimizing Java Bytecode Using the Soot Framework: Is It Feasible?, Proceedings of the 9th International Conference on Compiler Construction, p.18-34, March 25-April 02, 2000
• 40: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
• 41: Wei Xu , Sandeep Bhatkar , R. Sekar, Taint-enhanced policy enforcement: a practical approach to defeat a wide range of attacks, Proceedings of the 15th conference on USENIX Security Symposium, July 31-August 04, 2006, Vancouver, B.C., Canada

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms

Keywords:
flow analysis, points-to analysis