Jeff Foster
University of Maryland

Checking Type Safety of Foreign Function Calls


Foreign function interfaces (FFIs) provide support for writing multilingual software, in which components in different languages communicate directly with each other.  While FFIs are extremely useful, they often require writing tricky, low-level code and include little or no static safety checking, providing a rich source of difficult-to-find programming errors.

In this talk, I will present recent work on Saffire (Static Analysis of Foreign Function InteRfacEs), a pair of tools that enforce type safety across the OCaml-to-C FFI and the Java Native Interface (JNI), which connects Java to C.  Saffire uses novel constraint-based type inference algorithms to analyze multilingual programs and ensure that the C code, which does most of the work in these two FFIs, accesses high-level data and functions at the right types.  Our type inference algorithms have three novel components: they use special representational types to model C's low-level view of high-level data; they precisely track data values such as integers and strings, in order to correctly model data accesses by the C code; and they incorporate flow-sensitivity or polymorphism to accurately model particular FFI features.

We have developed two tools, O-Saffire for OCaml, and J-Saffire for Java, and applied them to a number of benchmarks.  We found many bugs and questionable coding practices in our experiments, suggesting that static checking of FFIs can be a valuable tool in writing correctmultilingual software.

Joint work with Mike Furr

Host:  Jonathan Aldrich
Appointments:  Jennifer Lucas <>

Thursday, October 5, 2006
12:00 p.m.
Newell-Simon Hall 3305

Principles of Programming Seminars