Resource bound certification
- 5 January 2000
- proceedings article
- Published by Association for Computing Machinery (ACM)
- p. 184-198
- https://doi.org/10.1145/325694.325716
Abstract
Various code certification systems allow the certification and static verification of important safety properties such as memory and control-flow safety. These systems are 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.Keywords
This publication has 16 references indexed in Scilit:
- Flexible type analysisPublished by Association for Computing Machinery (ACM) ,1999
- Recursion and dynamic data-structures in bounded spacePublished by Association for Computing Machinery (ACM) ,1999
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- Intensional polymorphism in type-erasure semanticsPublished by Association for Computing Machinery (ACM) ,1998
- Safe kernel extensions without run-time checkingPublished by Association for Computing Machinery (ACM) ,1996
- Extensibility safety and performance in the SPIN operating systemPublished by Association for Computing Machinery (ACM) ,1995
- Static dependent costs for estimating execution timePublished by Association for Computing Machinery (ACM) ,1994
- Efficient software-based fault isolationPublished by Association for Computing Machinery (ACM) ,1993
- Inductive types and type constraints in the second-order lambda calculusAnnals of Pure and Applied Logic, 1991
- Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des TypesPublished by Elsevier ,1971