| Many kinds of networked devices receive and execute new programs from various sources. Since we may not fully trust the producers of these programs, we must take measures to ensure that such code does not misbehave. Currently deployed mobile code formats can be checked for memory safety and other security properties, but they are relatively high-level. A type-preserving compiler generates lower-level, more optimized code that is still verifiable. This increases assurance by reducing the trusted computing base; we need not trust the compiler anymore. Moreover, lower-level representations naturally support a wider variety of source languages.; Previous research on type-preserving compilation focused on functional languages or safe subsets of C. How to adapt this technology to more widely-used object-oriented languages was unknown. This dissertation explores techniques that enable a single strongly-typed intermediate language to certify programs in two very different programming languages: Java and ML.; The major contribution is an efficient new encoding of object-oriented constructs into a typed intermediate language. I give a complete formal translation of a Java-like source calculus into a typed lambda calculus. I prove that both languages are sound and decidable, and that the translation preserves types.; I also address many practical concerns, moving beyond the formal model to include most features of the Java language. To stage the translation, I developed lambda JVM, a novel representation of Java byte-code that is simpler to verify. I describe a prototype compiler that supports both Java and ML, sharing the same typed intermediate language, optimizers, code generator, and runtime system. |
