Show simple item record

dc.contributor.authorKell, Stephenen
dc.contributor.authorMulligan, Dominicen
dc.contributor.authorSewell, Peteren
dc.date.accessioned2016-10-14T11:44:34Z
dc.date.available2016-10-14T11:44:34Z
dc.date.issued2016-10-19en
dc.identifier.issn1523-2867
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/260771
dc.description.abstractBeneath the surface, software usually depends on com- plex linker behaviour to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as 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 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.
dc.description.sponsorshipWe acknowledge funding from EPSRC grants EP/H005633 (Leadership Fellowship, Sewell) and EP/K008528 (REMS: Rigorous Engineering for Mainstream Systems Programme Grant).
dc.languageEnglishen
dc.language.isoenen
dc.publisherAssociation for Computing Machinery
dc.rightsAttribution 4.0 International
dc.rightsAttribution 4.0 Internationalen
dc.rightsAttribution 4.0 Internationalen
dc.rightsAttribution 4.0 Internationalen
dc.rightsAttribution 4.0 Internationalen
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.subjectlinkingen
dc.subjectformal specificationen
dc.subjectexecutable and linkable format (ELF)en
dc.subjecttheorem-provingen
dc.titleThe Missing Link: Explaining ELF Static Linking, Semanticallyen
dc.typeConference Object
dc.description.versionThis is the final version of the article. It first appeared from Association for Computing Machinery via https://doi.org/10.1145/3022671.2983996en
prism.endingPage623
prism.publicationDate2016en
prism.publicationNameACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) 2016en
prism.startingPage607
dc.identifier.doi10.17863/CAM.5923
dc.identifier.doi10.17863/CAM.5923
dc.identifier.doi10.17863/CAM.5923
dcterms.dateAccepted2016-08-02en
rioxxterms.versionofrecord10.1145/2983990.2983996en
rioxxterms.versionVoRen
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/en
rioxxterms.licenseref.startdate2016-10-19en
dc.contributor.orcidKell, Stephen [0000-0002-2702-5983]
dc.contributor.orcidMulligan, Dominic [0000-0003-4643-3541]
dc.identifier.eissn1558-1160
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/K008528/1)
datacite.issupplementedby.doi10.17863/CAM.1674en
cam.orpheus.successThu Nov 05 11:56:25 GMT 2020 - The item has an open VoR version.*
rioxxterms.freetoread.startdate2100-01-01


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International