JNI light: an operational model for the core JNI

摘要

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