Computer Science

Colloquium Details

Automated and Certified Conformance to Responsiveness Policies for Untrusted Mobile Code

Abstract

Certified code is a powerful technique for mitigating the security risks associated with running code from untrusted sources on a computer. In order to be practical, code certification must be able to address a wide range of safety concerns in addition to the usual baseline of type safety. In this talk, I will describe a desirable safety criterion called "responsiveness", related to the problem of bounding CPU usage, and a type system called TALT-R that I developed to certify programs that satisfy it. I will address the issue of how to compile programs written in a general-purpose source language into TALT-R, ensuring that they comply with the responsiveness policy without programmer assistance. Finally, I will argue that the concepts underlying TALT-R can be applied to other timing policies, and to the management of resources other than time.

Biography

Joseph Vanderwaart is a Computer Science Ph.D. candidate at Carnegie Mellon University. He received his B.A., Summa Cum Laude from Williams College in Computer Science and Mathematics. His research interests are programming languages; especially type theory, typed compilation and certified code.