Various code certification systems allow the certification and static
verification of a variety of important safety properties such as memory safety
and control-flow safety. These systems provide valuable tools for verifying
that untrusted and potentially malicious code is safe before execution.
However, one important safety property that is not usually included is that
programs adhere to specific bounds on resource consumption, such as running
We present a decidable type system capable of specifying and certifying bounds
on resource consumption. Our system makes two advances over previous resource
bound certification systems, both of which are necessary for a practical
system: we allow the execution time of programs and their subroutines to
vary, depending on their arguments, and we provide a fully automatic compiler
generating certified executables from source-level programs. The principal
device in our approach is a strategy for simulating dependent types using sum
and inductive kinds.
(dvi, pdf, ps.gz)