[Prev][Next][Index][Thread]

Paper Announcement: Resource Bound Certification

I'd like to announce the availability of the following paper (which
will appear in POPL '00):

Resource Bound Certification
Karl Crary and Stephanie Weirich

This paper is available at the following web sites:
http://www.cs.cmu.edu/afs/cs/user/crary/www/papers/
http://www.cs.cornell.edu/talc/papers.html

Thanks,
Stephanie Weirich

ABSTRACT
------------------------------------------------------------------------

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 time.

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.