Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-24T23:03:40.078Z Has data issue: false hasContentIssue false
  • English
  • Français

JNI light: an operational model for the core JNI

Published online by Cambridge University Press:  10 November 2014

GANG TAN
GANG TAN*
Affiliation:
Department of Computer Science and Engineering, Lehigh University, Bethlehem, Pennsylvania, U.S.A. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Through foreign function interfaces (FFIs), software components in different programming languages interact with each other in the same address space. Recent years have witnessed a number of systems that analyse FFIs for safety and reliability. However, lack of formal specifications of FFIs hampers progress in this endeavour. We present a formal operational model, Java Native Interface (JNI) light (JNIL), for a subset of a widely used FFI – the Java Native Interface (JNI). JNIL focuses on the core issues when a high-level garbage-collected language interacts with a low-level language. It proposes abstractions for handling a shared heap, cross-language method calls, cross-language exception handling, and garbage collection. JNIL can directly serve as a formal basis for JNI tools and systems. We demonstrate its utility by proving soundness of a system that checks native code in JNI programs for type-unsafe use of JNI functions. The abstractions in JNIL are also useful when modelling other FFIs, such as the Python/C interface and the OCaml/C interface.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 4: APLAS 2010 , May 2015 , pp. 805 - 840
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Bacon, D. F., Cheng, P. and Rajan, V. T. (2004) A unified theory of garbage collection. In: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), New York, ACM Press 50–68.Google Scholar
Czarnik, P. and Schubert, A. (2007) Extending operational semantics of the Java bytecode. In: Proceedings of Trustworth Global Computing 2007 57–72.Google Scholar
Drossopoulou, S. and Eisenbach, S. (1999) Describing the semantics of Java and proving type soundness. Formal Syntax and Semantics of Java. Springer-Verlag 41–82.Google Scholar
Flatt, M., Krishnamurthi, S. and Felleisen, M. (1999) A programmer's reduction semantics for classes and mixins. Formal Syntax and Semantics of Java. Springer-Verlag 241–269.Google Scholar
Freund, S. N. and Mitchell, J. (2003) A type system for the Java bytecode language and verifier. Journal of Automated Reasoning 30 (3–4)271–321.CrossRefGoogle Scholar
Furr, M. and Foster, J. (2006) Polymorphic type inference for the JNI. In: Proceedings of 15th European Symposium on Programming (ESOP) 309–324.Google Scholar
Furr, M. and Foster, J. (2008) Checking type safety of foreign function calls. ACM Transactions on Programming Languages and Systems 30 (4)1–63.Google Scholar
Gordon, A. D. and Syme, D. (2001) Typing a multi-language intermediate code. In: 28th ACM Symposium on Principles of Programming Languages (POPL) 248–260.CrossRefGoogle Scholar
Hirzel, M. and Grimm, R. (2007) Jeannie: Granting Java native interface developers their wishes. In: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) 19–38.CrossRefGoogle Scholar
Igarashi, A., Pierce, B. C. and Wadler, P. (2001) Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23 (3)396–450.Google Scholar
Klein, G. and Nipkow, T. (2006) A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems 28 (4)619–695.Google Scholar
Kondoh, G. and Onodera, T. (2008) Finding bugs in Java Native Interface programs. In: ISSTA'08: Proceedings of the 2008 International Symposium on Software Testing and Analysis, New York, NY, USA, ACM 109–118.Google Scholar
Lee, B., Hirzel, M., Grimm, R., Wiedermann, B. and McKinley, K. S. (2010) Jinn: Synthesizing a dynamic bug detector for foreign language interfaces. In: ACM Conference on Programming Language Design and Implementation (PLDI) 36–49.Google Scholar
Leroy, X. and Blazy, S. (2008) Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning 41 (1)1–31.Google Scholar
Li, S. and Tan, G. (2009) Finding bugs in exceptional situations of JNI programs. In: 16th ACM Conference on Computer and Communications Security (CCS) 442–452.Google Scholar
Liang, S. (1999) Java Native Interface: Programmer's Guide and Reference, Addison-Wesley Longman Publishing Co., Inc. ISBN 0201325772.Google Scholar
Lindholm, T. and Yellin, F. (1999) The Java Virtual Machine Specification, 2nd edition, Addison Wesley ISBN 0201432943.Google Scholar
Manson, J., Pugh, W. and Adve, S. V. (2005) The Java memory model. In: 32nd ACM Symposium on Principles of Programming Languages (POPL), New York, NY, USA, ACM 378–391.Google Scholar
Matthews, J. and Findler, R. B. (2007) Operational semantics for multi-language programs. In: 34th ACM Symposium on Principles of Programming Languages (POPL) 3–10.Google Scholar
McGraw, G. and Felten, E. W. (1999) Securing Java: Getting Down to Business with Mobile Code, John Wiley and Sons.Google Scholar
Moore, J. S. and Porter, G. (2002) The apprentice challenge. ACM Transactions on Programming Languages and Systems 24 (3)193–216.Google Scholar
Morrisett, G., Crary, K., Glew, N. and Walker, D. (2002) Stack-based typed assembly language. Journal of Functional Programming 12 (1)43–88.Google Scholar
Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B. and Gan, E. (2011) RockSalt: Better, faster, stronger SFI for the x86. submitted for conference publication, Technical report, Harvard University.Google Scholar
Necula, G., McPeak, S. and Weimer, W. (2002) CCured: Type-safe retrofitting of legacy code. In: 29th ACM Symposium on Principles of Programming Languages (POPL) 128–139.CrossRefGoogle Scholar
Petri, G. and Huisman, M. (2008) BicolanoMT: A formalization of multi-threaded Java at bytecode level. In: Bytecode 2008.Google Scholar
Pichardie, D. (2006) Bicolano – byte code language in Coq. Available at http://mobius.inria.fr/bicolano.Google Scholar
Pucella, R. (2002) Towards a formalization for COM, part I: The primitive calculus. In: ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), New York, ACM Press 331–342.Google Scholar
Siefers, J., Tan, G. and Morrisett, G. (2010) Robusta: Taming the native beast of the JVM. In: 17th ACM Conference on Computer and Communications Security (CCS) 201–211.Google Scholar
Tan, G. (2010) JNI Light: An operational model for the core JNI. In: Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS '10) 114–130.Google Scholar
Tan, G. and Croft, J. (2008) An empirical security study of the native code in the JDK. In: 17th Usenix Security Symposium 365–377.Google Scholar
Tan, G. and Morrisett, G. (2007) ILEA: Inter-language analysis across Java and C. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) 39–56.CrossRefGoogle Scholar
Tan, G., Appel, A., Chakradhar, S., Raghunathan, A., Ravi, S. and Wang, D. (2006) Safe Java native interface. In: Proceedings of IEEE International Symposium on Secure Software Engineering 97–106.Google Scholar
Trifonov, V. and Shao, Z. (1999) Safe and principled language interoperation. In: 8th European Symposium on Programming (ESOP) 128–146.Google Scholar