Karl Crary
Stephnie Weirich
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.
- 1.B. Bershad, S. Savage, P. Pardyak, E. Sirer, M. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In Fifteenth A CM Symposium on Operating Systems Principles, pages 267-284, Copper Mountain, Dec. 1995.]] Google Scholar
Digital Library
- 2.K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Twenty-Sixth A CM Symposium on Principles of Programming Languages, San Antonio, Texas, Jan. 1999.]] Google ScholarDigital Library
- 3.K. Crary and S. Weirich. Flexible type analysis. In 1999 A CM International Conference on Functional Programming, pages 233-248, Paris, Sept. 1999.]] Google ScholarDigital Library
- 4.K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In 1998 A CM International Conference on Functional Programming, pages 301- 312, Baltimore, Sept. 1998. Extended version published as Cornell University technical report TR98-1721.]] Google ScholarDigital Library
- 5.J.-Y. Girard. Une extension de l'interpr~tation de GSdel l'analyse, et son application ~ l'~limination de coupures dons l'analyse et la th~orie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63-92. North-Holland Publishing Co., 1971.]]Google ScholarCross Ref
- 6.J.-Y. Girard. Interprdtation fonctionelle et dlimination des coupures de l'arithm~tique d'ordre sup~rieur. PhD thesis, Universit~ Paris VII, 1972.]]Google Scholar
- 7.R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. :in Twenty-Second A CM Symposium on Principles of Programming Languages, pages 130- 1211, San Francisco, Jan. 1995.]] Google ScholarDigital Library
- 8.M. Hoffman. Linear types and non-size increasing polynomial time computation. In Fourteenth IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999.]] Google ScholarDigital Library
- 9.J. Hughes and L. Pareto. Recursion and dynamic datastructures in bounded space: Towards embedded ML programming. In 19P9 A CM international Conference on Functional Programming, pages 70-81, Paris, Sept. 1999.]] Google ScholarDigital Library
- 10.J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Twenty- Third A CM Symposium on Principles of Programming Languages, pages 410-423, St. Petersburg, Florida, Jan. 1996.]] Google ScholarDigital Library
- 11.T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.]] Google ScholarDigital Library
- 12.N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159-172, 1991.]]Google ScholarCross Ref
- 13.G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support .for System Software, Atlanta, May 1999.]]Google Scholar
- 14.G. Morrisett, D. Walker, K. Crary, aad N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 1999. To appear. An earlier version appeared in the 1998 Symposium on Principles of Programming Languages.]] Google ScholarDigital Library
- 15.G. Necula. Proof-carrying code. In Twenty-Fourth A CM Symposium on Principles of Programming Languages, pages 106-119, Paris, Jan. 1997.]] Google ScholarDigital Library
- 16.G. Necula and P. Lee. Safe kernel extensions without runtime checking. In Second Symposium on Operating Systems Design and Implementation, pages 229-243, Seattle, Oct. 1996.]] Google ScholarDigital Library
- 17.G. Necula and P. Lee. Safe, untrusted agents using proofcarrying code. In Special Issue on Mobile Agent Security, volume 1419 of Lecture Notes in Computer Science. Springer-Verlag, Oct. 1997.]] Google ScholarDigital Library
- 18.G. Necula and P. Lee. The design and implementation of a certifying compiler. In 1998 SIGPLAN Conference on Programming Language Design and Implementation, pages 333-344, Montreal, June 1998.]] Google ScholarDigital Library
- 19.B. Reistad and D. K. Gifford. Static dependent costs for estimating execution time. In 19g~ A CM Conference on Lisp and Functional Programming, pages 65-78, Orlando, Florida, June 1994.]] Google ScholarDigital Library
- 20.R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In Fourteenth A CM Symposium on Operating Systems Principles, pages 203- 216, Asheville, Dec. 1993.]] Google ScholarDigital Library
- 21.H. Xi and F. Pfenning. Dependent types in practical programming. In Twenty-Sizth A CM Symposium on Principles of Programming Languages, pages 214-227, San Antonio, Texas, Jan. 1999.]] Google ScholarDigital Library
Index Terms
- Resource bound certification
Comments