@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: /usr/bin/bib2bib -c topic:"linksem" -ob topic.linksem.bib sewellbib2.bib}}
  author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
  title = {The missing link: explaining {ELF} static linking, semantically},
  conf = {OOPSLA 2016},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  series = {OOPSLA 2016},
  year = {2016},
  month = nov,
  location = {Amsterdam, The Netherlands},
  numpages = {17},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Linking, formal specification, Executable and Linkable Format (ELF), theorem-proving},
  abstract = {Beneath the surface, software usually depends on complex \emph{linker
  behaviour} to work as intended.  Even linking
\texttt{hello\_world.c} is surprisingly involved, and systems software
such as \texttt{libc} and operating system kernels rely on a host of
linker features.  But linking is poorly understood by working
programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and
the poorly specified \emph{linker speak} by which they are controlled:
metadata in object files, command-line options, and linker-script
language.  We provide the first validated formalisation of a realistic
executable and linkable format (ELF), and capture aspects of the
Application Binary Interfaces for four mainstream platforms (AArch64,
AMD64, Power64, and IA32).  Using these, we develop an executable
specification of static linking, covering (among other things) enough to link
small C programs (we use the example of \textsf{bzip2}) into a correctly
running executable.  We
provide our specification in Lem and Isabelle/HOL forms.  This is the
first formal specification of mainstream linking.  We have used the
Isabelle/HOL version to prove a sample
correctness property for one case of AMD64 ABI relocation,
demonstrating that the specification supports formal proof, and as a
first step towards the much more ambitious goal of verified linking.
Our work should enable several novel strands of research, including
linker-aware verified compilation and program analysis, and better
languages for controlling linking.
  url = {},
  doi = {10.1145/2983990.2983996},
  pdf = {},
  project = {},
  topic = {linksem},
  recent = {true}