Scalable Certification for Typed Assembly Language

Dan Grossman, Greg Morrisett

To appear at ACM SIGPLAN Workshop on Types in Compilation (TIC00), Montreal, Canada, 21 September 2000


A type-based, certifying compiler maps source code to machine code and target-level typing 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 source language and compiler 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. The selective use of these techniques, which include common-subexpression elimination of types, higher-order type abbreviations, and selective reverification, can change certificate size and verification time by well over an order of magnitude.

Server START Conference Manager
Update Time 27 Jul 2000 at 15:10:31
Start Conference Manager
Conference Systems