{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T15:56:18Z","timestamp":1649174178762},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,5]]},"abstract":"<jats:p>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 \u2013 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.<\/jats:p>","DOI":"10.1017\/s0960129513000042","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T11:41:16Z","timestamp":1415619676000},"page":"805-840","source":"Crossref","is-referenced-by-count":1,"title":["JNI light: an operational model for the core JNI"],"prefix":"10.1017","volume":"25","author":[{"given":"GANG","family":"TAN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129513000042_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1377492.1377493"},{"key":"S0960129513000042_ref1","first-page":"50","volume-title":"ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","author":"Bacon","year":"2004"},{"key":"S0960129513000042_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48737-9_7"},{"key":"S0960129513000042_ref30","unstructured":"Tan G. and Croft J. (2008) An empirical security study of the native code in the JDK. In: 17th Usenix Security Symposium 365\u2013377."},{"key":"S0960129513000042_ref26","unstructured":"Pichardie D. (2006) Bicolano \u2013 byte code language in Coq. Available at http:\/\/mobius.inria.fr\/bicolano."},{"key":"S0960129513000042_ref24","doi-asserted-by":"crossref","unstructured":"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\u2013139.","DOI":"10.1145\/503272.503286"},{"key":"S0960129513000042_ref32","unstructured":"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\u2013106."},{"key":"S0960129513000042_ref29","doi-asserted-by":"crossref","unstructured":"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\u2013130.","DOI":"10.1007\/978-3-642-17164-2_9"},{"key":"S0960129513000042_ref16","volume-title":"Java Native Interface: Programmer's Guide and Reference","author":"Liang","year":"1999"},{"key":"S0960129513000042_ref27","first-page":"331","volume-title":"ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","author":"Pucella","year":"2002"},{"key":"S0960129513000042_ref15","doi-asserted-by":"crossref","unstructured":"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\u2013452.","DOI":"10.1145\/1653662.1653716"},{"key":"S0960129513000042_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004178"},{"key":"S0960129513000042_ref19","doi-asserted-by":"crossref","unstructured":"Matthews J. and Findler R. B. (2007) Operational semantics for multi-language programs. In: 34th ACM Symposium on Principles of Programming Languages (POPL) 3\u201310.","DOI":"10.1145\/1190216.1190220"},{"key":"S0960129513000042_ref5","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025011624925"},{"key":"S0960129513000042_ref20","volume-title":"Securing Java: Getting Down to Business with Mobile Code","author":"McGraw","year":"1999"},{"key":"S0960129513000042_ref23","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/2254064.2254111"},{"key":"S0960129513000042_ref18","first-page":"378","volume-title":"32nd ACM Symposium on Principles of Programming Languages (POPL)","author":"Manson","year":"2005"},{"key":"S0960129513000042_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360228"},{"key":"S0960129513000042_ref17","volume-title":"The Java Virtual Machine Specification","author":"Lindholm","year":"1999"},{"key":"S0960129513000042_ref28","doi-asserted-by":"crossref","unstructured":"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\u2013211.","DOI":"10.1145\/1866307.1866331"},{"key":"S0960129513000042_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514189"},{"key":"S0960129513000042_ref25","unstructured":"Petri G. and Huisman M. (2008) BicolanoMT: A formalization of multi-threaded Java at bytecode level. In: Bytecode 2008."},{"key":"S0960129513000042_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390645"},{"key":"S0960129513000042_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"S0960129513000042_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48737-9_2"},{"key":"S0960129513000042_ref9","doi-asserted-by":"crossref","unstructured":"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\u201338.","DOI":"10.1145\/1297027.1297030"},{"key":"S0960129513000042_ref2","unstructured":"Czarnik P. and Schubert A. (2007) Extending operational semantics of the Java bytecode. In: Proceedings of Trustworth Global Computing 2007 57\u201372."},{"key":"S0960129513000042_ref13","doi-asserted-by":"crossref","unstructured":"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\u201349.","DOI":"10.1145\/1806596.1806601"},{"key":"S0960129513000042_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"S0960129513000042_ref33","unstructured":"Trifonov V. and Shao Z. (1999) Safe and principled language interoperation. In: 8th European Symposium on Programming (ESOP) 128\u2013146."},{"key":"S0960129513000042_ref31","doi-asserted-by":"crossref","unstructured":"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\u201356.","DOI":"10.1145\/1297027.1297031"},{"key":"S0960129513000042_ref6","doi-asserted-by":"crossref","unstructured":"Furr M. and Foster J. (2006) Polymorphic type inference for the JNI. In: Proceedings of 15th European Symposium on Programming (ESOP) 309\u2013324.","DOI":"10.1007\/11693024_21"},{"key":"S0960129513000042_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T05:39:53Z","timestamp":1566020393000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000042\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["S0960129513000042"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000042","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}