Skip to main content

The Missing Link: Explaining ELF Static Linking, Semantically

Kell, Stephen, Mulligan, Dominic P., Sewell, Peter (2016) The Missing Link: Explaining ELF Static Linking, Semantically. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. SPLASH Systems, Programming, and Applications . pp. 607-623. ACM, New York, USA ISBN 978-1-4503-4444-9. (doi:10.1145/2983990.2983996) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:69700)

PDF Updated Version
Language: English

Restricted to Repository staff only
[thumbnail of oopsla-elf-linking-2016.pdf]
Official URL:
https://doi.org/10.1145/2983990.2983996

Abstract

Beneath the surface, software usually depends on complex linker behaviour to work as intended. Even linking <pre>hello_world.c</pre> is surprisingly involved, and systems software such as <pre>libc</pre> 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 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 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.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2983990.2983996
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Stephen Kell
Date Deposited: 07 Jan 2019 17:34 UTC
Last Modified: 17 Aug 2022 12:22 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/69700 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.