package linksem

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

elf_dynamic module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file.

Validity checks

val is_elf32_valid_program_header_table_for_dynamic_linking : Elf_program_header_table.elf32_program_header_table_entry list -> bool

is_elf32_valid_program_header_table_for_dynamic_linking pht checks whether * a program header table pht is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type elf_pt_interp, i.e. contains a string pointing * to the requested dynamic interpreter.

val is_elf64_valid_program_header_table_for_dynamic_linking : Elf_program_header_table.elf64_program_header_table_entry list -> bool

is_elf64_valid_program_header_table_for_dynamic_linking pht checks whether * a program header table pht is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type elf_pt_interp, i.e. contains a string pointing * to the requested dynamic interpreter.

Dynamic section entry

type ('a, 'b) dyn_union =
  1. | D_Val of 'a
  2. | D_Ptr of 'b
  3. | D_Ignored of Byte_sequence.byte_sequence0

dyn_union represents the C-union type used in the definition of elf32_dyn * and elf64_dyn types below. Some section tags correspond to entries where * the fields are either unspecified or ignored, hence the presence of the * D_Ignored constructor.

type elf32_dyn = {
  1. elf32_dyn_tag : Int32.t;
    (*

    The type of the entry.

    *)
  2. elf32_dyn_d_un : (Uint32_wrapper.uint32, Uint32_wrapper.uint32) dyn_union;
    (*

    The value of the entry, stored as a union.

    *)
}

elf32_dyn captures the notion of an ELF32 dynamic section entry. * Specialises the dyn_union type above to using elf32_word values and * elf32_addr pointers.

type elf64_dyn = {
  1. elf64_dyn_tag : Int64.t;
    (*

    The type of the entry.

    *)
  2. elf64_dyn_d_un : (Uint64_wrapper.uint64, Uint64_wrapper.uint64) dyn_union;
    (*

    The value of the entry, stored as a union.

    *)
}

elf64_dyn captures the notion of an ELF32 dynamic section entry. * Specialises the dyn_union type above to using elf64_xword values and * elf64_addr pointers.

Dynamic section tags

val dt_null : Nat_big_num.num

dt_null marks the end of the dynamic array

dt_needed holds the string table offset of a string containing the name of * a needed library.

val dt_needed : Nat_big_num.num

dt_needed holds the string table offset of a string containing the name of * a needed library.

dt_pltrelsz holds the size in bytes of relocation entries associated with * the PLT.

val dt_pltrelsz : Nat_big_num.num

dt_pltrelsz holds the size in bytes of relocation entries associated with * the PLT.

dt_pltgot holds an address associated with the PLT or GOT.

val dt_pltgot : Nat_big_num.num

dt_pltgot holds an address associated with the PLT or GOT.

dt_hash holds the address of a symbol-table hash.

val dt_hash : Nat_big_num.num

dt_hash holds the address of a symbol-table hash.

dt_strtab holds the address of the string table.

val dt_strtab : Nat_big_num.num

dt_strtab holds the address of the string table.

dt_symtab holds the address of a symbol table.

val dt_symtab : Nat_big_num.num

dt_symtab holds the address of a symbol table.

dt_rela holds the address of a relocation table.

val dt_rela : Nat_big_num.num

dt_rela holds the address of a relocation table.

dt_relasz holds the size in bytes of the relocation table.

val dt_relasz : Nat_big_num.num

dt_relasz holds the size in bytes of the relocation table.

dt_relaent holds the size in bytes of a relocation table entry.

val dt_relaent : Nat_big_num.num

dt_relaent holds the size in bytes of a relocation table entry.

dt_strsz holds the size in bytes of the string table.

val dt_strsz : Nat_big_num.num

dt_strsz holds the size in bytes of the string table.

dt_syment holds the size in bytes of a symbol table entry.

val dt_syment : Nat_big_num.num

dt_syment holds the size in bytes of a symbol table entry.

dt_init holds the address of the initialisation function.

val dt_init : Nat_big_num.num

dt_init holds the address of the initialisation function.

dt_fini holds the address of the finalisation function.

val dt_fini : Nat_big_num.num

