Joint ISR/POP Seminar

Thursday, October 5, noon
Newell Simon Hall 3305

lunch will be provided


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

Joint work with Mike Furr


Bio:

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.