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.

157 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]