The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - Jan.-Feb. (2013 vol.10)
pp: 1-13
Willard Rafnsson , Chalmers University of Technology, Göteborg
Keiko Nakata , Tallinn University of Technology, Tallinn
Andrei Sabelfeld , Chalmers University of Technology, Göteborg
ABSTRACT
Language-based information-flow security is concerned with specifying and enforcing security policies for information flow via language constructs. Although much progress has been made on understanding information flow in object-oriented programs, little attention has been given to the impact of class initialization on information flow. This paper turns the spotlight on security implications of class initialization. We reveal the subtleties of information propagation when classes are initialized, and demonstrate how these flows can be exploited to leak information through error recovery. Our main contribution is a type-and-effect system which tracks these information flows. The type system is parameterized by an arbitrary lattice of security levels. Flows through the class hierarchy and dependencies in field initializers are tracked by typing class initializers wherever they could be executed. The contexts in which each class can be initialized are tracked to prevent insecure flows of out-of-scope contextual information through class initialization statuses and error recovery. We show that the type system enforces termination-insensitive noninterference.
INDEX TERMS
Security, Java, Context, Lattices, Loading, Syntactics, Semantics, program analysis, Information flow control
CITATION
Willard Rafnsson, Keiko Nakata, Andrei Sabelfeld, "Securing Class Initialization in Java-like Languages", IEEE Transactions on Dependable and Secure Computing, vol.10, no. 1, pp. 1-13, Jan.-Feb. 2013, doi:10.1109/TDSC.2012.73
REFERENCES
[1] T. Amtoft, S. Bandhakavi, and A. Banerjee, "A Logic for Information Flow in Object-Oriented Programs," Proc. ACM Symp. Principles of Programming Languages, pp. 91-102, 2006.
[2] M. Avvenuti, C. Bernardeschi, and N. De Francesco, "Java Bytecode Verification for Secure Information Flow," SIGPLAN Notices, vol. 38, no. 12, pp. 20-27, 2003.
[3] M. Abadi and L. Cardelli, A Theory of Objects (Monographs in Computer Science). Springer-Verlag, 1996.
[4] A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands, "Termination-Insensitive Noninterference Leaks More than Just a Bit," Proc. European Symp. Research in Computer Security, pp. 333-348, Oct. 2008.
[5] A. Askarov and A. Sabelfeld, "Catch Me if You Can: Permissive Yet Secure Error Handling," Proc. ACM Workshop Programming Languages and Analysis for Security (PLAS), June 2009.
[6] P. Bieber, J. Cazin, P. Girard, J.-L. Lanet, and G. Zanon, "Checking Secure Interactions of Smart Card Applets: Extended Version," J. Computer Security, vol. 10, no. 4, pp. 369-398, 2002.
[7] C. Bernardeschi, N. De Francesco, G. Lettieri, and L. Martini, "Checking Secure Information Flow in Java Bytecode by Code Transformation and Standard Bytecode Verification," Software: Practice and Experience, vol. 34, pp. 1225-1255, 2005.
[8] B. Pugh et al., "The "Double-Checked Locking Is Broken" Declaration," http://www.cs.umd.edu/~pugh/java/memory Model DoubleCheckedLocking.html, 2012.
[9] A. Banerjee and D.A. Naumann, "Stack-Based Access Control and Secure Information Flow," J. Functional Programming, vol. 15, no. 2, pp. 131-177, Mar. 2005.
[10] G. Barthe, D. Pichardie, and T. Rezk, "A Certified Lightweight Non-Interference Java Bytecode Verifier," Proc. European Symp. Programming, 2007.
[11] G. Barthe and T. Rezk, "Non-Interference for a Jvm-Like Language," Proc. ACM SIGPLAN Int'l Workshop Types in Language Design and Implementation, pp. 103-112, 2005.
[12] G. Barthe, T. Rezk, and D. Naumann, "Deriving an Information Flow Checker and Certifying Compiler for Java," Proc. IEEE Symp. Security and Privacy, pp. 230-242, 2006.
[13] G. Barthe and B. Serpette, "Partial Evaluation and Non-Interference for Object Calculi," Proc. Fuji Int'l Symp. Functional and Logic Programming (FLOPS), pp. 53-67, Nov. 1999.
[14] D. Crockford, "Making Javascript Safe for Advertising," www.adsafe.org, 2009.
[15] D.E. Denning and P.J. Denning, "Certification of Programs for Secure Information Flow," Comm. ACM, vol. 20, no. 7, pp. 504-513, July 1977.
[16] D.E. Denning, "A Lattice Model of Secure Information Flow," Comm. ACM, vol. 19, no. 5, pp. 236-243, May 1976.
[17] Excalibur. Documentation and Software http://excalibur.apache. orgindex.html, 2012.
[18] Facebook, FBJS, http://wiki.developers.facebook.com/index. php FBJS, 2009.
[19] J. Gosling, B. Joy, and G. Steele, The Java Language Specification. Addison-Wesley, Aug. 1996.
[20] J.A. Goguen and J. Meseguer, "Security Policies and Security Models," Proc. IEEE Symp. Security and Privacy, pp. 11-20, Apr. 1982.
[21] D. Hedin and D. Sands, "Noninterference in the Presence of Non-Opaque Pointers," Proc. IEEE Computer Security Foundations Workshop, pp. 255-269, 2006.
[22] C. Hammer and G. Snelting, "Flow-Sensitive, Context-Sensitive, and Object-Sensitive Information Flow Control Based on Program Dependence Graphs," Int'l J. Information Security, vol. 8, no. 6, pp. 399-422, Oct. 2009.
[23] D. Kozen, "Language-Based Security," Proc. Conf. Math. Foundations of Computer Science, pp. 284-298, Sept. 1999.
[24] S. Liang and G. Bracha, "Dynamics Class Loading in the Java Virtual Machine," Proc. ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages & Applications, pp. 36-44, 1998.
[25] X. Leroy, "Java Bytecode Verification: Algorithms and Formalizations," J. Automated Reasoning, vol. 30, nos. 3/4, pp. 235-269, 2003.
[26] T. Lindholm and F. Yellin, The Java Virtual Machine Specification, second ed. Addison-Wesley, 1999.
[27] M. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay, "Caja: Safe Active Content in Sanitized Javascript," 2008.
[28] A.C. Myers, "JFlow: Practical Mostly-Static Information Flow Control," Proc. ACM Symp. Principles of Programming Languages, pp. 228-241, Jan. 1999.
[29] A.C. Myers, L. Zheng, S. Zdancewic, S. Chong, and N. Nystrom, "Jif: Java Information Flow," Software, http://www.cs.cornell. edujif, 2010.
[30] D. Naumann, "From Coupling Relations to Mated Invariants for Checking Information Flow," Proc. European Symp. Research in Computer Security, pp. 279-296, 2006.
[31] K. Nakata and A. Sabelfeld, "Securing Class Initialization," Proc. IFIP Int'l Conf. Trust Management (IFIPTM), June 2010.
[32] F. Pottier and V. Simonet, "Information Flow Inference for ML," ACM Trans. Programming Languages and Systems, vol. 25, no. 1, pp. 117-158, Jan. 2003.
[33] W. Rafnsson, K. Nakata, and A. Sabelfeld, "Secure Class Initialization," technical report, Chalmers Univ. of Technology, http://www.cse.chalmers.se/rafnsson2011TDSC , 2011.
[34] C.D. Schmidt and T. Harrison, "Double-Checked Locking," Pattern Languages of Program Design 3, R.C. Martin, D. Riehle, and F. Buschmann, eds., pp. 363-375, Addison-Wesley Longman Publishing Co., Inc., 1997.
[35] V. Simonet, "The Flow Caml System," Software, http://cristal. inria.fr/~simonet/softflowcaml , July 2003.
[36] A. Sabelfeld and A.C. Myers, "Language-Based Information-Flow Security," IEEE J. Selected Areas in Comm., vol. 21, no. 1, pp. 5-19, Jan. 2003.
[37] F.B. Schneider, G. Morrisett, and R. Harper, "A Language-Based Approach to Security," Proc. Informatics—10 Years Back, 10 Years Ahead, pp. 86-101, 2000.
[38] Java 2 Platform, Standard ed. 5.0, API Specification, http://java.sun.com/j2se/1.5.0/docsapi/, 2012.
[39] Praxis High Integrity Systems, "Sparkada Examinar," Software, http://www.praxis-his.comsparkada/, 2010.
[40] D. Volpano, G. Smith, and C. Irvine, "A Sound Type System for Secure Flow Analysis," J. Computer Security, vol. 4, no. 3, pp. 167-187, 1996.
[41] D.S. Wallach, A.W. Appel, and E.W. Felten, "The Security Architecture Formerly Known as Stack Inspection: A Security Mechanism for Language-Based Systems," ACM Trans. Software Eng. and Methodology, vol. 9, no. 4, pp. 341-378, Oct. 2000.
[42] M. Warnier, "Language Based Security for Java and JML," PhD thesis, Radboud Univ., Nijmegen, Netherlands, 2006.
29 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool