diff options
Diffstat (limited to 'src/elf_model/elf_executable_file5.lem')
| -rw-r--r-- | src/elf_model/elf_executable_file5.lem | 339 |
1 files changed, 339 insertions, 0 deletions
diff --git a/src/elf_model/elf_executable_file5.lem b/src/elf_model/elf_executable_file5.lem new file mode 100644 index 00000000..164cccb6 --- /dev/null +++ b/src/elf_model/elf_executable_file5.lem @@ -0,0 +1,339 @@ +open import Basic_classes +open import List +open import Maybe +open import Num +open import Tuple + +open import Elf_executable_file4 +open import Elf_header +open import Elf_interpreted_segment +open import Elf_program_header_table +open import Elf_section_header_table +open import Elf_types +open import String_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +(** Type [elf32_executable_file5] is an elf32_executable_file4 type where segments + * have been read from the program header table and interpreted. A process + * image can be obtained from this type. + *) +type elf32_executable_file5 = + <| elf32_executable_file5_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file5_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file5_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) + ; elf32_executable_file5_section_header_string_table : string_table (** The section header string table *) + ; elf32_executable_file5_segments : list elf32_interpreted_segment (** The list of segments as described by the program header table *) + ; elf32_executable_file5_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf32ExecutableFile5 'a) + val get_elf32_executable_file5 : 'a -> elf32_executable_file5 +end + +instance (HasElf32ExecutableFile5 elf32_executable_file5) + let get_elf32_executable_file5 f5 = f5 +end + +instance (HasElf32ExecutableFile4 elf32_executable_file5) + let get_elf32_executable_file4 f5 = + <| elf32_executable_file4_header = f5.elf32_executable_file5_header; + elf32_executable_file4_program_header_table = f5.elf32_executable_file5_program_header_table; + elf32_executable_file4_section_header_table = f5.elf32_executable_file5_section_header_table; + elf32_executable_file4_section_header_string_table = f5.elf32_executable_file5_section_header_string_table; + elf32_executable_file4_body = f5.elf32_executable_file5_body |> +end + +instance (HasElf32Header elf32_executable_file5) + let get_elf32_header f5 = f5.elf32_executable_file5_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file5) + let get_elf32_program_header_table f5 = Just (f5.elf32_executable_file5_program_header_table) +end + +instance (HasElf32SectionHeaderTable elf32_executable_file5) + let get_elf32_section_header_table f5 = f5.elf32_executable_file5_section_header_table +end + +instance (HasElf32SectionHeaderStringTable elf32_executable_file5) + let get_elf32_section_header_string_table f5 = f5.elf32_executable_file5_section_header_string_table +end + +(** Type [elf64_executable_file5] is an elf64_executable_file4 type where segments + * have been read from the program header table and interpreted. A process + * image can be obtained from this type. + *) +type elf64_executable_file5 = + <| elf64_executable_file5_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file5_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file5_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) + ; elf64_executable_file5_section_header_string_table : string_table (** The section header string table *) + ; elf64_executable_file5_segments : list elf64_interpreted_segment (** The list of segments as described by the program header table *) + ; elf64_executable_file5_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf64ExecutableFile5 'a) + val get_elf64_executable_file5 : 'a -> elf64_executable_file5 +end + +instance (HasElf64ExecutableFile5 elf64_executable_file5) + let get_elf64_executable_file5 f5 = f5 +end + +instance (HasElf64ExecutableFile4 elf64_executable_file5) + let get_elf64_executable_file4 f5 = + <| elf64_executable_file4_header = f5.elf64_executable_file5_header; + elf64_executable_file4_program_header_table = f5.elf64_executable_file5_program_header_table; + elf64_executable_file4_section_header_table = f5.elf64_executable_file5_section_header_table; + elf64_executable_file4_section_header_string_table = f5.elf64_executable_file5_section_header_string_table; + elf64_executable_file4_body = f5.elf64_executable_file5_body |> +end + +instance (HasElf64Header elf64_executable_file5) + let get_elf64_header f5 = f5.elf64_executable_file5_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file5) + let get_elf64_program_header_table f5 = Just (f5.elf64_executable_file5_program_header_table) +end + +instance (HasElf64SectionHeaderTable elf64_executable_file5) + let get_elf64_section_header_table f5 = f5.elf64_executable_file5_section_header_table +end + +instance (HasElf64SectionHeaderStringTable elf64_executable_file5) + let get_elf64_section_header_string_table f5 = f5.elf64_executable_file5_section_header_string_table +end + +(** [refine_elf32_executable_file4 f4] refines an elf32_executable_file4 [f4] into + * an elf32_executable_file5 by adding the interpreted segment field. Fails + * if an interpreted segment has a memory size smaller than its associated + * file size, an invalidation of the ELF spec. + *) +val refine_elf32_executable_file4 : elf32_executable_file4 -> error elf32_executable_file5 +let refine_elf32_executable_file4 f4 = + let pht = f4.elf32_executable_file4_program_header_table in + let bdy = f4.elf32_executable_file4_body in + let segs = + List.map (fun ph -> + let offset = nat_of_elf32_off ph.elf32_p_offset * 8 in + let size = nat_of_elf32_word ph.elf32_p_filesz * 8 in + let relevant = Bitstring.offset_and_cut offset size bdy in + let vaddr = nat_of_elf32_addr ph.elf32_p_vaddr in + let memsz = nat_of_elf32_word ph.elf32_p_memsz * 8 in + let typ = nat_of_elf32_word ph.elf32_p_type in + let flags = elf32_interpret_program_header_flags ph.elf32_p_flags in + <| elf32_segment_body = relevant; + elf32_segment_type = typ; + elf32_segment_size = size; + elf32_segment_memsz = memsz; + elf32_segment_base = vaddr; + elf32_segment_flags = flags |> + ) pht + in + let segs = + mapM (fun sg -> + if sg.elf32_segment_memsz < sg.elf32_segment_size then + Fail "refine_elf32_executable_file4: memory size of segment cannot be less than file size" + else + return sg) segs + in + segs >>= fun segs -> + return <| + elf32_executable_file5_header = f4.elf32_executable_file4_header; + elf32_executable_file5_program_header_table = f4.elf32_executable_file4_program_header_table; + elf32_executable_file5_section_header_table = f4.elf32_executable_file4_section_header_table; + elf32_executable_file5_section_header_string_table = f4.elf32_executable_file4_section_header_string_table; + elf32_executable_file5_segments = segs; + elf32_executable_file5_body = f4.elf32_executable_file4_body |> + +(** [refine_elf64_executable_file4 f4] refines an elf64_executable_file4 [f4] into + * an elf64_executable_file5 by adding the interpreted segment field. Fails + * if an interpreted segment has a memory size smaller than its associated + * file size, an invalidation of the ELF spec. + *) +val refine_elf64_executable_file4 : elf64_executable_file4 -> error elf64_executable_file5 +let refine_elf64_executable_file4 f4 = + let pht = f4.elf64_executable_file4_program_header_table in + let bdy = f4.elf64_executable_file4_body in + let segs = + List.map (fun ph -> + let offset = nat_of_elf64_off ph.elf64_p_offset * 8 in + let size = nat_of_elf64_xword ph.elf64_p_filesz * 8 in + let relevant = Bitstring.offset_and_cut offset size bdy in + let vaddr = nat_of_elf64_addr ph.elf64_p_vaddr in + let memsz = nat_of_elf64_xword ph.elf64_p_memsz * 8 in + let typ = nat_of_elf64_word ph.elf64_p_type in + let flags = elf64_interpret_program_header_flags ph.elf64_p_flags in + <| elf64_segment_body = relevant; + elf64_segment_type = typ; + elf64_segment_size = size; + elf64_segment_memsz = memsz; + elf64_segment_base = vaddr; + elf64_segment_flags = flags |> + ) pht + in + let segs = + mapM (fun sg -> + if sg.elf64_segment_memsz < sg.elf64_segment_size then + fail "refine_elf64_executable_file4: memory size of segment cannot be less than file size" + else + return sg) segs + in + segs >>= fun segs -> + return <| + elf64_executable_file5_header = f4.elf64_executable_file4_header; + elf64_executable_file5_program_header_table = f4.elf64_executable_file4_program_header_table; + elf64_executable_file5_section_header_table = f4.elf64_executable_file4_section_header_table; + elf64_executable_file5_section_header_string_table = f4.elf64_executable_file4_section_header_string_table; + elf64_executable_file5_segments = segs; + elf64_executable_file5_body = f4.elf64_executable_file4_body |> + +(** [read_elf32_executable_file5 bs0] reads an elf32_executable_file5 from bitstring + * [bs0]. + *) +val read_elf32_executable_file5 : bitstring -> error elf32_executable_file5 +let read_elf32_executable_file5 bs0 = + read_elf32_executable_file4 bs0 >>= refine_elf32_executable_file4 + +(** [read_elf64_executable_file5 bs0] reads an elf64_executable_file5 from bitstring + * [bs0]. + *) +val read_elf64_executable_file5 : bitstring -> error elf64_executable_file5 +let read_elf64_executable_file5 bs0 = + read_elf64_executable_file4 bs0 >>= refine_elf64_executable_file4 + +(** [elf32_construct_image f5] constructs a memory image from an elf32_executable5 object + * [f5]. The function returns the following: + * * A list of bytes with a corresponding address where they should be located + * in the program image and, + * * The entry point for the process. All addresses in the aforementioned list + * should be interpreted wrt this address. + * [construct_image] fails if a loadable segment has a memory size smaller than + * its associated file size, an error according to the ELF spec. This should + * never happen as relevant checks are made when refining an elf_executable_file4 + * into an elf_executable_file5. The function may also fail if there are no loadable + * segments in this executable file, again an error. + * By the ELF specification, you may assume that the list of bitstring, elf32_addr + * pairs is sorted ascending on the second component, i.e. that all pairs are in + * order of the address at which point they should be loaded in memory. + *) +val elf32_construct_image : elf32_executable_file5 -> error (list (bitstring * nat) * nat) +let elf32_construct_image f5 = + let segs = f5.elf32_executable_file5_segments in + let entr = f5.elf32_executable_file5_header.elf32_entry in + match List.filter (fun sg -> sg.elf32_segment_type = elf_pt_load) segs with + | [] -> fail "elf32_construct_image: an executable ELF file must have at least one loadable segment" + | load -> + mapM (fun sg -> + if sg.elf32_segment_memsz = 0 then + return [] + else if sg.elf32_segment_memsz = sg.elf32_segment_size then + return [(sg.elf32_segment_body, sg.elf32_segment_base)] + else if sg.elf32_segment_size < sg.elf32_segment_memsz then + (* Cannot be negative due to check in constructing [f5]. *) + let diff = sg.elf32_segment_memsz - sg.elf32_segment_size in + let zeros = Bitstring.zeros diff in + let addr = sg.elf32_segment_base + sg.elf32_segment_size in + return [(sg.elf32_segment_body, sg.elf32_segment_base); (zeros, addr)] + else + fail "elf32_construct_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf32_addr entr) + end + +(** [elf64_construct_image f5] constructs a memory image from an elf64_executable5 object + * [f5]. The function returns the following: + * * A list of bytes with a corresponding address where they should be located + * in the program image and, + * * The entry point for the process. All addresses in the aforementioned list + * should be interpreted wrt this address. + * [construct_image] fails if a loadable segment has a memory size smaller than + * its associated file size, an error according to the ELF spec. This should + * never happen as relevant checks are made when refining an elf_executable_file4 + * into an elf_executable_file5. The function may also fail if there are no loadable + * segments in this executable file, again an error. + * By the ELF specification, you may assume that the list of bitstring, elf32_addr + * pairs is sorted ascending on the second component, i.e. that all pairs are in + * order of the address at which point they should be loaded in memory. + *) +val elf64_construct_image : elf64_executable_file5 -> error (list (bitstring * nat) * nat) +let elf64_construct_image f5 = + let segs = f5.elf64_executable_file5_segments in + let entr = f5.elf64_executable_file5_header.elf64_entry in + match List.filter (fun sg -> sg.elf64_segment_type = elf_pt_load) segs with + | [] -> fail "elf64_construct_image: an executable ELF file must have at least one loadable segment" + | load -> + mapM (fun sg -> + if sg.elf64_segment_memsz = 0 then + return [] + else if sg.elf64_segment_memsz = sg.elf64_segment_size then + return [(sg.elf64_segment_body, sg.elf64_segment_base)] + else if sg.elf64_segment_size < sg.elf64_segment_memsz then + (* Cannot be negative due to check in constructing [f5]. *) + let diff = sg.elf64_segment_memsz - sg.elf64_segment_size in + let zeros = Bitstring.zeros diff in + let addr = sg.elf64_segment_base + sg.elf64_segment_size in + return [(sg.elf64_segment_body, sg.elf64_segment_base); (zeros, addr)] + else + fail "elf64_construct_image: invariant invalidated") load >>= fun bs_base -> + return (List.concat bs_base, nat_of_elf64_addr entr) + end + +(** [string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string + * representation of elf32_executable_file5 [f5] using user-supplied print bundles. + *) +val string_of_elf32_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file5 -> string +let string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5 = + let sht = + match f5.elf32_executable_file5_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf32_section_header_table' sht_bdl f5.elf32_executable_file5_section_header_string_table sht + end + in + unlines [ + "\n*Type elf32_executable_file5" + ; "**Header" + ; string_of_elf32_header hdr_bdl f5.elf32_executable_file5_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f5.elf32_executable_file5_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf32_executable_file5_section_header_string_table)) + ; "**Interpreted segments:" + ; unlines (List.map (fun x -> "\n" ^ string_of_elf32_interpreted_segment x) f5.elf32_executable_file5_segments) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf32_executable_file5_body) + ] + +(** [string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string + * representation of elf64_executable_file5 [f5] using user-supplied print bundles. + *) +val string_of_elf64_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file5 -> string +let string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5 = + let sht = + match f5.elf64_executable_file5_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf64_section_header_table' sht_bdl f5.elf64_executable_file5_section_header_string_table sht + end + in + unlines [ + "\n*Type elf64_executable_file5" + ; "**Header" + ; string_of_elf64_header hdr_bdl f5.elf64_executable_file5_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f5.elf64_executable_file5_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf64_executable_file5_section_header_string_table)) + ; "**Interpreted segments:" + ; unlines (List.map (fun x -> "\n" ^ string_of_elf64_interpreted_segment x) f5.elf64_executable_file5_segments) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf64_executable_file5_body) + ]
\ No newline at end of file |