Type-Based Certifying Compilation

Last modified: Mon Apr 29 14:46:56 2002 GMT.

Authors

Abstract

Type-based certifying compilers are compilers that use static type information to help generate provably secure target code. Many modern programming languages (e.g., Java, ML) have a strong type system: a program that passes typechecking will not ``go wrong'' at runtime. A conventional untyped compiler discards all the type information after typechecking. A type-preserving compiler, on the other hand, translates both the program and the type information into the intermediate and target languages.

This tutorial will give a gentle introduction to the area of typed intermediate languages and certifying compilation. We will describe the design of various intermediate representations and show how to use type information to certify advanced constructs such as unboxed data structures, array access without bounds-checking, runtime type dispatch, method invocation, and memory management. We will also examine several existing type-based compilers and discuss the impact of their design on their capabilities and performance. This tutorial is aimed for those interested in mobile code security, virtual machine design, proof-carrying code, and program validation.

Published

Invited tutorial presented at 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Salt Lake City, Utah, June 2001.

PowerPoint [656k]
PDF [570k]

Here are a list of accompanying references.

colophon