package linksem

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

Source file gnu_ext_note.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
(*Generated by Lem from gnu_extensions/gnu_ext_note.lem.*)
(** [gnu_ext_note] contains GNU extension specific definitions relating to the
  * .note section/segment of an ELF file.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_string

open Byte_sequence
open Endianness
open Error
open Missing_pervasives
open String_table

open Elf_note
open Elf_section_header_table
open Elf_types_native_uint

open Gnu_ext_section_header_table

(** The following two functions are utility functions to convert a list of bytes
  * into words, ready for further processing into strings.
  *)

(*val group_elf32_words : endianness -> list byte -> error (list elf32_word)*)
let rec group_elf32_words endian xs:((Uint32_wrapper.uint32)list)error=
   ((match xs with
    | []                 -> return []
    | x1::x2::x3::x4::xs ->
      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in bind (read_elf32_word   endian bs0) (fun (w, _) ->  bind (group_elf32_words endian xs) (fun ws ->
      return (w::ws)))
    | xs                 -> fail "group_elf32_words: the impossible happened"
  ))

(*val group_elf64_words : endianness -> list byte -> error (list elf64_word)*)
let rec group_elf64_words endian xs:((Uint32_wrapper.uint32)list)error=
   ((match xs with
    | []                 -> return []
    | x1::x2::x3::x4::xs ->
      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in bind (read_elf64_word   endian bs0) (fun (w, _) ->  bind (group_elf64_words endian xs) (fun ws ->
      return (w::ws)))
    | xs                 -> fail "group_elf64_words: the impossible happened"
  ))

(** [gnu_ext_check_elf32_abi_note_tag_section endain sht stbl bs0] checks the
  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
  * extensions.  The string in this note should contain the string "GNU".
  *)
(*val gnu_ext_check_elf32_abi_note_tag_section : endianness -> elf32_section_header_table ->
  string_table -> byte_sequence -> bool*)
let gnu_ext_check_elf32_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf32_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint32_wrapper.to_bigint note.elf32_sh_offset) in
        let siz = (Uint32_wrapper.to_bigint note.elf32_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf32_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> false
            | Success abi_tag ->
              let str = (name_string_of_elf32_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then
                    if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then Nat_big_num.greater_equal
                      (Byte_sequence.length0 abi_tag.elf32_note_desc)( (Nat_big_num.of_int 16))
                    else
                      true
                  else
                    false
                else
                  false
          )
      | _      ->
          false
    ))

(** [gnu_ext_check_elf64_abi_note_tag_section endain sht stbl bs0] checks the
  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
  * extensions.  The string in this note should contain the string "GNU".
  *)
(*val gnu_ext_check_elf64_abi_note_tag_section : endianness -> elf64_section_header_table ->
  string_table -> byte_sequence -> bool*)
let gnu_ext_check_elf64_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf64_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint64_wrapper.to_bigint note.elf64_sh_offset) in
        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf64_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> false
            | Success abi_tag ->
              let str = (name_string_of_elf64_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf64_note_descsz)( (Nat_big_num.of_int 16)) then Nat_big_num.greater_equal
                    (Byte_sequence.length0 abi_tag.elf64_note_desc)( (Nat_big_num.of_int 16))
                  else
                    false
                else
                  false
          )
      | _      ->
          false
    ))

(** [gnu_ext_extract_elf32_earliest_compatible_kernel end sht stab bs0] extracts
  * the earliest compatible Linux kernel with the given ELF file from its section
  * header table [sht], and string table [stbl], assuming endianness [endian].
  * NB: marked as OCaml only as need to extract a string from integers.
  * TODO: implement some string parsing functions in Isabelle/HOL so things like
  * this can be extracted.
  *)
(*val gnu_ext_extract_elf32_earliest_compatible_kernel : endianness -> elf32_section_header_table ->
  string_table -> byte_sequence -> error string*)
let gnu_ext_extract_elf32_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf32_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint32_wrapper.to_bigint note.elf32_sh_offset) in
        let siz = (Uint32_wrapper.to_bigint note.elf32_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf32_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: parsing of NOTE section failed"
            | Success abi_tag ->
              let str = (name_string_of_elf32_note abi_tag) in
                if str = "GNU\000" then
                if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then
                  (match Byte_sequence.takebytes( (Nat_big_num.of_int 16)) abi_tag.elf32_note_desc with
                    | Fail _ -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: the impossible happened"
                    | Success take2 ->
                      (match group_elf32_words endian (Byte_sequence.byte_list_of_byte_sequence take2) with
                        | Fail err   -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: word grouping failed"
                        | Success ss ->
                          (match ss with
                            | c1::c2::c3::cs ->
                              let c1 = (Uint32_wrapper.to_string c1) in
                              let c2 = (Uint32_wrapper.to_string c2) in
                              let c3 = (Uint32_wrapper.to_string c3) in
                                return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
                            | _              -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: kernel version must have three components"
                          )
                      )
                  )
                else
                  fail "gnu_ext_extract_elf32_earliest_compatible_kernel: .note.ABI-tag description size not required length"
                else
                  fail "gnu_ext_extract_elf32_earliest_compatible_kernel: required GNU string not present"
          )
      | _      -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: more than one .note.ABI-tag section present"
    ))

(** [gnu_ext_extract_elf64_earliest_compatible_kernel end sht stab bs0] extracts
  * the earliest compatible Linux kernel with the given ELF file from its section
  * header table [sht], and string table [stbl], assuming endianness [endian].
  * NB: marked as OCaml only as need to extract a string from integers.
  * TODO: implement some string parsing functions in Isabelle/HOL so things like
  * this can be extracted.
  *)
(*val gnu_ext_extract_elf64_earliest_compatible_kernel : endianness -> elf64_section_header_table ->
  string_table -> byte_sequence -> error string*)
let gnu_ext_extract_elf64_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf64_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint64_wrapper.to_bigint note.elf64_sh_offset) in
        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf64_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: parsing of NOTE section failed"
            | Success abi_tag ->
              let str = (name_string_of_elf64_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf64_note_descsz)( (Nat_big_num.of_int 16)) then
                    (match Byte_sequence.takebytes( (Nat_big_num.of_int 16)) abi_tag.elf64_note_desc with
                      | Fail _ -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: the impossible happened"
                      | Success take2 ->
                        (match group_elf64_words endian (Byte_sequence.byte_list_of_byte_sequence take2) with
                          | Fail err   -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: word grouping failed"
                          | Success ss ->
                            (match ss with
                              | c1::c2::c3::cs ->
                                let c1 = (Uint32_wrapper.to_string c1) in
                                let c2 = (Uint32_wrapper.to_string c2) in
                                let c3 = (Uint32_wrapper.to_string c3) in
                                  return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
                              | _              -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: kernel version must have three components"
                            )
                        )
                    )
                  else
                    fail "gnu_ext_extract_elf64_earliest_compatible_kernel: .note.ABI-tag description size not required length"
                else
                  fail "gnu_ext_extract_elf64_earliest_compatible_kernel: required GNU string not present"
          )
      | _      -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: more than one .note.ABI-tag section present"
    ))
OCaml

Innovation. Community. Security.