dt_fini holds the address of the finalisation function.

dt_soname holds the string table offset of a string containing the shared- * object name.

val dt_soname : Nat_big_num.num

dt_soname holds the string table offset of a string containing the shared- * object name.

dt_rpath holds the string table offset of a string containing the library * search path.

val dt_rpath : Nat_big_num.num

dt_rpath holds the string table offset of a string containing the library * search path.

dt_symbolic alters the linker's symbol resolution algorithm so that names * are resolved first from the shared object file itself, rather than the * executable file.

val dt_symbolic : Nat_big_num.num

dt_symbolic alters the linker's symbol resolution algorithm so that names * are resolved first from the shared object file itself, rather than the * executable file.

dt_rel is similar to dt_rela except its table has implicit addends.

val dt_rel : Nat_big_num.num

dt_rel is similar to dt_rela except its table has implicit addends.

dt_relsz holds the size in bytes of the dt_rel relocation table.

val dt_relsz : Nat_big_num.num

dt_relsz holds the size in bytes of the dt_rel relocation table.

dt_relent holds the size in bytes of a dt_rel relocation entry.

val dt_relent : Nat_big_num.num

dt_relent holds the size in bytes of a dt_rel relocation entry.

dt_pltrel specifies the type of relocation entry to which the PLT refers.

val dt_pltrel : Nat_big_num.num

dt_pltrel specifies the type of relocation entry to which the PLT refers.

dt_debug is used for debugging and its purpose is not specified in the ABI. * Programs using this entry are not ABI-conformant.

val dt_debug : Nat_big_num.num

dt_debug is used for debugging and its purpose is not specified in the ABI. * Programs using this entry are not ABI-conformant.

dt_textrel absence of this entry indicates that no relocation entry should * cause a modification to a non-writable segment. Otherwise, if present, one * or more relocation entries may request modifications to a non-writable * segment.

val dt_textrel : Nat_big_num.num

dt_textrel absence of this entry indicates that no relocation entry should * cause a modification to a non-writable segment. Otherwise, if present, one * or more relocation entries may request modifications to a non-writable * segment.

dt_jmprel's member holds the address of relocation entries associated with * the PLT.

val dt_jmprel : Nat_big_num.num

dt_jmprel's member holds the address of relocation entries associated with * the PLT.

dt_bindnow instructs the linker to process all relocations for the object * containing the entry before transferring control to the program.

val dt_bindnow : Nat_big_num.num

dt_bindnow instructs the linker to process all relocations for the object * containing the entry before transferring control to the program.

dt_init_array holds the address to the array of pointers to initialisation * functions.

val dt_init_array : Nat_big_num.num

dt_init_array holds the address to the array of pointers to initialisation * functions.

dt_fini_array holds the address to the array of pointers to finalisation * functions.

val dt_fini_array : Nat_big_num.num

dt_fini_array holds the address to the array of pointers to finalisation * functions.

dt_init_arraysz holds the size in bytes of the array of pointers to * initialisation functions.

val dt_init_arraysz : Nat_big_num.num

dt_init_arraysz holds the size in bytes of the array of pointers to * initialisation functions.

dt_fini_arraysz holds the size in bytes of the array of pointers to * finalisation functions.

val dt_fini_arraysz : Nat_big_num.num

dt_fini_arraysz holds the size in bytes of the array of pointers to * finalisation functions.

dt_runpath holds an offset into the string table holding a string containing * the library search path.

val dt_runpath : Nat_big_num.num

dt_runpath holds an offset into the string table holding a string containing * the library search path.

dt_flags holds flag values specific to the object being loaded.

val dt_flags : Nat_big_num.num

dt_flags holds flag values specific to the object being loaded.

val dt_encoding : Nat_big_num.num

dt_preinit_array holds the address to the array of pointers of pre- * initialisation functions.

val dt_preinit_array : Nat_big_num.num

dt_preinit_array holds the address to the array of pointers of pre- * initialisation functions.

dt_preinit_arraysz holds the size in bytes of the array of pointers of * pre-initialisation functions.

val dt_preinit_arraysz : Nat_big_num.num

