JNI light: An operational model for the core JNI

Research output: Contribution to journalArticlepeer-review

2 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)805-840
Number of pages36
JournalMathematical Structures in Computer Science
Issue number4
StatePublished - May 9 2015

All Science Journal Classification (ASJC) codes

  • Mathematics (miscellaneous)
  • Computer Science Applications


Dive into the research topics of 'JNI light: An operational model for the core JNI'. Together they form a unique fingerprint.

Cite this