Extant papers touching on dynamic linking and loading.

CompCert is a formally verified optimizing C compiler. Initial versions did not offer support for concurrent programs or proofs regarding separately compiled programs. Various extensions to CompCert have been proposed to alleviate either or both of these deficiencies, but unfortunately none offer us a compelling model for continuing our research.

Compositional CompCert

CompComp modifies the existing CompCert proofs to enable guarantees of separately compiled programs. Unlike SepCompCert, it does not rely on the programs being compiled by (almost) the same compiler, but rather imposes some restrictions on the behaviour of the linked modules. The restrictions are all things that would be unsound in Rust. The proofs rely on the modules not touching eachothers memory unless a pointer is explicitly passed to a function. This notion of memory blocks may be similar to certain formalizations of Rust lifetimes, although I’d need to do further research.

SepCompCert

Lightweight Verification of Separate Compilation (POPL 2016): SepCompCert makes various safety assumptions that are acceptable for programs in C, but are ones that we would like to mechanically ensure in our model. Namely, it defines a notion of “syntactic linking” that is far simpler than either static or dynamic linking of real object files. Moreover, this model does not handle “static” variables. These kinds of semantics are precisely those that our research is trying to make explicit and build ontop of.

CASCompCert

Towards Certified Separate Compilation for Concurrent Programs (PLDI 2019): CASCompCert extends the meta-theory of CompCert to enable the linking of concurrent programs. Unfortunately the models of both concurrency and linking are overly simplistic for our use cases. The meta-theory stops short of creating actual binaries, instead creating assembly to be passed to a separate assembler. Furthermore, the theory does not include any mention of thread-local or global variables, and does not model the actual spawning of threads.

The Security of Static Typing with Dynamic Linking

doi: 10.1145/266420.266428 (CCS 1997), by Drew Dean. Java applets in Netscape Navigator 2.02 had a security hole where the typechecker could be circumvented by switching which class would be loaded at runtime. The gist is that the applet would be typechecked against system libraries, but the libraries could be replaced before they were actually loaded. The proposed solution was to always load each class only once, such that the types and “content” of the classes could not mismatch.

We cannot lift their solution though, as it relies on a runtime typechecker to be present, and for types to exist at runtime. This overhead is acceptable in the presence of a large runtime like the JVM, and most type information needs to be present regardless to support garbage collection and inheritance. For a language with a minimal runtime, this cost needs to be more carefully considered against other tradeoffs however.

SunOS dynamic linker whitepaper

Published at the Summer 1987 USENIX conference, Shared Libraries in SunOS by Robert A. Gingell, Meng Lee, Xuong T. Dang & Mary S. Weeks. It gives a pretty good explanation of the procedure linkage table (PLT), and the global offset table (GOT). Of particular interest to the current work is that this system requires minimal kernel-level support, meaning that the semantics of loading libraries can be modified from userspace. The position-independent executables created in this manner can also be used with address-space layout randomization (ASLR), although this only becomes standard from 2003 onwards. The paper does describe linking the a.out format rather than the modern ELF format, but the linking is pretty similar. Also of note is that a lot of modern linker features originated in [Open]Solaris.

Of interest as well is that the description of “library interposition” fulfils the requirements of Rubicons import/export-globals without having to create an ancillary shared object.

Rubicon

Rubicon (presentation) is a project by Amos Wenger to enable dynamic linking of Rust programs, as long as many invariants are maintained. Particularly, the compiler version must stay the same for all libraries. The only feature of Rubicon is the ability to put all globals (both global-globals and thread-local variables) into a single shared object. This enables the sharing of for example a tokio runtime between multiple dynamic libraries.

A philosophical peculiarity of Rubicon is the “xgraph” model. Under xgraph, every dependency has its own dependencies without being deduplicated. The advantage is that significantly less work has to be performed when no changes have been made to the libraries. The disadvantage is that one project will depend on many versions of the same library, each with different monomorphisations.

All that would be needed to support this usecase is to make the --import-globals and --export-globals linker options available from rustc. This can be included in the questionarre to gage interest.

Java and C♯ models

There are multiple papers on specifying and abstracting the dynamic linking and loading models of Java and C♯. Unfortunately they make the assumption that the language guarantees safety by being a bit dynamic. There is also no exploration of if safe code can break the invariants of loaded code or vice versa.

Both Java and C♯ ensure that a whole class is loaded together, rather than symbols being resolved individually. An implementation that uses the system linker/loader for symbol resolution does not natively have that guarantee. One solution is to mediate all methods through a handle provided by the object, but this adds runtime overhead, and does not solve the problem for other types used by the method.

Glosses over guaranteeing versioning, but do cite work on it.

Papers: [1] and [2]

[1]		Ancona, D. et al. 2003. A calculus for dynamic linking. Springer, Berlin, Heidelberg.
[2]		Drossopoulou, S. et al. 2003. Flexible models for dynamic linking. Springer, Berlin, Heidelberg.