dt_preinit_arraysz holds the size in bytes of the array of pointers of * pre-initialisation functions.

dt_loos and dt_hios: this inclusive range is reserved for OS-specific * semantics.

val dt_loos : Nat_big_num.num

dt_loos and dt_hios: this inclusive range is reserved for OS-specific * semantics.

val dt_hios : Nat_big_num.num

dt_loproc and dt_hiproc: this inclusive range is reserved for processor * specific semantics.

val dt_loproc : Nat_big_num.num

dt_loproc and dt_hiproc: this inclusive range is reserved for processor * specific semantics.

val dt_hiproc : Nat_big_num.num
val string_of_dynamic_tag : bool -> Nat_big_num.num -> (Nat_big_num.num -> bool) -> (Nat_big_num.num -> string) -> (Nat_big_num.num -> string) -> string

string_of_dynamic_tag so t os proc produces a string-based representation of * dynamic section tag t. For tag values between LO_OS and HI_OS os is * used to produce the resulting value. For tag values between LO_PROC and * HI_PROC proc is used to produce the resulting value. Boolean flag so * indicates whether the flag in question is derived from a shared object file, * which alters the printing of ENCODING and PRE_INITARRAY flags.

type tag_correspondence =
  1. | C_Val
    (*

    dyn_union should be interpreted as a value.

    *)
  2. | C_Ptr
    (*

    dyn_union should be interpreted as a pointer.

    *)
  3. | C_Ignored
    (*

    dyn_union is irrelevant, so we do not care.

    *)

tag_correspondence is a type used to emulate the functionality of a C-union * in Lem. The type records whether the union should be interpreted as a value, * a pointer, or a "do not care" value. An accompanying function will map a * dynamic section tag to a tag_correspondence, so that transcription functions * know how to properly use the dyn_union value in a dynamic section entry.

tag_correspondence_of_tag tag os_additional_ranges os proc produces a * tag_correspondence value for a given dynamic tag, tag. Some tag values * are reserved for interpretation by the OS or processor supplement (i.e. the * ABI). We therefore also take in a predicate, os_additional_ranges, that * recognises when a tag is "special" for a given ABI, and a means of interpreting * that tag, using os and proc functions.

read_elf32_dyn endian bs0 so os_additional_ranges os proc reads an elf32_dyn * record from byte sequence bs0, assuming endianness endian. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate os_additional_ranges and interpreted by * the functions os and proc. Fails if the transcription of the record from * bs0 fails, or if os or proc fail.

read_elf64_dyn endian bs0 os_additional_ranges os proc reads an elf64_dyn * record from byte sequence bs0, assuming endianness endian. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate os_additional_ranges and interpreted by * the functions os and proc. Fails if the transcription of the record from * bs0 fails, or if os or proc fail.

obtain_elf32_dynamic_section_contents' endian bs0 os_additional_ranges os * proc exhaustively reads in elf32_dyn values from byte sequence bs0, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf32_dyn entry is not 0.

obtain_elf64_dynamic_section_contents' endian bs0 os_additional_ranges os * proc exhaustively reads in elf64_dyn values from byte sequence bs0, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf64_dyn entry is not 0.

obtain_elf32_dynamic_section_contents' f1 os_additional_ranges os * proc bs0 exhaustively reads in elf32_dyn values from byte sequence bs0, * obtaining endianness and the section header table from elf32_file f1, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf32_dyn entry is not 0.

obtain_elf64_dynamic_section_contents' f1 os_additional_ranges os * proc bs0 exhaustively reads in elf64_dyn values from byte sequence bs0, * obtaining endianness and the section header table from elf64_file f1, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf64_dyn entry is not 0.

DT Flags values

val df_origin : Nat_big_num.num

df_origin specific that the object being loaded may make reference to the * $(ORIGIN) substitution string.

df_symbolic changes the linker's symbol resolution algorithm, resolving * symbols first from the shared object file rather than the executable file.

val df_symbolic : Nat_big_num.num

df_symbolic changes the linker's symbol resolution algorithm, resolving * symbols first from the shared object file rather than the executable file.

