Reliable and secure software: practical type systems that prevent errors

The Faculty of Informatics is pleased to announce a seminar given by Werner Dietl

DATE: Monday, May 6th 2013
PLACE: USI Università della Svizzera italiana, room SI-006, Informatics building (Via G. Buffi 13)
TIME: 09.30

ABSTRACT:
The development of bug-free software is not only a challenging research question, but, more importantly, a very pressing societal need: bugs can cost time, money, privacy, and even lives. In this talk I present my work to improve software reliability and security in practical ways.  I have developed type systems for software reliability and security, and I have implemented tools to support the use and easy adoption of such advanced type systems.  Finally, I have applied my tools to practical problems and have established their benefits.
I have developed a simple and precise type system for mobile devices, which can make explicit the origin and destination of data.  Thus, it can flag any illegal flow of information, and it can address the security challenges of mobile devices, where, e.g. one would want to prevent the flow of personal data to the network.  In a competition run by DARPA, my toolset helped to identify malware in 50 applications written by an adversarial Red Team.
I have developed new type inference techniques to automatically find desirable type assignments.  Such type inference is key, because it will significantly ease the adoption of advanced type systems.  A key contribution of my work was the development of scoring functions that allow the selection of a best solution. In situations where no solutions exist, traditional type inference approaches give hard to comprehend error messages.  I am currently investigating how to identify the optimal fixes for such programs --- by crowd-sourcing a game that can be played by laypersons without knowledge of programming theory.
To ensure the practicality of my theoretical developments, I implemented a toolset that makes it easy to define custom type checkers and type inference approaches.  I have applied various type systems on several million lines of real-world source code.  I am working with Oracle to integrate my work into Java 8.

BIO:
Werner Dietl is a post-doctoral research associate at the University of Washington.  Previously, he was a research and teaching assistant at ETH Zurich, Switzerland.  He works on light-weight and sound type systems that provide compile-time guarantees about properties chosen by the developer.  He uses theoretical developments to improve the practice of real-world developers.  More information is available at his homepage, http://homes.cs.washington.edu/~wmdietl/.

HOST: Prof. Mauro Pezzè