Checking type safety of foreign function calls

ABSTRACT

Foreign function interfaces (FFIs) allow components in different languages to communicate directly with each other. While FFIs are useful, they often require writing tricky low-level code and include little or no static safety checking, thus providing a rich source of hard-to-find programming errors. In this article, we study the problem of enforcing type safety across the OCaml-to-C FFI and the Java Native Interface (JNI). We present O-Saffire and J-Saffire, a pair of multilingual type inference systems that ensure C code that uses these FFIs accesses high-level data safely. Our inference systems use representational types to model C's low-level view of OCaml and Java values, and singleton types to track integers, strings, memory offsets, and type tags through C. J-Saffire, our Java system, uses a polymorphic flow-insensitive, unification-based analysis. Polymorphism is important because it allows us to precisely model user-defined wrapper functions and the more than 200 JNI functions. O-Saffire, our OCaml system, uses a monomorphic flow-sensitive analysis because, while polymorphism is much less important for the OCaml FFI flow-sensitivity is critical to track conditional branches, which are used when pattern matching OCaml data in C. O-Saffire also tracks garbage collection information to ensure that local C pointers to the OCaml heap are registered properly, which is not necessary for the JNI. We have applied O-Saffire and J-Saffire to a set of benchmarks and found many bugs and questionable coding practices. These results suggest that static checking of FFIs can be a valuable tool in writing correct multilingual software.

REFERENCES

• 1: Mockingbird: Flexible Stub Compilation from Pairs of Declarations, Proceedings of the 19th IEEE International Conference on Distributed Computing Systems, p.393, May 31-June 04, 1999
• 2: Daniel Jay Barrett , Jack C. Wileden, Polylingual systems: an approach to seamless interoperability, University of Massachusetts Amherst, 1998
• 3: David M. Beazley, SWIG: an easy to use tool for integrating scripting languages with C and C++, Proceedings of the 4th conference on USENIX Tcl/Tk Workshop, 1996, p.15-15, July 10-13, 1996, Monterey, California
• 4: Blume, M. 2001. No-longer-foreign: Teaching an ML compiler to speak C “natively”. In Proceedings of the 1st International Workshop on Multilanguage Infrastructure and Interoperability (BABEL'01). Firenze, Italy.
• 5: Alan Kaplan , John Bubba , Jack C. Wileden, The Exu Approach to Safe, Transparent and Lightweight Interoperability, Proceedings of the 25th International Computer Software and Applications Conference on Invigorating Software Development, p.393-394, October 08-12, 2001
• 6: Cannasse, N. 2004. Ocaml javalib. http://team.motion-twin.com/ncannasse/javaLib/.
• 7: Satish Chandra , Thomas Reps, Physical type checking for C, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.66-75, September 06-06, 1999, Toulouse, France
• 8: Christensen, A. S., Møller, A., and Schwartzbach, M. I. 2003. Precise analysis of string expressions. In Proceedings of the 10th International Symposium on Static Analysis. San Diego, CA.
• 9: DeLine, R. and Fähndrich, M. 2004. The Fugue protocol checker: Is your software baroque? Tech. rep. MSR-TR-2004-07, Microsoft Research.
• 10: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 12: Sigbjorn Finne , Daan Leijen , Erik Meijer , Simon Peyton Jones, Calling hell from heaven and heaven from hell, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.114-125, September 27-29, 1999, Paris, France
• 13: Fisher, K., Pucella, R., and Reppy, J. 2001. A framework for interoperability. In Proceedings of the 1st International Workshop on Multilanguage Infrastructure and Interoperability (BABEL'01). Firenze, Italy.
• 14: Michael Furr , Jeffrey S. Foster, Checking type safety of foreign function calls, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 15: Furr, M. and Foster, J. S. 2005b. Java SE 6 “Mustang” bug 6362203. http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=6362203.
• 16: Furr, M. and Foster, J. S. 2006a. Checking type safety of foreign function calls. Tech. rep. CS-TR-4845, Computer Science Department, University of Maryland.
• 17: Furr, M. and Foster, J. S. 2006b. Polymorphic type inference for the JNI. In Proceedings of the 15th European Symposium on Programming. Vienna, Austria. To appear.
• 18: Carl Gould , Zhendong Su , Premkumar Devanbu, Static Checking of Dynamically Generated Queries in Database Applications, Proceedings of the 26th International Conference on Software Engineering, p.645-654, May 23-28, 2004
• 19: David N. Gray , John Hotchkiss , Seth LaForge , Andrew Shalit , Toby Weinberg, Modern languages and Microsoft's component object model, Communications of the ACM, v.41 n.5, p.55-65, May 1998 [doi>10.1145/274946.274957]
• 20: Mark Grechanik , Don Batory , Dewayne E. Perry, Design of Large-Scale Polylingual Systems, Proceedings of the 26th International Conference on Software Engineering, p.357-366, May 23-28, 2004
• 21: Jennifer Hamilton, Interlanguage object sharing with SOM, Proceedings of the 2nd conference on USENIX Conference on Object-Oriented Technologies (COOTS), p.4-4, June 17-21, 1996, Toronto, Ontario, Canada
• 22: Jennifer Hamilton, Language integration in the common language runtime, ACM SIGPLAN Notices, v.38 n.2, February 2003 [doi>10.1145/772970.772973]
• 23: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 24: Huelsbergen, L. 1996. A portable C interface for standard ML of New Jersey. http://www.smlnj.org//doc/SMLNJ-C/smlnj-c.ps.
• 25: Java-Gnome Developers. 2005. Java bindings for the gnome and gtk libraries. http://java-gnome.sourceforge.net.
• 26: Jones, S. P. 2001. Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In Engineernig Theories of Software Construction, T. Hoare, M. Broy, and R. Steinbruggen, Eds. IOS Press, 47--96.
• 27: Leroy, X. 2004. The Objective Caml system. Release 3.08, http://caml.inria.fr/distrib/ocaml-3.08/ocaml-3.08-refman.pdf.
• 28: Sheng Liang, Java Native Interface: Programmer's Guide and Reference, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 29: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 30: Jacob Matthews , Robert Bruce Findler, Operational semantics for multi-language programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 31: Erik Meijer , Nigel Perry , Arjan van Yzendoorn, Scripting .NET Using Mondrian, Proceedings of the 15th European Conference on Object-Oriented Programming, p.150-164, June 18-22, 2001
• 32: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 33: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 34: Susumu Nishimura, Static typing for dynamic messages, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-278, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268968]
• 35: Object Management Group 2004. Common object request broker architecture: Core specification, Version 3.0.3. Object Management Group.
• 36: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 37: Tan, G., Appel, A. W., Chakradhar, S., Raghunathan, A., Ravi, S., and Wang, D. 2006. Safe java native interface. In Proceedings of the IEEE International Symposium on Secure Software Engineering. Arlington, VA.
• 38: Peter Thiemann, Grammar-based analysis of string expressions, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.59-70, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040300]
• 39: Valery Trifonov , Zhong Shao, Safe and Principled Language Interoperation, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.128-146, March 22-28, 1999
• 40: Andrew K. Wright , Robert Cartwright, A practical soft type system for Scheme, Proceedings of the 1994 ACM conference on LISP and functional programming, p.250-262, June 27-29, 1994, Orlando, Florida, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
FFI, Foreign function interface, JNI, Java, Java Native Interface, OCaml, dataflow analysis, flow-sensitive type system, foreign function calls, multilingual type inference, multilingual type system, representational type