df_textrel if this flag is not set then no relocation entry should cause * modification to a non-writable segment.

val df_textrel : Nat_big_num.num

df_textrel if this flag is not set then no relocation entry should cause * modification to a non-writable segment.

df_bindnow if set this instructs the linker to process all relocation entries * of the containing object before transferring control to the program.

val df_bindnow : Nat_big_num.num

df_bindnow if set this instructs the linker to process all relocation entries * of the containing object before transferring control to the program.

df_static_tls if set instructs the linker to reject all attempts to load * the containing file dynamically.

val df_static_tls : Nat_big_num.num

df_static_tls if set instructs the linker to reject all attempts to load * the containing file dynamically.

val check_flag : Nat_big_num.num -> Nat_big_num.num -> bool

check_flag is a utility function for testing whether a flag is set. * TODO: so simple it is probably unneccessary now.

val string_of_dt_flag : Nat_big_num.num -> string

string_of_dt_flag f produces a string-based representation of dynamic * section flag f.

type rel_type =
  1. | Rel
    (*

    Plain relocation type.

    *)
  2. | RelA
    (*

    Relocation with addends type.

    *)

rel_type represents the two types of relocation records potentially present * in an ELF file: relocation, and relocation with addends.

val string_of_rel_type : rel_type -> string

string_of_rel_type r produces a string-based representation of rel_type, * r.

type ('addr, 'size) dyn_value =
  1. | Address of 'addr
    (*

    An address.

    *)
  2. | Size of 'size
    (*

    A size (in bytes).

    *)
  3. | FName of string
    (*

    A filename.

    *)
  4. | SOName of string
    (*

    A shared object name.

    *)
  5. | Path of string
    (*

    A path to some directory.

    *)
  6. | RPath of string
    (*

    A "run path".

    *)
  7. | RunPath of string
    (*

    A "run path".

    *)
  8. | Library of string
    (*

    A library path.

    *)
  9. | Flags1 of Nat_big_num.num
    (*

    Flags.

    *)
  10. | Flags of Nat_big_num.num
    (*

    Flags.

    *)
  11. | Numeric of Nat_big_num.num
    (*

    An uninterpreted numeric value.

    *)
  12. | Checksum of Nat_big_num.num
    (*

    A checksum value

    *)
  13. | RelType of rel_type
    (*

    A relocation entry type.

    *)
  14. | Timestamp of Nat_big_num.num
    (*

    A timestamp value.

    *)
  15. | Null
    (*

    A null (0) value.

    *)
  16. | Ignored
    (*

    An ignored value.

    *)

Type dyn_value represents the value of an ELF dynamic section entry. Values * can represent various different types of objects (e.g. paths to libraries, or * flags, or sizes of other entries in a file), and this type collates them all. * Parameterised over two type variables so the type can be shared between ELF32 * and ELF64.

elf32_dyn_value and elf64_dyn_value are specialisations of dyn_value * fixing the correct types for the 'addr and 'size type variables.

get_string_table_of_elf32_dyn_section endian dyns sht bs0 searches through * dynamic section entries dyns looking for one pointing to a string table, looks * up the corresponding section header sht pointed to by that dynamic * section entry, finds the section in bs0 and decodes a string table from that * section assuming endianness endian. May fail.

get_string_table_of_elf64_dyn_section endian dyns sht bs0 searches through * dynamic section entries dyns looking for one pointing to a string table, looks * up the corresponding section header sht pointed to by that dynamic * section entry, finds the section in bs0 and decodes a string table from that * section assuming endianness endian. May fail.

get_value_of_elf32_dyn so dyn os_additional_ranges os proc stab returns the value * stored in a dynamic section entry dyn, using os_additional_ranges and * os to decode ABI-reserved tags. String table stab is used to correctly * decode library and run paths, etc. * May fail.

get_value_of_elf64_dyn dyn os_additional_ranges os proc stab returns the value * stored in a dynamic section entry dyn, using os_additional_ranges and * os to decode ABI-reserved tags. String table stab is used to correctly * decode library and run paths, etc. * May fail.

OCaml

Innovation. Community. Security.