Type-based information flow analysis for bytecode languages with variable object field policies

ABSTRACT

Static, type-based information flow analysis techniques targeted at Java and JVM-like code typically assume a global security policy on object fields: all fields are assigned a fixed security level. In essence they are treated as standard variables. However different objects may be created under varying security contexts, particularly for widely used classes such as wrapper or collection classes. This entails an important loss in precision of the analysis. We present a flow-sensitive type system for statically detecting illegal flows of information in a JVM-like language that allows the level of a field to vary at different object creation points. Also, we prove a noninterference result for this language.

REFERENCES

• 1: Anindya Banerjee , David A. Naumann, Secure Information Flow and Pointer Confinement in a Java-like Language, Proceedings of the 15th IEEE workshop on Computer Security Foundations, p.253, June 24-26, 2002
• 2: Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005 [doi>10.1017/S0956796804005453]
• 3: Gilles Barthe , Tamara Rezk , Amitabh Basu, Security types preserving compilation, Computer Languages, Systems and Structures, v.33 n.2, p.35-59, July, 2007 [doi>10.1016/j.cl.2005.05.002]
• 4: G. Barthe, D. Pichardie, and T. Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc. of ESOP'01, volume 4421 of LNCS. Springer-Verlag, 2007.
• 5: Gilles Barthe , Tamara Rezk, Non-interference for a JVM-like language, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.103-112, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040304]
• 6: Gilles Barthe , Tamara Rezk , David Naumann, Deriving an Information Flow Checker and Certifying Compiler for Java, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.230-242, May 21-24, 2006 [doi>10.1109/SP.2006.13]
• 7: G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld. Security of multithreaded programs by compilation. In Proc. of the 12th ESORICS, LNCS. Springer-Verlag, 2007. To appear.
• 8: F. Bavera and E. Bonelli. www.lifia.info.unlp.edu.ar/~eduardo/publications/jvmsLong.pdf, 2007.
• 9: J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy, pages 11--20, April, 1982.
• 10: Xavier Leroy, Bytecode verification on Java smart cards, Software—Practice & Experience, v.32 n.4, p.319-340, 10 April 2002 [doi>10.1002/spe.438]
• 11: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 12: A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
• 13: 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

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

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

General Terms:
Design, Management, Verification