Skip to main content
SpringerLink
Log in

Scalable Certification for Typed Assembly Language

  • Conference paper
  • First Online:
Types in Compilation (TIC 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2071))

Included in the following conference series:

Abstract

A type-based certifying compiler maps source code to machine code and target-level type annotations. The target-level annotations make it possible to prove easily that the machine code is type-safe, independent of the source code or compiler. To be useful across a range of source languages and compilers, the target-language type system should provide powerful type constructors for encoding higher-level invariants. Unfortunately, it is difficult to engineer such type systems so that annotation sizes are small and verification times are fast. In this paper, we describe our experience writing a certifying compiler that targets Typed Assembly Language (TALx86) and discuss some general techniques we have used to keep annotation sizes small and verification times fast. We quantify the effectiveness of these techniques by measuring their effects on a sizeable application — the certifying compiler itself. Using these techniques, which include common-subexpression elimination of types, higher-order type abbreviations, and selective reverification, can dramatically change certificate size and verification time.

This material is based on work supported in part by the AFOSR grant F49620- 97-1-0013, ARPA/RADC grant F30602-1-0317, and a National Science Foundation Graduate Fellowship. Any opinions,findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Twenty-Seventh ACM Symposium on Principles of Programming Languages, pages 243–253, Boston, MA, January 2000.

    Google Scholar 

  2. Quetzalcoatl Bradley, R. Nigel Horspool, and Jan Vitek. Jazz: An efficient compressed format for Java archive files. In CASCON’98, November 1998.

    Google Scholar 

  3. Preston Briggs, Keith Cooper, and Linda Torczon. Improvements to graph coloring register allocation. ACM Transactions on Progamming Languages and Systems, 16(3):428–455, May 1994.

    Article  Google Scholar 

  4. G. Chaitin, M. Auslander, A. Chandra, J. Cocke, M. Hopkins, and P. Markstein. Register allocation via coloring. Computer Languages, 6:47–57, 1981.

    Article  Google Scholar 

  5. Christopher Colby, Peter Lee, George Necula, and Fred Blau. A certifying compiler for Java. In ACM Conference on Programming Language Design and Implementation, pages 95–107, Vancouver, Canada, 2000.

    Google Scholar 

  6. Karl Crary. A simple proof technique for certain parametricity results. In Fourth ACM International Conference on Functional Programming, pages 82–89, Paris, France, September 1999.

    Google Scholar 

  7. Jens Ernst, William Evans, Christopher W. Fraser, Todd A. Proebsting, and Steven Lucco. Code compression. In ACM Conference on Programming Language Design and Implementation, pages 358–365, Las Vegas, NV, June 1997.

    Google Scholar 

  8. Lal George and Andrew W. Appel. Iterated register coalescing. ACM Transactions on Progamming Languages and Systems, 18(3):300–324, May 1996.

    Article  Google Scholar 

  9. Neal Glew. Type dispatch for named hierarchical types. In Fourth ACM International Conference on Functional Programming, pages 172–182, Paris, France, September 1999.

    Google Scholar 

  10. Neal Glew and Greg Morrisett. Type safe linking and modular assembly language. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 250–261, San Antonio, TX, January 1999.

    Google Scholar 

  11. R. Harper, F. Honsell, and G. Plotkin. A framework for de ning logics. Journal of the ACM, 40(1):143–184, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  12. Luke Hornof and Trevor Jim. Certifying compilation and run-time code generation. In ACM Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 60–74, San Antonio, TX, January 1999.

    Google Scholar 

  13. David Kempe. Personal communication. Scalable Certi cation for Typed Assembly Language 145

    Google Scholar 

  14. Dexter Kozen. Efficient code certification. Technical Report 98-1661, Department of Computer Science, Cornell University, Ithaca, NY, January 1998.

    Google Scholar 

  15. Xavier Leroy. The Objective Caml system, documentation, and user’s guide, 1998.

    Google Scholar 

  16. Steven Lucco. Split-stream dictionary program compression. In ACM Conference on Programming Language Design and Implementation, pages 27–34, Vancouver, Canada, June 2000.

    Google Scholar 

  17. Harry Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387–394, September 1992.

    Article  MATH  MathSciNet  Google Scholar 

  18. Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25–35, Atlanta, GA, 1999. Published as INRIA Technical Report 0288, March, 1999.

    Google Scholar 

  19. Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28–52, Kyoto, Japan, March 1998. Springer-Verlag.

    Chapter  Google Scholar 

  20. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Progamming Languages and Systems, 21(3):528–569, May 1999.

    Google Scholar 

  21. Gapolan Nadathur. A notation for lambda terms II: Re nements and applications. Technical Report CS-1994-01, Duke University, Durham, NC, January 1994.

    Google Scholar 

  22. George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation, pages 333–344, Montreal, Canada, June 1998.

    Google Scholar 

  23. George Necula and Peter Lee. Efficient representation and validation of proofs. In Thirteenth Symposium on Logic in Computer Science, pages 93–104, Indianapolis, IN, June 1998.

    Google Scholar 

  24. George Necula and S. P. Rahul. Oracle-based checking of untrusted software. In Twenty-Eigth ACM Symposium on Principles of Programming Languages, pages 142–154, London, United Kingdom, January 2001.

    Google Scholar 

  25. William Pugh. Compressing Java class files. In ACM Conference on Programming Language Design and Implementation, pages 247–258, Atlanta, GA, May 1999.

    Google Scholar 

  26. Zhong Shao, Christopher League, and Stefan Monnier. Implementing typed intermediate languages. In Third ACM International Conference on Functional Programming, pages 313–323, Baltimore, MD, September 1998.

    Google Scholar 

  27. Fred Smith, David Walker, and Greg Morrisett. Alias types. In Ninth European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366–381, Berlin, Germany, March 2000. Springer-Verlag.

    Google Scholar 

  28. D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: a type-directed optimizing compiler for ML. In ACM Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, PA, May 1996.

    Google Scholar 

  29. Philip Wadler. Theorems for free! In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 347–359, London, United Kingdom, September 1989.

    Google Scholar 

  30. Andrew K. Wright and Robert Cartwright. A practical soft type system for Scheme. ACM Transactions on Progamming Languages and Systems, 19(1):87–152, January 1997.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, USA

    Dan Grossman

  2. Department of Computer Science, Cornell University, USA

    Greg Morrisett

Authors
  1. Dan Grossman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Greg Morrisett
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University School of Computer Science, 5000 Forbes Avenue, Pittsburgh, PA, 15213-3891, USA

    Robert Harper

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grossman, D., Morrisett, G. (2001). Scalable Certification for Typed Assembly Language. In: Harper, R. (eds) Types in Compilation. TIC 2000. Lecture Notes in Computer Science, vol 2071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45332-6_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-45332-6_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42196-2

  • Online ISBN: 978-3-540-45332-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation