Java bytecode verification for secure information flow

ABSTRACT

Security of Java programs is important as they can be executed in different platforms. This paper addresses the problem of secure information flow for Java bytecode. In information flow analysis one wishes to check if high security data can ever propagate to low security observers. We propose a static analysis similar to the type-level abstract interpretation used for standard bytecode verification. Instead of types, our technique works with secrecy levels assigned to classes, methods' parameters and returned values, and handles implicit information flows. A verification tool based on the proposed technique is under development. Using the tool, programs downloaded from untrusted hosts can be checked locally prior to executing them.

REFERENCES

• 1: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 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: Thomas Ball, What's in a region?: or computing control dependence regions in near-linear time for reducible control flow, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.1-16, March–Dec. 1993 [doi>10.1145/176454.176456]
• 4: 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
• 5: R. Barbuti , C. Bernardeschi , N. De Francesco, Abstract interpretation of operational semantics for secure information flow, Information Processing Letters, v.83 n.2, p.101-108, 31 July 2002 [doi>10.1016/S0020-0190(02)00219-3]
• 6: Roberto Barbuti , Cinzia Bernardeschi , Nicoletta De Francesco, Checking security of Java bytecode by abstract interpretation, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain [doi>10.1145/508791.508839]
• 7: Cinzia Bernardeschi , Nicoletta De Francesco, Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode, Revised Papers from the Third International Workshop on Verification, Model Checking, and Abstract Interpretation, p.1-15, January 21-22, 2002
• 8: C. Bernardeschi, N. D. Francesco, and G. Lettieri. An abstract semantics tool for secure information flow of stack-based assembly programs. Microprocessors and Microsystems, 26(8):391--398, 2002.
• 9: Pierre Bieber , Jacques Cazin , Pierre Girard , Jean Louis Lanet , Virginie Wiels , Guy Zanon, Checking Secure Interactions of Smart Card Applets, Proceedings of the 6th European Symposium on Research in Computer Security, p.1-16, October 04-06, 2000
• 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: Xavier Leroy, Java Bytecode Verification: An Overview, Proceedings of the 13th International Conference on Computer Aided Verification, p.265-285, July 18-22, 2001
• 12: M. Mizuno and D. A. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing, 4:727--754, 1992.
• 13: Joachim Posegga , Harald Vogt, Byte Code Verification for Java Smart Card Based on Model Checking, Proceedings of the 5th European Symposium on Research in Computer Security, p.175-190, September 16-18, 1998
• 14: François Pottier , Sylvain Conchon, Information flow inference for free, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.46-57, September 2000
• 15: Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000 [doi>10.1145/363911.363915]
• 16: E. Rose and K. Rose. Lightweight bytecode verification. In WFUJ 98 Proceedings, 1998.
• 17: Andrei Sabelfeld , David Sands, A Per Model of Secure Information Flow in Sequential Programs, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.40-58, March 22-28, 1999
• 18: L. T. and F. Yellin. The Java virtual machine specification. Addison-Wesley Publishing Company, Reading, Massachusetts, 1996.
• 19: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 20: Steve Zdancewic , Andrew C. Myers, Secure Information Flow and CPS, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.46-61, April 02-06, 2001

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Validation

General Terms:
Languages, Security, Theory, Verification

Keywords:
Java bytecode, data protection, information flow, static analysis, verification tool