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 <jmlucas@cs.cmu.edu>
Thursday, October 5, 2006
12:00 p.m.
Newell-Simon
Hall 3305