From 32a6fcb12814550633261960b540ffeb8a0fcab5 Mon Sep 17 00:00:00 2001 From: varobert Date: Wed, 4 Apr 2012 11:59:40 +0000 Subject: Added safety to potentially overflowing arithmetics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/ELF_parsers.ml | 117 ++++++++++++++++++++++++----------------------- 1 file changed, 61 insertions(+), 56 deletions(-) (limited to 'checklink/ELF_parsers.ml') diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml index c71ff00..ba04c68 100644 --- a/checklink/ELF_parsers.ml +++ b/checklink/ELF_parsers.ml @@ -17,24 +17,24 @@ let elfdata_to_endian (e: elfdata): Bitstring.endian = (** Parses an elf32 header *) let read_elf32_ehdr (bs: bitstring): elf32_ehdr = bitmatch bs with - | { e_ident : 16*8 : bitstring ; - rest : -1 : bitstring } -> + | { e_ident : 16*8 : bitstring ; + rest : -1 : bitstring } -> ( bitmatch e_ident with - | { 0x7F : 8 ; - "ELF" : 24 : string ; - ei_class : 8 : int ; - ei_data : 8 : int ; - ei_version : 8 : int ; - padding : 72 : bitstring } -> + | { 0x7F : 8 ; + "ELF" : 24 : string ; + ei_class : 8 : int ; + ei_data : 8 : int ; + ei_version : 8 : int ; + padding : 72 : bitstring } -> assert (is_zeros padding 72); - let ei_data = ( - match ei_data with + let ei_data = + begin match ei_data with | 0 -> ELFDATANONE | 1 -> ELFDATA2LSB | 2 -> ELFDATA2MSB | _ -> ELFDATAUNKNOWN - ) + end in let e = elfdata_to_endian ei_data in ( @@ -59,32 +59,32 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = { e_ident = { - ei_class = ( - match ei_class with + ei_class = + begin match ei_class with | 0 -> ELFCLASSNONE | 1 -> ELFCLASS32 | 2 -> ELFCLASS64 | _ -> ELFCLASSUNKNOWN - ); + end; ei_data = ei_data; - ei_version = ( - match ei_version with + ei_version = + begin match ei_version with | 0 -> EV_NONE | 1 -> EV_CURRENT | _ -> EV_UNKNOWN - ); + end; }; - e_type = ( - match e_type with + e_type = + begin match e_type with | 0 -> ET_NONE | 1 -> ET_REL | 2 -> ET_EXEC | 3 -> ET_DYN | 4 -> ET_CORE | _ -> ET_UNKNOWN - ); - e_machine = ( - match e_machine with + end; + e_machine = + begin match e_machine with | 0 -> EM_NONE | 1 -> EM_M32 | 2 -> EM_SPARC @@ -96,13 +96,13 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = | 10 -> EM_MIPS_RS4_BE | 20 -> EM_PPC | _ -> EM_UNKNOWN - ); - e_version = ( - match e_version with + end; + e_version = + begin match e_version with | 0l -> EV_NONE | 1l -> EV_CURRENT | _ -> EV_UNKNOWN - ); + end; e_entry = e_entry; e_phoff = e_phoff; e_shoff = e_shoff; @@ -119,22 +119,24 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = (** Returns the file offset of the section header indexed *) let section_header_offset (e_hdr: elf32_ehdr) (sndx: int): int = - int32_int e_hdr.e_shoff + sndx * e_hdr.e_shentsize + Safe.(of_int32 e_hdr.e_shoff + (sndx * e_hdr.e_shentsize)) (** Returns the ndx-th string in the provided bitstring, according to null characters *) let strtab_string (bs: bitstring) (ndx: int): string = let (str, ofs, _) = bs in - let start = (ofs/8 + ndx) in + let start = (ofs / 8 + ndx) in String.sub str start (String.index_from str start '\000' - start) (** Reads an ELF section header *) let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) (num: int): elf32_shdr = let e = elfdata_to_endian e_hdr.e_ident.ei_data in - let byte_ofs = section_header_offset e_hdr num in + let bit_ofs = Safe.( + (section_header_offset e_hdr num) * 8 + ) in bitmatch bs with - | { sh_name : 32 : endian(e), offset(byte_ofs*8) ; + | { sh_name : 32 : endian(e), offset(bit_ofs) ; sh_type : 32 : endian(e) ; sh_flags : 32 : endian(e) ; sh_addr : 32 : endian(e) ; @@ -145,9 +147,9 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) sh_addralign : 32 : endian(e) ; sh_entsize : 32 : endian(e) } -> { - sh_name = strtab_string strtab (int32_int sh_name); - sh_type = ( - match sh_type with + sh_name = strtab_string strtab (Safe32.to_int sh_name); + sh_type = + begin match sh_type with | 0l -> SHT_NULL | 1l -> SHT_PROGBITS | 2l -> SHT_SYMTAB @@ -161,7 +163,7 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) | 10l -> SHT_SHLIB | 11l -> SHT_DYNSYM | _ -> SHT_UNKNOWN - ); + end; sh_flags = sh_flags ; sh_addr = sh_addr ; sh_offset = sh_offset ; @@ -173,12 +175,13 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) } (** Reads an elf program header *) -let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) - : elf32_phdr = +let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int): elf32_phdr = let e = elfdata_to_endian e_hdr.e_ident.ei_data in - let phdr_ofs = int32_int e_hdr.e_phoff + ndx * e_hdr.e_phentsize in + let bit_ofs = Safe.( + ((of_int32 e_hdr.e_phoff) + (ndx * e_hdr.e_phentsize)) * 8 + ) in bitmatch bs with - | { p_type : 32 : endian(e), offset(phdr_ofs*8) ; + | { p_type : 32 : endian(e), offset(bit_ofs) ; p_offset : 32 : endian(e) ; p_vaddr : 32 : endian(e) ; p_paddr : 32 : endian(e) ; @@ -187,8 +190,8 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) p_flags : 32 : bitstring ; p_align : 32 : endian(e) } -> { - p_type = ( - match p_type with + p_type = + begin match p_type with | 0l -> PT_NULL | 1l -> PT_LOAD | 2l -> PT_DYNAMIC @@ -197,7 +200,7 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) | 5l -> PT_SHLIB | 6l -> PT_PHDR | _ -> PT_UNKNOWN - ); + end; p_offset = p_offset ; p_vaddr = p_vaddr ; p_paddr = p_paddr ; @@ -211,8 +214,9 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) (num: int): elf32_sym = let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let bit_ofs = Safe.(num * 128) in (* each symbol takes 16 bytes = 128 bits *) bitmatch symtab with - | { st_name : 32 : endian(e), offset(num*16*8) ; + | { st_name : 32 : endian(e), offset(bit_ofs) ; st_value : 32 : endian(e) ; st_size : 32 : endian(e) ; st_bind : 4 ; @@ -220,30 +224,30 @@ let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) st_other : 8 ; st_shndx : 16 : endian(e) } -> { - st_name = strtab_string strtab (int32_int st_name) ; + st_name = strtab_string strtab (Safe32.to_int st_name) ; st_value = st_value ; st_size = st_size ; - st_bind = ( - match st_bind with + st_bind = + begin match st_bind with | 0 -> STB_LOCAL | 1 -> STB_GLOBAL | 2 -> STB_WEAK | _ -> STB_UNKNOWN - ); - st_type = ( - match st_type with + end; + st_type = + begin match st_type with | 0 -> STT_NOTYPE | 1 -> STT_OBJECT | 2 -> STT_FUNC | 3 -> STT_SECTION | 4 -> STT_FILE | _ -> STT_UNKNOWN - ); + end; st_other = st_other ; st_shndx = st_shndx ; } -(** Aborts if two sections overlap *) +(** Abort if two sections overlap *) let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = let intersect a asize b bsize = asize <> 0l && bsize <> 0l && @@ -263,9 +267,9 @@ let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = if ai_intersects 0l 52l (* ELF header *) || ai_intersects ehdr.e_phoff - (int_int32 (ehdr.e_phnum * ehdr.e_phentsize)) + (Int32.of_int (ehdr.e_phnum * ehdr.e_phentsize)) || ai_intersects ehdr.e_shoff - (int_int32 (ehdr.e_shnum * ehdr.e_shentsize)) + (Int32.of_int (ehdr.e_shnum * ehdr.e_shentsize)) then assert false else Array.iteri @@ -288,10 +292,11 @@ let read_elf_bs (bs: bitstring): elf = let e = elfdata_to_endian e_hdr.e_ident.ei_data in let strtab_sndx = e_hdr.e_shstrndx in let strtab_shofs = section_header_offset e_hdr strtab_sndx in + let skipped_bits = Safe.(strtab_shofs * 8 + 128) in bitmatch bs with - | { ofs : 32 : endian(e), offset(strtab_shofs * 8 + 128) ; + | { ofs : 32 : endian(e), offset(skipped_bits) ; size : 32 : endian(e) } -> - Bitstring.subbitstring bs (int32_int ofs * 8) (int32_int size * 8) + Bitstring.subbitstring bs Safe.(of_int32 ofs * 8) Safe.(of_int32 size * 8) ) in let e_shdra = @@ -307,11 +312,11 @@ let read_elf_bs (bs: bitstring): elf = e_symtab = ( let symtab_shdr = e_shdra.(symtab_sndx) in let symtab_strtab_sndx = symtab_shdr.sh_link in - let symtab_nb_ent = (int32_int symtab_shdr.sh_size / 16) in + let symtab_nb_ent = (Safe32.to_int symtab_shdr.sh_size / 16) in Array.init symtab_nb_ent (read_elf32_sym e_hdr (section_bitstring_noelf bs e_shdra symtab_sndx) - (section_bitstring_noelf bs e_shdra (int32_int symtab_strtab_sndx))) + (section_bitstring_noelf bs e_shdra (Safe32.to_int symtab_strtab_sndx))) ); e_symtab_sndx = symtab_sndx; } -- cgit v1.2.3