Safe and flexible dynamic linking of native code

Abstract. We present the design and implementation of the first com-plete framework for flexible and safe dynamic linking of native code. Our approach extends Typed Assembly Language with a primitive for loading and typechecking code, which is flexible enough to support a variety of linking strategies, but simple enough that it does not signif-icantly expand the trusted computing base. Using this primitive, along with the ability to compute with types, we show that we can program many existing dynamic linking approaches. As a concrete demonstra-tion, we have used our framework to implement dynamic linking for a type-safe dialect of C, closely modeled after the standard linking facility for Unix C programs. Aside from the unavoidable cost of verification, our implementation performs comparably with the standard, untyped approach.