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, the impact of class initialization on information flow has been so far largely unexplored. This paper turns the spotlight on security implications of class initialization. We discuss the subtleties of information propagation when classes are initialized and propose a formalization that illustrates how to track information flow in presence of class initialization by a type-and-effect system for a simple language. We show how to extend the formalization to a language with exception handling.
Chapter PDF
References
Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 91–102 (2006)
Avvenuti, M., Bernardeschi, C., De Francesco, N.: Java bytecode verification for secure information flow. SIGPLAN Notices 38(12), 20–27 (2003)
Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, New York (1996)
Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 333–348. Springer, Heidelberg (2008)
Askarov, A., Sabelfeld, A.: Catch me if you can: Permissive yet secure error handling. In: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS) (June 2009)
Bieber, P., Cazin, J., Girard, P., Lanet, J.-L., Zanon, G.: Checking secure interactions of smart card applets: extended version. J. Computer Security 10(4), 369–398 (2002)
Bernardeschi, C., De Francesco, N., Lettieri, G., Martini, L.: Checking secure information flow in java bytecode by code transformation and standard bytecode verification. Software: Practice and Experience 34, 1225–1255 (2005)
Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. Journal of Functional Programming 15(2), 131–177 (2005)
Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)
Barthe, G., Rezk, T.: Non-interference for a jvm-like language. In: Proc. Types in Language Design and Implementation, pp. 103–112 (2005)
Barthe, G., Rezk, T., Naumann, D.: Deriving an information flow checker and certifying compiler for java. In: Proc. IEEE Symp. on Security and Privacy, pp. 230–242 (2006)
Barthe, G., Serpette, B.: Partial evaluation and non-interference for object calculi. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol. 1722, pp. 53–67. Springer, Heidelberg (1999)
Crockford, D.: Making javascript safe for advertising. adsafe.org (2009)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)
Denning, D.E.: A lattice model of secure information flow. Comm. of the ACM 19(5), 236–243 (1976)
Excalibur. Documentation and Software, http://excalibur.apache.org/index.html
Facebook. FBJS (2009), http://wiki.developers.facebook.com/index.php/FBJS
Gosling, J., Joy, B., Steele, G., Bracha, G.: The JavaTM Language Specification. Addison-Wesley, Reading (1996)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, April 1982, pp. 11–20 (1982)
Hedin, D., Sands, D.: Noninterference in the presence of non-opaque pointers. In: Proc. IEEE Computer Security Foundations Workshop, pp. 255–269 (2006)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive informationflow control based on program dependence graphs. International Journal of Information Security 8(6), 399–422 (2009); Supersedes ISSSE and ISoLA 2006
Kozen, D.: Language-based security. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 284–298. Springer, Heidelberg (1999)
Liang, S., Bracha, G.: Dynamics class loading in the Java virtual machine. In: Proc. ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, pp. 36–44 (1998)
Leroy, X.: Java bytecode verification: algorithms and formalizations. J. Automated Reasoning 30(3–4), 235–269 (2003)
Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
Miller, M., Samuel, M., Laurie, B., Awad, I., Stay, M.: Caja: Safe active content in sanitized javascript (2008)
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symp. on Principles of Programming Languages, January 1999, pp. 228–241 (1999)
Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow. Software release (2001– 2010), http://www.cs.cornell.edu/jif
Naumann, D.: From coupling relations to mated invariants for checking information flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 279–296. Springer, Heidelberg (2006)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM TOPLAS 25(1), 117–158 (2003)
Simonet, V.: The Flow Caml system. Software release (July 2003), http://cristal.inria.fr/~simonet/soft/flowcaml
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Schneider, F.B., Morrisett, G., Harper, R.: A language-based approach to security. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 86–101. Springer, Heidelberg (2001)
Java 2 platform, standard edition 5.0, API specification, http://java.sun.com/j2se/1.5.0/docs/api/
Praxis High Integrity Systems. Sparkada examinar. Software release (2010), http://www.praxis-his.com/sparkada
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)
Wallach, D.S., Appel, A.W., Felten, E.W.: The security architecture formerly known as stack inspection: A security mechanism for language-based systems. ACM Transactions on Software Engineering and Methodology 9(4), 341–378 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 IFIP
About this paper
Cite this paper
Nakata, K., Sabelfeld, A. (2010). Securing Class Initialization. In: Nishigaki, M., Jøsang, A., Murayama, Y., Marsh, S. (eds) Trust Management IV. IFIPTM 2010. IFIP Advances in Information and Communication Technology, vol 321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13446-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-13446-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13445-6
Online ISBN: 978-3-642-13446-3
eBook Packages: Computer ScienceComputer Science (R0)