When: Thursday, October 05, 12:00 p.m.

Where: 3305 Newell-Simon Hall

Jeff Foster, Assistant Professor, Computer Science Department and UMIACS
University of Maryland, College Park

Joint ISRI/POP Seminar

Abstract:
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 correct multilingual software.

Joint work with Mike Furr.

Jeff Foster is an Assistant Professor in the Department of Computer Science at the University of Maryland, College Park. He received his Ph.D. in Computer Science from the University of California, Berkeley. He is a recipient of the 2004 NSF CAREER award. Jeff's research focuses on programming languages with applications to software engineering and security. His recent research contributions include novel techniques to analyze software systems written in multiple languages; a new static analysis system for checking that network protocol implementations conform to specifications from standards documents; a type- and constraint-based system for finding data races in C programs; and the development of basic techniques for inferring type qualifiers and their application to program analysis.

Lunch provided.

<< Back