Wed Jul 26, 2006, 2:30-3:30pm, 4549 Boelter Hall

SAFECode: A Platform for Developing Reliable Software in Unsafe Languages

Vikram Adve
University of Illinois, Urbana-Champaign

A vast majority of current software is written in weakly typed  
languages such as C and C++. These unsafe languages provide very weak  
semantic guarantees due to the possibility of undetected memory  
errors such as dangling pointer references, array bounds overflow and  
arbitrary casting between types. This failing has two major  
implications.  First, systems written in these languages are  
vulnerable to security attacks. Second, most software analysis and  
verification tools assume the absence of memory errors and so cannot  
provide guarantees for software written in these languages.

In this talk, I will describe a compiler and runtime system called  
SAFECode that enables development of reliable software in unsafe  
languages.  SAFECode enables a class of sound analysis techniques for  
C and C++ programs (and also ensures memory safety) despite the  
possibility of undetected dangling pointer and array bounds  
violations, i.e., it renders such errors "harmless" from the  
viewpoint of sound analysis and memory safety.  I will present the  
main insights behind our approach and briefly discuss a formalization  
that we have used to prove soundness.  SAFECode also provides two new  
debugging techniques to detect all array bounds violations and all  
dangling pointer dereferences.  Both techniques are backwards- 
compatible, fully automatic, require no source changes, and have far  
lower overhead than previous comparable techniques (often low enough  
for production use).  Through the course of the talk, I will also  
show how a single, novel compiler transformation -- Automatic Pool  
Allocation -- is used by all three components of this work (sound  
analysis, array bounds, and dangling pointers) in three different ways.


About the speaker:
Vikram Adve is an Associate Professor of Computer Science at the  
University of Illinois at Urbana-Champaign. His research interests  
include compilers, security, and performance evaluation.  His  
research group has developed the LLVM Compiler Infrastructure, a  
widely distributed and novel compiler framework for 'lifelong'  
optimization of programs.  The group is using LLVM for several broad  
research projects, including "whole data structure" transformations,  
the SAFECode system for sound analysis and memory safety, and a  
compiler-based virtual-machine for operating system kernels.  Adve  
received a B.Tech. from I.I.T. Bombay in 1987, a Ph.D. in Computer  
Science from the University of Wisconsin-Madison in 1993, and was a  
Research Scientist at Rice University before joining the University  
of Illinois. He has received the NSF CAREER award, Best Paper Awards  
at PLDI 2005 and PADS 2001, and the UIUC Computer Science  
Department's Outstanding Junior Faculty Award. He is an Associate  
Editor of the ACM Transactions on Programming Languages and Systems  
(TOPLAS).

Hosts: Rajive Bagrodia and Jens Palsberg.