C. Joseph Vanderwaart

Static Enforcement of Timing Policies Using Code Certification Degree Type: Ph.D. in Computer Science
Advisor(s): Karl Crary
Graduated: August 2006

Abstract:

Explicit or implicit, enforced or not, safety policies are ubiquitous in software systems. In the many settings where third-party software is executed in the context of a larger client program, the supervisor usually enforces a safety policy that prevents the foreign code from behaving in ways that would disrupt the client, corrupt data or destabilize the system. Certified code provides a static means for controlling the behavior of untrusted programs or components by bringing the power of type systems and formal logic to bear on the problem. Code certification systems that prevent bad memory accesses and enforce the abstractions provided by libraries and runtime system interfaces have been well studied.

This thesis presents a system for certifying conformance to timing requirements. The approach is simple, comprising an incremental change to an existing type system for assembly language, but flexible in the set of policies it can enforce. Moreover, in principle, it can be extended to support arbitrarily complex coding idioms. Focusing on a particular timing policy of interest, I describe a compiler that produces certifiably compliant programs with no help from the programmer and only a small impact on runtime performance. Later, I discuss the applicability of both the type system and the compilation techniques to other timing and resource control problems.

Thesis Committee:
Karl Crary (chair)
Robert Haper
Peter Lee
Stephanie Weirich (University of Pennsylvania)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Type systems, type theory, typed assembly language, certified code, certifying compilation, type safety, timing, responsiveness, liveness, resource management