Department of Computer Science
Cornell University
4pm Tuesday 29 April 2003
Room 2511, JCMB, King's Buildings
Our society is increasingly dependent upon its computing and communications infrastructure. Unfortunately, that infrastructure is built using unsafe, error-prone C and C++ code where buffer overruns, format string attacks, and space leaks are not only possible, but frighteningly common. Safe languages, such as Java, Scheme, or ML do not admit these attacks but relatively little infrastructure (i.e., operating systems, databases, protocols, etc.) is built using a safe language.
For the past two years, we have been exploring and building type systems for C code in the context of a project called Cyclone. The challenge is to find type systems and type inference techniques that are (a) sound, (b) scalable, (c) admit common idioms such as pointer arithmetic and manual memory management without losing the benefits that C provides for writing systems code (e.g., control over data representations.)