Linking is a low-level task that is usually vaguely specified, if at all, by language definitions. However, the security of web brows&s and other extensible systems depends crucially upon a set of checks that must be performed at link time. Building upon the simple, but elegant ideas of Cardelli, and module constructs from high-level languages, we present a formal model of typed object jiles and a set of inference rules that are sufficient to guarantee that type safety is preserved by the linking process. Whereas Cardelli's link calculus is built on top of the simply-typed lambda calculus, our object files are based upon typed assembly language so that we may model important low-level implementation issues. Furthermore, unlike Cardelli, we provide support for abstract types and higherorder type constructors-features critical for building extensible systems or modern programming languages such as ML. Linking separately compiled program units is an important task that is typically omitted from language definitions. In large part, this omission is due to low-level architecture and compiler dependencies that seem outside the realm of language design. However, extensible systems [LY97, WLAG93, BSP+95, Nec97, Koz98, HCC+98] are being built based upon the strong safety guarantees that language definitions provide. These systems use linking and loading as a fundamental part of their operation, so it is critical to precisely define the consistency checks a linker, be it static or dynamic, must perform. For example, Java-extensible web browsers, such as Netscape's Navigator and Microsoft's Internet Explorer, rely on static type systems with link checks to enforce a wide class of important safety properties. Extensions (applets) are written in a high-level language such as Java, and then compiled by an untrusted compiler to a target language (Java Virtual Machine bytecode). The integrity of the browser does not depend on type soundness of Java, but rather on type soundness (among other properties) of the JVM. As the JVM supports dynamic linking and loading of applets, a critical component of the JVM definition is the description of well-formed compilation units and link compatibility. Unfortunately, this component is vaguely specified and has been a source of well publicised security holes [MF96, Sar97]. Recently, Cardelli proposed a calculus of compilation units for the simply-typed lambda-calculus and presented a set of rules for determining link compatibility [Car97]. Cardelli's work specified high-level abstractions for modules and interfaces, and provided a set of inference rules for determining that program fragments, when compiled under certain typing assumptions, met a set of consistency requirements necessary to ensure that the resulting program was well-formed and hence would not "go wrong" when evaluated. In previous work, we presented a Typed Assembly Language (TAL) [MWCG98] that was suitable for compiling high-level core languages, and it seemed natural to extend this work with the ideas of Cardelli to give a detailed treatment of type-safe linking. However, though Cardelli's calculus is an elegant formulation 'of some of the high-level issues involved in linking, we found that it abstracts from many important low-level details such as binding and alpha-variance of labels, and omits certain critical features, notably support for cyclic inter-object file references, user-defined type abstraction, and dynamic linking. Hence, the goal of this paper is to build upon Cardelli's work and provide a suitable treatment of these issues. In particular, we extend core TAL with a language of typed object files and formalise the concepts of linking and link compatibility. The goals of the design were to model important properties of conventional object files and linkers (e.g., Unix's Id or Win32's link), and provide a module structure that supports separate type-checking of object files and separate compilation of high-level language features such as the abstract types, signatures, structures, and functors of SML. Our design for typed object files borrows heavily from the previous work on modules for high-level languages and hence there are relatively few important innovations. However, we believe this to be a virtue as it demonstrates that the programming language community has identified most of the critical issues for any module language, and it allows us to concentrate on those issues specific to object files. We have implemented the resulting design as part of an on-going language-based security project. The implementation provides a set of tools for defining and typechecking a variant of IA32 (Intel 80x86) object files and interfaces. These tools, together with a compiler that maps a variant of type-safe C code to type-safe object files is available at http: //www . cs . Cornell. edu/home/walker/ talnet/tal.html#talc. We proceed as follows: In Section 2, we present the abstractions of conventional untyped object files and linkers (e.g., Unix's Id) and discuss the issues of link compatibility in this simplified setting. In Section 3, we briefly review the type system of TAL and introduce a simple module language MTALo, which, in the spirit of Cardelli, provides support for separate compilation, separate type-checking, and a stronger notion of link compatibility. We extend MTALe in Section 4 with support for abstract types in the style of Clu or Modula-2, higher-order type constructors in the style of Objective Caml, and translucent types in the style of Harper and Lillibridge [HL94] and Leroy [Ler94]. The resulting language, MTAL (pronounced metal), is sufficiently expressive that we may compile ML-style modules, including functors, to the target language. Finally, in Section 5 we discuss extending our model to include dynamic linking and dynamic loading. We begin with a model of typical untyped object files and the process of linking. Untyped Assembly Language Figure 1 Here, the initial program state includes a register file that maps r2 to the value 6, and the program counter points to an instruction sequence where the first instruction is intended to add 3 to the contents of register r2, placing the 'A proper account would need to distinguish word values that may be stored in the heap or in a register from values that may be operands (which include registers). resulting value in ri. Hence, the reduction relation takes us to a program state with the same heap, an updated register file that maps rl to the value 9, and an updated program counter that points to the next instruction in the sequence to be executed. Abstractly, an object file consists of three components:
Glew and Morrisett REF tackle the problem of safe linking for TAL program fragments and provide an extension of TAL's type system that guarantees that linking preserves type safety.
Type-safe linking and modular assembly language
POPL '99
Computer Science