Karl Crary, Michael Hicks, Stephanie Weirich
We present the design and implementation of a framework for flexible and
safe dynamic linking of native code. Our approach extends Typed Assembly
Language with a typechecking primitive, which is flexible enough to
support a variety of linking strategies, but simple enough that it does
not significantly 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
demonstration, 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.
(ps.gz)