This report describes a type theory for certified code, called TALT-R, in which type safety guarantees cooperation with a mechanism to limit the CPU usage of untrusted code. At its core is the foundational typed assembly language TALT, extended with an instruction-counting mechanism, or "virtual clock", intended to bound the number of non-yielding instructions a program may execute in a row. The type theory also contains a form of dependent refinement that allows reasoning about integer values to be reflected in the typing of a program; in particular, the refinement system enables a simple but effective dynamic checking scheme for the clock, which we predict will greatly improve the performance of TALT-R programs. We exhibit a translation from a clock-ignorant source language into a form of TALT-R, demonstrating that the type system is expressive enough to write general programs in.

62 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu