mold design notes very interesting. performance tricks, history of linker features The teensy files - writing elf by hand On ELF, Part 2 - a ctrique of elf for being too complex compared to previous formats and for little gain. Counterpoints Assembler and loaders - David Salomon compcert linking file This file follows “approach A” from the paper “Lightweight Verification of Separate Compilation” by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016. Cody tweeting about it

APE - Actually portable executable, Cosmopolitan library geometry of interaction stuff. Neel Krinshnasawmi

Dwarf - it’s like complicated. But there is a lot in there.

addr2line and other binutils libdwarf. dwarfdump - lots of interesting stuff on linkers, elf, other - his small linker. Uses ocaml? - generates ocaml?

ld_preload hacking Hmm. So one thing you can do is mock out functions for testing. That’s nice referenced guide on how to write dynamic linker

ryan oneill elfmaster silvio text segement padding SCOP padding secure cide oartitioning PT_LOAD insertion - “learning linux binary analysis” book. reverse text extension techniuqe github elfmaster - skeski virus, dt data segment insertion - “learning linux binary analysis” dt_needed override dt_infect. dynamic segment .got.plt infection ymbol string redirection - global data in the .got elf binary control flow hooks, function trampolines, function pointer hooks, breakpoint hnadlerh ook, tls resolver, sigill handler

ptrace , injecting a loader

  • the author of gold, Ian Lance Taylor’s 20 part Linker posts V good

Symbols - Types and values? Relocations - Bits of code that runs in general? Kind of bytecode?

Executable config files - dhall. Others. Kaitai has executable aspects. if then else, others.

Functional models of linking

type fixups/relocs = Mov Add ?

{ relocs: fixups symbols: {name : string ; typ : typ; value : value}list contents: { section : name; contents : string } }

bap’s model

type name = [
  | `tid of tid
  | `addr of addr
  | `symbol of string
] [@@deriving bin_io, compare, sexp]

type exn += Unbound_name of name

module type Code = functor (Machine : Machine) -> sig
  val exec : unit Machine.t

type code = (module Code)

(* the same piece of code can be referred via multiple names *)
type refs = {
  term : tid option;
  name : string option;
  addr : addr option;

type t = {
  codes : code Int.Map.t;
  alias : refs Int.Map.t;
  terms : int Tid.Map.t;
  names : int String.Map.t;
  addrs : int Addr.Map.t;
} This is the ocaml data format of cmo files

JT’s notes

ld has default linker script ld --verbose to see -T linker script (manual)

SECTION : set current address. tell what sections from different files to include.


So could I use a linker script to build a computation? By wiring together input and output cells?

Here’s an interesting challenge: linking verification Verify a relational property that after linking the program still does the same thing. Requires a model of linking and patching requires fixups maybe you could have the loader actually do its work and pop in by peeking at /proc/mem Or maybe ld_preload ? You’d want a total program verification. In principle the problem is easy? There is link level modulairty there. So maybe that’s good