From 8af4d1d3a74960e2c71f80d581b03ba26d8495a5 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Mon, 4 Apr 2022 11:42:53 -0600 Subject: [PATCH] Validate input ELF file using Everparse. Everparse generated files are checked in until #834 is fixed. Signed-off-by: Alan Jowett --- .gitmodules | 3 + ebpf-for-windows.sln | 37 + scripts/.check-license.ignore | 1 + spec/Directory.Build.props | 39 + spec/elf/Elf.c | 1982 +++++++++++++++++++++++++ spec/elf/Elf.h | 157 ++ spec/elf/ElfWrapper.c | 33 + spec/elf/ElfWrapper.h | 10 + spec/elf/EverParse.h | 192 +++ spec/elf/EverParseEndianness.h | 110 ++ spec/elf/elf.vcxproj | 158 ++ spec/elf/elf.vcxproj.filters | 39 + spec/spec.md | 8 + tests/bpf2c_tests/bpf2c_tests.vcxproj | 4 +- tools/bpf2c/bpf2c.cpp | 28 +- tools/bpf2c/bpf2c.vcxproj | 10 +- tools/bpf2c/bpf2c.vcxproj.filters | 3 + tools/bpf2c/bpf_code_generator.cpp | 6 +- tools/bpf2c/bpf_code_generator.h | 4 +- 19 files changed, 2812 insertions(+), 12 deletions(-) create mode 100644 spec/Directory.Build.props create mode 100644 spec/elf/Elf.c create mode 100644 spec/elf/Elf.h create mode 100644 spec/elf/ElfWrapper.c create mode 100644 spec/elf/ElfWrapper.h create mode 100644 spec/elf/EverParse.h create mode 100644 spec/elf/EverParseEndianness.h create mode 100644 spec/elf/elf.vcxproj create mode 100644 spec/elf/elf.vcxproj.filters create mode 100644 spec/spec.md diff --git a/.gitmodules b/.gitmodules index 1103384249..1d56acdb73 100644 --- a/.gitmodules +++ b/.gitmodules @@ -20,3 +20,6 @@ [submodule "external/parcon"] path = external/parcon url = https://github.com/javawizard/parcon.git +[submodule "external/everparse"] + path = external/everparse + url = https://github.com/project-everest/everparse.git diff --git a/ebpf-for-windows.sln b/ebpf-for-windows.sln index 3042b71f95..b2ab8713ac 100644 --- a/ebpf-for-windows.sln +++ b/ebpf-for-windows.sln @@ -152,13 +152,21 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "droppacket_km", "tests\samp EndProjectSection EndProject Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "bindmonitor_km", "tests\sample\generated\sys\bindmonitor_km\bindmonitor_sys.vcxproj", "{34481DE6-D212-41A6-8F46-34959FF66B9A}" + ProjectSection(ProjectDependencies) = postProject + {69B97E52-18DC-434E-A6E4-4C0F3E88C44A} = {69B97E52-18DC-434E-A6E4-4C0F3E88C44A} + EndProjectSection EndProject Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "bindmonitor_tailcall_km", "tests\sample\generated\sys\bindmonitor_tailcall_km\bindmonitor_tailcall_sys.vcxproj", "{2B51E0EF-4589-430B-9CCC-D09A4E6FD8B2}" + ProjectSection(ProjectDependencies) = postProject + {69B97E52-18DC-434E-A6E4-4C0F3E88C44A} = {69B97E52-18DC-434E-A6E4-4C0F3E88C44A} + EndProjectSection EndProject Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "Catch2WithMain", "external\Catch2\build\src\Catch2WithMain.vcxproj", "{8BD3552A-2CFB-4A59-AB15-2031B97ADA1E}" EndProject Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "Catch2", "external\Catch2\build\src\Catch2.vcxproj", "{8D538CBE-01BF-4A2E-A98A-6C368FDF13D7}" EndProject +Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "spec_elf", "spec\elf\elf.vcxproj", "{E2B1C5CE-99D2-4732-ACFB-0133F31A450F}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|ARM = Debug|ARM @@ -1493,6 +1501,34 @@ Global {8D538CBE-01BF-4A2E-A98A-6C368FDF13D7}.RelWithDebInfo|x64.ActiveCfg = RelWithDebInfo|x64 {8D538CBE-01BF-4A2E-A98A-6C368FDF13D7}.RelWithDebInfo|x64.Build.0 = RelWithDebInfo|x64 {8D538CBE-01BF-4A2E-A98A-6C368FDF13D7}.RelWithDebInfo|x86.ActiveCfg = RelWithDebInfo|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|ARM.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|ARM64.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|x64.ActiveCfg = Debug|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|x64.Build.0 = Debug|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|x86.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Debug|x86.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|ARM.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|ARM.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|ARM64.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|ARM64.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|x64.ActiveCfg = Debug|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|x64.Build.0 = Debug|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|x86.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.MinSizeRel|x86.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|ARM.ActiveCfg = Release|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|ARM64.ActiveCfg = Release|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|x64.ActiveCfg = Release|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|x64.Build.0 = Release|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|x86.ActiveCfg = Release|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.Release|x86.Build.0 = Release|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|ARM.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|ARM.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|ARM64.ActiveCfg = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|ARM64.Build.0 = Debug|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|x64.ActiveCfg = Release|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|x64.Build.0 = Release|x64 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|x86.ActiveCfg = Release|Win32 + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F}.RelWithDebInfo|x86.Build.0 = Release|Win32 EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE @@ -1546,6 +1582,7 @@ Global {2B51E0EF-4589-430B-9CCC-D09A4E6FD8B2} = {5C9E1337-D8EF-41AB-815D-E1990D19E4E0} {8BD3552A-2CFB-4A59-AB15-2031B97ADA1E} = {492C9B22-9237-4996-9E33-CA14D3533616} {8D538CBE-01BF-4A2E-A98A-6C368FDF13D7} = {492C9B22-9237-4996-9E33-CA14D3533616} + {E2B1C5CE-99D2-4732-ACFB-0133F31A450F} = {69CDB6A1-434D-4BC9-9BFF-D12DF7EDBB6B} EndGlobalSection GlobalSection(ExtensibilityGlobals) = postSolution SolutionGuid = {3D5F862D-74C6-4357-9F95-0B152E33B7B8} diff --git a/scripts/.check-license.ignore b/scripts/.check-license.ignore index 9f9241be4f..f990716bd3 100644 --- a/scripts/.check-license.ignore +++ b/scripts/.check-license.ignore @@ -10,6 +10,7 @@ # Generated files tools/netsh/resource.h +spec/* # Other Files LICENSE.txt diff --git a/spec/Directory.Build.props b/spec/Directory.Build.props new file mode 100644 index 0000000000..d2afe5ac1a --- /dev/null +++ b/spec/Directory.Build.props @@ -0,0 +1,39 @@ + + + + + + + $(SolutionDir)external\Analyze.external.ruleset + + + true + + + + true + Level4 + stdcpplatest + false + true + false + ProgramDatabase + true + + + + + MultiThreadedDLL + + + + + true + true + MultiThreadedDebugDLL + + + \ No newline at end of file diff --git a/spec/elf/Elf.c b/spec/elf/Elf.c new file mode 100644 index 0000000000..582bab38e7 --- /dev/null +++ b/spec/elf/Elf.c @@ -0,0 +1,1982 @@ + + +#include "Elf.h" + +static inline uint64_t +ValidateZeroByte( + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + /* Validating field zero */ + /* Checking that we have enough space for a UINT8, i.e., 1 byte */ + BOOLEAN hasBytes = (uint64_t)1U <= (InputLength - StartPosition); + uint64_t positionAfterzero_refinement; + if (hasBytes) { + positionAfterzero_refinement = StartPosition + (uint64_t)1U; + } else { + positionAfterzero_refinement = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); + } + uint64_t positionAfterZeroByte; + if (EverParseIsError(positionAfterzero_refinement)) { + positionAfterZeroByte = positionAfterzero_refinement; + } else { + /* reading field_value */ + uint8_t zero_refinement = Input[(uint32_t)StartPosition]; + /* start: checking constraint */ + BOOLEAN zero_refinementConstraintIsOk = zero_refinement == (uint8_t)0U; + /* end: checking constraint */ + positionAfterZeroByte = EverParseCheckConstraintOk(zero_refinementConstraintIsOk, positionAfterzero_refinement); + } + if (EverParseIsSuccess(positionAfterZeroByte)) { + return positionAfterZeroByte; + } + Err("_ZeroByte", + "zero.refinement", + EverParseErrorReasonOfResult(positionAfterZeroByte), + Ctxt, + Input, + StartPosition); + return positionAfterZeroByte; +} + +static inline uint64_t +ValidateEIdent( + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + /* Checking that we have enough space for a UINT8, i.e., 1 byte */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - StartPosition); + uint64_t positionAfternone; + if (hasBytes0) { + positionAfternone = StartPosition + (uint64_t)1U; + } else { + positionAfternone = EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); + } + uint64_t positionAfterEIdent; + if (EverParseIsError(positionAfternone)) { + positionAfterEIdent = positionAfternone; + } else { + uint8_t none = Input[(uint32_t)StartPosition]; + BOOLEAN noneConstraintIsOk = none == ELF____ELFMAG0; + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterEIdent = positionAfternone1; + } else { + /* Checking that we have enough space for a UINT8, i.e., 1 byte */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - positionAfternone1); + uint64_t positionAfternone2; + if (hasBytes0) { + positionAfternone2 = positionAfternone1 + (uint64_t)1U; + } else { + positionAfternone2 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } + uint64_t positionAfterEIdent0; + if (EverParseIsError(positionAfternone2)) { + positionAfterEIdent0 = positionAfternone2; + } else { + uint8_t none1 = Input[(uint32_t)positionAfternone1]; + BOOLEAN noneConstraintIsOk1 = none1 == ELF____ELFMAG1; + uint64_t positionAfternone3 = EverParseCheckConstraintOk(noneConstraintIsOk1, positionAfternone2); + if (EverParseIsError(positionAfternone3)) { + positionAfterEIdent0 = positionAfternone3; + } else { + /* Checking that we have enough space for a UINT8, i.e., 1 + * byte */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - positionAfternone3); + uint64_t positionAfternone4; + if (hasBytes0) { + positionAfternone4 = positionAfternone3 + (uint64_t)1U; + } else { + positionAfternone4 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone3); + } + uint64_t positionAfterEIdent; + if (EverParseIsError(positionAfternone4)) { + positionAfterEIdent = positionAfternone4; + } else { + uint8_t none2 = Input[(uint32_t)positionAfternone3]; + BOOLEAN noneConstraintIsOk2 = none2 == ELF____ELFMAG2; + uint64_t positionAfternone5 = + EverParseCheckConstraintOk(noneConstraintIsOk2, positionAfternone4); + if (EverParseIsError(positionAfternone5)) { + positionAfterEIdent = positionAfternone5; + } else { + /* Checking that we have enough space for a UINT8, + * i.e., 1 byte */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - positionAfternone5); + uint64_t positionAfternone6; + if (hasBytes0) { + positionAfternone6 = positionAfternone5 + (uint64_t)1U; + } else { + positionAfternone6 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone5); + } + uint64_t positionAfterEIdent0; + if (EverParseIsError(positionAfternone6)) { + positionAfterEIdent0 = positionAfternone6; + } else { + uint8_t none3 = Input[(uint32_t)positionAfternone5]; + BOOLEAN noneConstraintIsOk3 = none3 == ELF____ELFMAG3; + uint64_t positionAfternone7 = + EverParseCheckConstraintOk(noneConstraintIsOk3, positionAfternone6); + if (EverParseIsError(positionAfternone7)) { + positionAfterEIdent0 = positionAfternone7; + } else { + /* Checking that we have enough space for a + * UINT8, i.e., 1 byte */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - positionAfternone7); + uint64_t positionAfternone8; + if (hasBytes0) { + positionAfternone8 = positionAfternone7 + (uint64_t)1U; + } else { + positionAfternone8 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone7); + } + uint64_t positionAfterEIdent; + if (EverParseIsError(positionAfternone8)) { + positionAfterEIdent = positionAfternone8; + } else { + uint8_t none4 = Input[(uint32_t)positionAfternone7]; + BOOLEAN + noneConstraintIsOk4 = + none4 == ELF____ELFCLASS64 && + (ELF____ELFCLASSNONE == none4 || ELF____ELFCLASS32 == none4 || + ELF____ELFCLASS64 == none4); + uint64_t positionAfternone9 = + EverParseCheckConstraintOk(noneConstraintIsOk4, positionAfternone8); + if (EverParseIsError(positionAfternone9)) { + positionAfterEIdent = positionAfternone9; + } else { + /* This 3d spec applies to 64-bit + * only currently */ + /* Checking that we have enough + * space for a UINT8, i.e., 1 byte + */ + BOOLEAN hasBytes0 = (uint64_t)1U <= (InputLength - positionAfternone9); + uint64_t positionAfterFIVE_refinement; + if (hasBytes0) { + positionAfterFIVE_refinement = positionAfternone9 + (uint64_t)1U; + } else { + positionAfterFIVE_refinement = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone9); + } + uint64_t positionAfterEIdent0; + if (EverParseIsError(positionAfterFIVE_refinement)) { + positionAfterEIdent0 = positionAfterFIVE_refinement; + } else { + /* reading field_value */ + uint8_t fIVE_refinement = Input[(uint32_t)positionAfternone9]; + /* start: checking constraint */ + BOOLEAN + fIVE_refinementConstraintIsOk = ELF____ELFDATANONE == fIVE_refinement || + ELF____ELFDATA2LSB == fIVE_refinement || + ELF____ELFDATA2MSB == fIVE_refinement; + /* end: checking constraint */ + positionAfterEIdent0 = EverParseCheckConstraintOk( + fIVE_refinementConstraintIsOk, positionAfterFIVE_refinement); + } + uint64_t positionAfterFIVE_refinement0; + if (EverParseIsSuccess(positionAfterEIdent0)) { + positionAfterFIVE_refinement0 = positionAfterEIdent0; + } else { + Err("_E_IDENT", + "FIVE.refinement", + EverParseErrorReasonOfResult(positionAfterEIdent0), + Ctxt, + Input, + positionAfternone9); + positionAfterFIVE_refinement0 = positionAfterEIdent0; + } + if (EverParseIsError(positionAfterFIVE_refinement0)) { + positionAfterEIdent = positionAfterFIVE_refinement0; + } else { + /* Checking that we have enough + * space for a UINT8, i.e., 1 + * byte */ + BOOLEAN + hasBytes0 = + (uint64_t)1U <= (InputLength - positionAfterFIVE_refinement0); + uint64_t positionAfternone10; + if (hasBytes0) { + positionAfternone10 = positionAfterFIVE_refinement0 + (uint64_t)1U; + } else { + positionAfternone10 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfterFIVE_refinement0); + } + uint64_t positionAfterEIdent0; + if (EverParseIsError(positionAfternone10)) { + positionAfterEIdent0 = positionAfternone10; + } else { + uint8_t none5 = Input[(uint32_t)positionAfterFIVE_refinement0]; + BOOLEAN + noneConstraintIsOk5 = none5 == (uint8_t)1U; + uint64_t positionAfternone11 = EverParseCheckConstraintOk( + noneConstraintIsOk5, positionAfternone10); + if (EverParseIsError(positionAfternone11)) { + positionAfterEIdent0 = positionAfternone11; + } else { + /* ELF specification + * version is always set + * to 1 */ + /* Checking that we have + * enough space for a + * UINT8, i.e., 1 byte + */ + BOOLEAN hasBytes0 = + (uint64_t)1U <= (InputLength - positionAfternone11); + uint64_t positionAfterSEVEN_refinement; + if (hasBytes0) { + positionAfterSEVEN_refinement = + positionAfternone11 + (uint64_t)1U; + } else { + positionAfterSEVEN_refinement = + EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfternone11); + } + uint64_t positionAfterEIdent; + if (EverParseIsError(positionAfterSEVEN_refinement)) { + positionAfterEIdent = positionAfterSEVEN_refinement; + } else { + /* reading + * field_value */ + uint8_t sEVEN_refinement = + Input[(uint32_t)positionAfternone11]; + /* start: checking + * constraint */ + BOOLEAN + sEVEN_refinementConstraintIsOk = + ELF____ELFOSABI_NONE == sEVEN_refinement || + ELF____ELFOSABI_SYSV == sEVEN_refinement || + ELF____ELFOSABI_HPUX == sEVEN_refinement || + ELF____ELFOSABI_NETBSD == sEVEN_refinement || + ELF____ELFOSABI_LINUX == sEVEN_refinement || + ELF____ELFOSABI_SOLARIS == sEVEN_refinement || + ELF____ELFOSABI_IRIX == sEVEN_refinement || + ELF____ELFOSABI_FREEBSD == sEVEN_refinement || + ELF____ELFOSABI_TRU64 == sEVEN_refinement || + ELF____ELFOSABI_ARM == sEVEN_refinement || + ELF____ELFOSABI_STANDALONE == sEVEN_refinement; + /* end: checking + * constraint */ + positionAfterEIdent = EverParseCheckConstraintOk( + sEVEN_refinementConstraintIsOk, + positionAfterSEVEN_refinement); + } + uint64_t positionAfterSEVEN_refinement0; + if (EverParseIsSuccess(positionAfterEIdent)) { + positionAfterSEVEN_refinement0 = positionAfterEIdent; + } else { + Err("_E_IDENT", + "SEVEN." + "refinement", + EverParseErrorReasonOfResult(positionAfterEIdent), + Ctxt, + Input, + positionAfternone11); + positionAfterSEVEN_refinement0 = positionAfterEIdent; + } + if (EverParseIsError(positionAfterSEVEN_refinement0)) { + positionAfterEIdent0 = positionAfterSEVEN_refinement0; + } else { + /* Validating field + * EIGHT */ + /* Checking that we + * have enough space + * for a UINT8, + * i.e., 1 byte */ + BOOLEAN + hasBytes = (uint64_t)1U <= + (InputLength - positionAfterSEVEN_refinement0); + uint64_t positionAfterEIGHT_refinement; + if (hasBytes) { + positionAfterEIGHT_refinement = + positionAfterSEVEN_refinement0 + (uint64_t)1U; + } else { + positionAfterEIGHT_refinement = + EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfterSEVEN_refinement0); + } + uint64_t positionAfterEIdent; + if (EverParseIsError(positionAfterEIGHT_refinement)) { + positionAfterEIdent = positionAfterEIGHT_refinement; + } else { + /* reading + * field_value + */ + uint8_t eIGHT_refinement = + Input[(uint32_t)positionAfterSEVEN_refinement0]; + /* start: + * checking + * constraint */ + BOOLEAN + eIGHT_refinementConstraintIsOk = + eIGHT_refinement == (uint8_t)0U; + /* end: checking + * constraint */ + positionAfterEIdent = EverParseCheckConstraintOk( + eIGHT_refinementConstraintIsOk, + positionAfterEIGHT_refinement); + } + uint64_t positionAfterEIGHT_refinement0; + if (EverParseIsSuccess(positionAfterEIdent)) { + positionAfterEIGHT_refinement0 = positionAfterEIdent; + } else { + Err("_E_IDENT", + "EIGHT." + "refinemen" + "t", + EverParseErrorReasonOfResult(positionAfterEIdent), + Ctxt, + Input, + positionAfterSEVEN_refinement0); + positionAfterEIGHT_refinement0 = positionAfterEIdent; + } + if (EverParseIsError(positionAfterEIGHT_refinement0)) { + positionAfterEIdent0 = positionAfterEIGHT_refinement0; + } else { + /* ABI version, + * always set to + * 0 */ + BOOLEAN + hasEnoughBytes = + (uint64_t)(uint32_t)ELF____E_IDENT_PADDING_SIZE <= + (InputLength - positionAfterEIGHT_refinement0); + uint64_t positionAfterEIdent; + if (!hasEnoughBytes) { + positionAfterEIdent = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfterEIGHT_refinement0); + } else { + uint8_t* truncatedInput = Input; + uint64_t truncatedInputLength = + positionAfterEIGHT_refinement0 + + (uint64_t)(uint32_t)ELF____E_IDENT_PADDING_SIZE; + uint64_t result = positionAfterEIGHT_refinement0; + while (TRUE) { + uint64_t position = *&result; + BOOLEAN + ite; + if (!((uint64_t)1U <= + (truncatedInputLength - position))) { + ite = TRUE; + } else { + uint64_t positionAfterEIdent = + ValidateZeroByte( + Ctxt, + Err, + truncatedInput, + truncatedInputLength, + position); + uint64_t result1; + if (EverParseIsSuccess( + positionAfterEIdent)) { + result1 = positionAfterEIdent; + } else { + Err("_E_IDENT", + "NINE_FIFTEEN.element", + EverParseErrorReasonOfResult( + positionAfterEIdent), + Ctxt, + truncatedInput, + position); + result1 = positionAfterEIdent; + } + result = result1; + ite = EverParseIsError(result1); + } + if (ite) { + break; + } + } + uint64_t res = result; + positionAfterEIdent = res; + } + if (EverParseIsSuccess(positionAfterEIdent)) { + positionAfterEIdent0 = positionAfterEIdent; + } else { + Err("_E_" + "IDENT", + "NINE_" + "FIFTEE" + "N", + EverParseErrorReasonOfResult( + positionAfterEIdent), + Ctxt, + Input, + positionAfterEIGHT_refinement0); + positionAfterEIdent0 = positionAfterEIdent; + } + } + } + } + } + if (EverParseIsSuccess(positionAfterEIdent0)) { + positionAfterEIdent = positionAfterEIdent0; + } else { + Err("_E_IDENT", + "none", + EverParseErrorReasonOfResult(positionAfterEIdent0), + Ctxt, + Input, + positionAfterFIVE_refinement0); + positionAfterEIdent = positionAfterEIdent0; + } + } + } + } + if (EverParseIsSuccess(positionAfterEIdent)) { + positionAfterEIdent0 = positionAfterEIdent; + } else { + Err("_E_IDENT", + "none", + EverParseErrorReasonOfResult(positionAfterEIdent), + Ctxt, + Input, + positionAfternone7); + positionAfterEIdent0 = positionAfterEIdent; + } + } + } + if (EverParseIsSuccess(positionAfterEIdent0)) { + positionAfterEIdent = positionAfterEIdent0; + } else { + Err("_E_IDENT", + "none", + EverParseErrorReasonOfResult(positionAfterEIdent0), + Ctxt, + Input, + positionAfternone5); + positionAfterEIdent = positionAfterEIdent0; + } + } + } + if (EverParseIsSuccess(positionAfterEIdent)) { + positionAfterEIdent0 = positionAfterEIdent; + } else { + Err("_E_IDENT", + "none", + EverParseErrorReasonOfResult(positionAfterEIdent), + Ctxt, + Input, + positionAfternone3); + positionAfterEIdent0 = positionAfterEIdent; + } + } + } + if (EverParseIsSuccess(positionAfterEIdent0)) { + positionAfterEIdent = positionAfterEIdent0; + } else { + Err("_E_IDENT", + "none", + EverParseErrorReasonOfResult(positionAfterEIdent0), + Ctxt, + Input, + positionAfternone1); + positionAfterEIdent = positionAfterEIdent0; + } + } + } + if (EverParseIsSuccess(positionAfterEIdent)) { + return positionAfterEIdent; + } + Err("_E_IDENT", "none", EverParseErrorReasonOfResult(positionAfterEIdent), Ctxt, Input, StartPosition); + return positionAfterEIdent; +} + +static inline uint64_t +ValidateProgramHeaderTableEntry( + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + /* Validating field P_TYPE */ + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - StartPosition); + uint64_t positionAfterProgramHeaderTableEntry; + if (hasBytes0) { + positionAfterProgramHeaderTableEntry = StartPosition + (uint64_t)4U; + } else { + positionAfterProgramHeaderTableEntry = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry)) { + res0 = positionAfterProgramHeaderTableEntry; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_TYPE", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry), + Ctxt, + Input, + StartPosition); + res0 = positionAfterProgramHeaderTableEntry; + } + uint64_t positionAfterPType = res0; + if (EverParseIsError(positionAfterPType)) { + return positionAfterPType; + } + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes1 = (uint64_t)4U <= (InputLength - positionAfterPType); + uint64_t positionAfternone; + if (hasBytes1) { + positionAfternone = positionAfterPType + (uint64_t)4U; + } else { + positionAfternone = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPType); + } + uint64_t positionAfterProgramHeaderTableEntry0; + if (EverParseIsError(positionAfternone)) { + positionAfterProgramHeaderTableEntry0 = positionAfternone; + } else { + uint32_t none = Load32Le(Input + (uint32_t)positionAfterPType); + BOOLEAN noneConstraintIsOk = none <= (uint32_t)(uint8_t)7U; + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterProgramHeaderTableEntry0 = positionAfternone1; + } else { + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfternone1); + uint64_t positionAfterProgramHeaderTableEntry; + if (hasBytes0) { + positionAfterProgramHeaderTableEntry = positionAfternone1 + (uint64_t)8U; + } else { + positionAfterProgramHeaderTableEntry = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } + uint64_t positionAfterPOffset; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry)) { + positionAfterPOffset = positionAfterProgramHeaderTableEntry; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_OFFSET", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry), + Ctxt, + Input, + positionAfternone1); + positionAfterPOffset = positionAfterProgramHeaderTableEntry; + } + if (EverParseIsError(positionAfterPOffset)) { + positionAfterProgramHeaderTableEntry0 = positionAfterPOffset; + } else { + uint64_t pOffset = Load64Le(Input + (uint32_t)positionAfternone1); + /* Validating field P_VADDR */ + /* Checking that we have enough space for a UINT64, i.e., 8 + * bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterPOffset); + uint64_t positionAfterProgramHeaderTableEntry; + if (hasBytes0) { + positionAfterProgramHeaderTableEntry = positionAfterPOffset + (uint64_t)8U; + } else { + positionAfterProgramHeaderTableEntry = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPOffset); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry)) { + res0 = positionAfterProgramHeaderTableEntry; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_VADDR", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry), + Ctxt, + Input, + positionAfterPOffset); + res0 = positionAfterProgramHeaderTableEntry; + } + uint64_t positionAfterPVaddr = res0; + if (EverParseIsError(positionAfterPVaddr)) { + positionAfterProgramHeaderTableEntry0 = positionAfterPVaddr; + } else { + /* Validating field P_PADDR */ + /* Checking that we have enough space for a UINT64, i.e., 8 + * bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterPVaddr); + uint64_t positionAfterProgramHeaderTableEntry; + if (hasBytes0) { + positionAfterProgramHeaderTableEntry = positionAfterPVaddr + (uint64_t)8U; + } else { + positionAfterProgramHeaderTableEntry = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPVaddr); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry)) { + res0 = positionAfterProgramHeaderTableEntry; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_PADDR", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry), + Ctxt, + Input, + positionAfterPVaddr); + res0 = positionAfterProgramHeaderTableEntry; + } + uint64_t positionAfterPPaddr = res0; + if (EverParseIsError(positionAfterPPaddr)) { + positionAfterProgramHeaderTableEntry0 = positionAfterPPaddr; + } else { + /* Checking that we have enough space for a UINT64, + * i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterPPaddr); + uint64_t positionAfternone2; + if (hasBytes0) { + positionAfternone2 = positionAfterPPaddr + (uint64_t)8U; + } else { + positionAfternone2 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPPaddr); + } + uint64_t positionAfterProgramHeaderTableEntry; + if (EverParseIsError(positionAfternone2)) { + positionAfterProgramHeaderTableEntry = positionAfternone2; + } else { + uint64_t none1 = Load64Le(Input + (uint32_t)positionAfterPPaddr); + BOOLEAN noneConstraintIsOk1 = none1 < ElfFileSize && pOffset <= (ElfFileSize - none1); + uint64_t positionAfternone3 = + EverParseCheckConstraintOk(noneConstraintIsOk1, positionAfternone2); + if (EverParseIsError(positionAfternone3)) { + positionAfterProgramHeaderTableEntry = positionAfternone3; + } else { + /* Validating field P_MEMSZ */ + /* Checking that we have enough space for a + * UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfternone3); + uint64_t positionAfterProgramHeaderTableEntry0; + if (hasBytes0) { + positionAfterProgramHeaderTableEntry0 = positionAfternone3 + (uint64_t)8U; + } else { + positionAfterProgramHeaderTableEntry0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone3); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry0)) { + res0 = positionAfterProgramHeaderTableEntry0; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_MEMSZ", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry0), + Ctxt, + Input, + positionAfternone3); + res0 = positionAfterProgramHeaderTableEntry0; + } + uint64_t positionAfterPMemsz = res0; + if (EverParseIsError(positionAfterPMemsz)) { + positionAfterProgramHeaderTableEntry = positionAfterPMemsz; + } else { + /* Validating field P_ALIGN */ + /* Checking that we have enough space for a + * UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes = (uint64_t)8U <= (InputLength - positionAfterPMemsz); + uint64_t positionAfterProgramHeaderTableEntry0; + if (hasBytes) { + positionAfterProgramHeaderTableEntry0 = positionAfterPMemsz + (uint64_t)8U; + } else { + positionAfterProgramHeaderTableEntry0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPMemsz); + } + uint64_t res; + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry0)) { + res = positionAfterProgramHeaderTableEntry0; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "P_ALIGN", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry0), + Ctxt, + Input, + positionAfterPMemsz); + res = positionAfterProgramHeaderTableEntry0; + } + positionAfterProgramHeaderTableEntry = res; + } + } + } + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry)) { + positionAfterProgramHeaderTableEntry0 = positionAfterProgramHeaderTableEntry; + } else { + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "none", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry), + Ctxt, + Input, + positionAfterPPaddr); + positionAfterProgramHeaderTableEntry0 = positionAfterProgramHeaderTableEntry; + } + } + } + } + } + } + if (EverParseIsSuccess(positionAfterProgramHeaderTableEntry0)) { + return positionAfterProgramHeaderTableEntry0; + } + Err("_PROGRAM_HEADER_TABLE_ENTRY", + "none", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableEntry0), + Ctxt, + Input, + positionAfterPType); + return positionAfterProgramHeaderTableEntry0; +} + +static inline uint64_t +ValidateProgramHeaderTableOpt( + uint16_t PhNum, + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLen, + uint64_t StartPosition) +{ + if (PhNum == (uint16_t)(uint8_t)0U) { + /* Validating field Empty */ + uint64_t positionAfterProgramHeaderTableOpt = StartPosition; + if (EverParseIsSuccess(positionAfterProgramHeaderTableOpt)) { + return positionAfterProgramHeaderTableOpt; + } + Err("_PROGRAM_HEADER_TABLE_OPT", + "missing", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableOpt), + Ctxt, + Input, + StartPosition); + return positionAfterProgramHeaderTableOpt; + } + /* Validating field Tbl */ + BOOLEAN + hasEnoughBytes = (uint64_t)((uint32_t)56U * (uint32_t)PhNum) <= (InputLen - StartPosition); + uint64_t positionAfterProgramHeaderTableOpt; + if (!hasEnoughBytes) { + positionAfterProgramHeaderTableOpt = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); + } else { + uint8_t* truncatedInput = Input; + uint64_t truncatedInputLength = StartPosition + (uint64_t)((uint32_t)56U * (uint32_t)PhNum); + uint64_t result = StartPosition; + while (TRUE) { + uint64_t position = *&result; + BOOLEAN ite; + if (!((uint64_t)1U <= (truncatedInputLength - position))) { + ite = TRUE; + } else { + uint64_t positionAfterProgramHeaderTableOpt = ValidateProgramHeaderTableEntry( + ElfFileSize, Ctxt, Err, truncatedInput, truncatedInputLength, position); + uint64_t result1; + if (EverParseIsSuccess(positionAfterProgramHeaderTableOpt)) { + result1 = positionAfterProgramHeaderTableOpt; + } else { + Err("_PROGRAM_HEADER_TABLE_OPT", + ".element", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableOpt), + Ctxt, + truncatedInput, + position); + result1 = positionAfterProgramHeaderTableOpt; + } + result = result1; + ite = EverParseIsError(result1); + } + if (ite) { + break; + } + } + uint64_t res = result; + positionAfterProgramHeaderTableOpt = res; + } + if (EverParseIsSuccess(positionAfterProgramHeaderTableOpt)) { + return positionAfterProgramHeaderTableOpt; + } + Err("_PROGRAM_HEADER_TABLE_OPT", + "missing", + EverParseErrorReasonOfResult(positionAfterProgramHeaderTableOpt), + Ctxt, + Input, + StartPosition); + return positionAfterProgramHeaderTableOpt; +} + +static inline uint64_t +ValidateSectionHeaderTableEntry( + uint16_t ShNum, + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + /* Validating field SH_NAME */ + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - StartPosition); + uint64_t positionAfterSectionHeaderTableEntry; + if (hasBytes0) { + positionAfterSectionHeaderTableEntry = StartPosition + (uint64_t)4U; + } else { + positionAfterSectionHeaderTableEntry = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry)) { + res0 = positionAfterSectionHeaderTableEntry; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_NAME", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry), + Ctxt, + Input, + StartPosition); + res0 = positionAfterSectionHeaderTableEntry; + } + uint64_t positionAfterShName = res0; + if (EverParseIsError(positionAfterShName)) { + return positionAfterShName; + } + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes1 = (uint64_t)4U <= (InputLength - positionAfterShName); + uint64_t positionAfterSectionHeaderTableEntry0; + if (hasBytes1) { + positionAfterSectionHeaderTableEntry0 = positionAfterShName + (uint64_t)4U; + } else { + positionAfterSectionHeaderTableEntry0 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShName); + } + uint64_t positionAfterShType; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry0)) { + positionAfterShType = positionAfterSectionHeaderTableEntry0; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_TYPE", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry0), + Ctxt, + Input, + positionAfterShName); + positionAfterShType = positionAfterSectionHeaderTableEntry0; + } + if (EverParseIsError(positionAfterShType)) { + return positionAfterShType; + } + uint32_t shType = Load32Le(Input + (uint32_t)positionAfterShName); + /* Validating field SH_FLAGS */ + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes2 = (uint64_t)8U <= (InputLength - positionAfterShType); + uint64_t positionAfterSectionHeaderTableEntry1; + if (hasBytes2) { + positionAfterSectionHeaderTableEntry1 = positionAfterShType + (uint64_t)8U; + } else { + positionAfterSectionHeaderTableEntry1 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShType); + } + uint64_t res1; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry1)) { + res1 = positionAfterSectionHeaderTableEntry1; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_FLAGS", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry1), + Ctxt, + Input, + positionAfterShType); + res1 = positionAfterSectionHeaderTableEntry1; + } + uint64_t positionAfterShFlags = res1; + if (EverParseIsError(positionAfterShFlags)) { + return positionAfterShFlags; + } + /* Validating field SH_ADDR */ + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes3 = (uint64_t)8U <= (InputLength - positionAfterShFlags); + uint64_t positionAfterSectionHeaderTableEntry2; + if (hasBytes3) { + positionAfterSectionHeaderTableEntry2 = positionAfterShFlags + (uint64_t)8U; + } else { + positionAfterSectionHeaderTableEntry2 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShFlags); + } + uint64_t res2; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry2)) { + res2 = positionAfterSectionHeaderTableEntry2; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_ADDR", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry2), + Ctxt, + Input, + positionAfterShFlags); + res2 = positionAfterSectionHeaderTableEntry2; + } + uint64_t positionAfterShAddr = res2; + if (EverParseIsError(positionAfterShAddr)) { + return positionAfterShAddr; + } + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes4 = (uint64_t)8U <= (InputLength - positionAfterShAddr); + uint64_t positionAfterSectionHeaderTableEntry3; + if (hasBytes4) { + positionAfterSectionHeaderTableEntry3 = positionAfterShAddr + (uint64_t)8U; + } else { + positionAfterSectionHeaderTableEntry3 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShAddr); + } + uint64_t positionAfterShOffset; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry3)) { + positionAfterShOffset = positionAfterSectionHeaderTableEntry3; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_OFFSET", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry3), + Ctxt, + Input, + positionAfterShAddr); + positionAfterShOffset = positionAfterSectionHeaderTableEntry3; + } + if (EverParseIsError(positionAfterShOffset)) { + return positionAfterShOffset; + } + uint64_t shOffset = Load64Le(Input + (uint32_t)positionAfterShAddr); + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes5 = (uint64_t)8U <= (InputLength - positionAfterShOffset); + uint64_t positionAfternone; + if (hasBytes5) { + positionAfternone = positionAfterShOffset + (uint64_t)8U; + } else { + positionAfternone = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShOffset); + } + uint64_t positionAfterSectionHeaderTableEntry4; + if (EverParseIsError(positionAfternone)) { + positionAfterSectionHeaderTableEntry4 = positionAfternone; + } else { + uint64_t none = Load64Le(Input + (uint32_t)positionAfterShOffset); + BOOLEAN + noneConstraintIsOk = + shType == (uint32_t)ELF____SH_NOBITS || (none <= ElfFileSize && shOffset <= (ElfFileSize - none)); + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterSectionHeaderTableEntry4 = positionAfternone1; + } else { + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - positionAfternone1); + uint64_t positionAfternone2; + if (hasBytes0) { + positionAfternone2 = positionAfternone1 + (uint64_t)4U; + } else { + positionAfternone2 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } + uint64_t positionAfterSectionHeaderTableEntry; + if (EverParseIsError(positionAfternone2)) { + positionAfterSectionHeaderTableEntry = positionAfternone2; + } else { + uint32_t none1 = Load32Le(Input + (uint32_t)positionAfternone1); + BOOLEAN noneConstraintIsOk1 = none1 < (uint32_t)ShNum; + uint64_t positionAfternone3 = EverParseCheckConstraintOk(noneConstraintIsOk1, positionAfternone2); + if (EverParseIsError(positionAfternone3)) { + positionAfterSectionHeaderTableEntry = positionAfternone3; + } else { + /* Validating field SH_INFO */ + /* Checking that we have enough space for a UINT32, i.e., 4 + * bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - positionAfternone3); + uint64_t positionAfterSectionHeaderTableEntry0; + if (hasBytes0) { + positionAfterSectionHeaderTableEntry0 = positionAfternone3 + (uint64_t)4U; + } else { + positionAfterSectionHeaderTableEntry0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone3); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry0)) { + res0 = positionAfterSectionHeaderTableEntry0; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_INFO", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry0), + Ctxt, + Input, + positionAfternone3); + res0 = positionAfterSectionHeaderTableEntry0; + } + uint64_t positionAfterShInfo = res0; + if (EverParseIsError(positionAfterShInfo)) { + positionAfterSectionHeaderTableEntry = positionAfterShInfo; + } else { + /* Validating field SH_ADDRALIGN */ + /* Checking that we have enough space for a UINT64, + * i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterShInfo); + uint64_t positionAfterSectionHeaderTableEntry0; + if (hasBytes0) { + positionAfterSectionHeaderTableEntry0 = positionAfterShInfo + (uint64_t)8U; + } else { + positionAfterSectionHeaderTableEntry0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShInfo); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry0)) { + res0 = positionAfterSectionHeaderTableEntry0; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_ADDRALIGN", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry0), + Ctxt, + Input, + positionAfterShInfo); + res0 = positionAfterSectionHeaderTableEntry0; + } + uint64_t positionAfterShAddralign = res0; + if (EverParseIsError(positionAfterShAddralign)) { + positionAfterSectionHeaderTableEntry = positionAfterShAddralign; + } else { + /* Validating field SH_ENTSIZE */ + /* Checking that we have enough space for a UINT64, + * i.e., 8 bytes */ + BOOLEAN hasBytes = (uint64_t)8U <= (InputLength - positionAfterShAddralign); + uint64_t positionAfterSectionHeaderTableEntry0; + if (hasBytes) { + positionAfterSectionHeaderTableEntry0 = positionAfterShAddralign + (uint64_t)8U; + } else { + positionAfterSectionHeaderTableEntry0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterShAddralign); + } + uint64_t res; + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry0)) { + res = positionAfterSectionHeaderTableEntry0; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "SH_ENTSIZE", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry0), + Ctxt, + Input, + positionAfterShAddralign); + res = positionAfterSectionHeaderTableEntry0; + } + positionAfterSectionHeaderTableEntry = res; + } + } + } + } + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry)) { + positionAfterSectionHeaderTableEntry4 = positionAfterSectionHeaderTableEntry; + } else { + Err("_SECTION_HEADER_TABLE_ENTRY", + "none", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry), + Ctxt, + Input, + positionAfternone1); + positionAfterSectionHeaderTableEntry4 = positionAfterSectionHeaderTableEntry; + } + } + } + if (EverParseIsSuccess(positionAfterSectionHeaderTableEntry4)) { + return positionAfterSectionHeaderTableEntry4; + } + Err("_SECTION_HEADER_TABLE_ENTRY", + "none", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableEntry4), + Ctxt, + Input, + positionAfterShOffset); + return positionAfterSectionHeaderTableEntry4; +} + +static inline uint64_t +ValidateSectionHeaderTable( + uint64_t PhTableEnd, + uint64_t ShOff, + uint16_t ShNum, + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + uint64_t positionAfternone = StartPosition; + uint64_t positionAfterSectionHeaderTable; + if (EverParseIsError(positionAfternone)) { + positionAfterSectionHeaderTable = positionAfternone; + } else { + BOOLEAN + noneConstraintIsOk = PhTableEnd <= ShOff && (ShOff - PhTableEnd) <= (uint64_t)ELF____MAX_UINT32; + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterSectionHeaderTable = positionAfternone1; + } else { + /* Validating field PHTABLE_SHTABLE_GAP */ + BOOLEAN + hasEnoughBytes0 = (uint64_t)(uint32_t)(ShOff - PhTableEnd) <= (InputLength - positionAfternone1); + uint64_t positionAfterSectionHeaderTable0; + if (!hasEnoughBytes0) { + positionAfterSectionHeaderTable0 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } else { + uint8_t* truncatedInput = Input; + uint64_t truncatedInputLength = positionAfternone1 + (uint64_t)(uint32_t)(ShOff - PhTableEnd); + uint64_t result = positionAfternone1; + while (TRUE) { + uint64_t position = *&result; + BOOLEAN ite; + if (!((uint64_t)1U <= (truncatedInputLength - position))) { + ite = TRUE; + } else { + /* Checking that we have enough space for a UINT8, i.e., + * 1 byte */ + BOOLEAN hasBytes = (uint64_t)1U <= (truncatedInputLength - position); + uint64_t positionAfterSectionHeaderTable; + if (hasBytes) { + positionAfterSectionHeaderTable = position + (uint64_t)1U; + } else { + positionAfterSectionHeaderTable = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, position); + } + uint64_t res; + if (EverParseIsSuccess(positionAfterSectionHeaderTable)) { + res = positionAfterSectionHeaderTable; + } else { + Err("_SECTION_HEADER_TABLE", + "PHTABLE_SHTABLE_GAP.element", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable), + Ctxt, + truncatedInput, + position); + res = positionAfterSectionHeaderTable; + } + uint64_t result1 = res; + result = result1; + ite = EverParseIsError(result1); + } + if (ite) { + break; + } + } + uint64_t res = result; + positionAfterSectionHeaderTable0 = res; + } + uint64_t positionAfterPhtableShtableGap; + if (EverParseIsSuccess(positionAfterSectionHeaderTable0)) { + positionAfterPhtableShtableGap = positionAfterSectionHeaderTable0; + } else { + Err("_SECTION_HEADER_TABLE", + "PHTABLE_SHTABLE_GAP", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable0), + Ctxt, + Input, + positionAfternone1); + positionAfterPhtableShtableGap = positionAfterSectionHeaderTable0; + } + if (EverParseIsError(positionAfterPhtableShtableGap)) { + positionAfterSectionHeaderTable = positionAfterPhtableShtableGap; + } else { + /* Validating field SHTABLE */ + BOOLEAN + hasEnoughBytes = + (uint64_t)((uint32_t)64U * (uint32_t)ShNum) <= (InputLength - positionAfterPhtableShtableGap); + uint64_t positionAfterSectionHeaderTable0; + if (!hasEnoughBytes) { + positionAfterSectionHeaderTable0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterPhtableShtableGap); + } else { + uint8_t* truncatedInput = Input; + uint64_t truncatedInputLength = + positionAfterPhtableShtableGap + (uint64_t)((uint32_t)64U * (uint32_t)ShNum); + uint64_t result = positionAfterPhtableShtableGap; + while (TRUE) { + uint64_t position = *&result; + BOOLEAN ite; + if (!((uint64_t)1U <= (truncatedInputLength - position))) { + ite = TRUE; + } else { + uint64_t positionAfterSectionHeaderTable = ValidateSectionHeaderTableEntry( + ShNum, ElfFileSize, Ctxt, Err, truncatedInput, truncatedInputLength, position); + uint64_t result1; + if (EverParseIsSuccess(positionAfterSectionHeaderTable)) { + result1 = positionAfterSectionHeaderTable; + } else { + Err("_SECTION_HEADER_TABLE", + "SHTABLE.element", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable), + Ctxt, + truncatedInput, + position); + result1 = positionAfterSectionHeaderTable; + } + result = result1; + ite = EverParseIsError(result1); + } + if (ite) { + break; + } + } + uint64_t res = result; + positionAfterSectionHeaderTable0 = res; + } + uint64_t positionAfterSHTABLE; + if (EverParseIsSuccess(positionAfterSectionHeaderTable0)) { + positionAfterSHTABLE = positionAfterSectionHeaderTable0; + } else { + Err("_SECTION_HEADER_TABLE", + "SHTABLE", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable0), + Ctxt, + Input, + positionAfterPhtableShtableGap); + positionAfterSHTABLE = positionAfterSectionHeaderTable0; + } + if (EverParseIsError(positionAfterSHTABLE)) { + positionAfterSectionHeaderTable = positionAfterSHTABLE; + } else { + /* ; Check that we have consumed all the bytes in the file; + */ + uint64_t positionAfterSectionHeaderTable0 = positionAfterSHTABLE; + uint64_t positionAfterEndOfFile; + if (EverParseIsSuccess(positionAfterSectionHeaderTable0)) { + positionAfterEndOfFile = positionAfterSectionHeaderTable0; + } else { + Err("_SECTION_HEADER_TABLE", + "EndOfFile.base", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable0), + Ctxt, + Input, + positionAfterSHTABLE); + positionAfterEndOfFile = positionAfterSectionHeaderTable0; + } + uint64_t res; + if (EverParseIsSuccess(positionAfterEndOfFile)) { + uint32_t hd = (uint32_t)positionAfterSHTABLE; + BOOLEAN actionSuccessEndOfFile = (uint64_t)hd == ElfFileSize; + if (!actionSuccessEndOfFile) { + res = EVERPARSE_VALIDATOR_ERROR_ACTION_FAILED; + } else { + res = positionAfterEndOfFile; + } + } else { + res = positionAfterEndOfFile; + } + uint64_t positionAfterSectionHeaderTable1 = res; + if (EverParseIsSuccess(positionAfterSectionHeaderTable1)) { + positionAfterSectionHeaderTable = positionAfterSectionHeaderTable1; + } else { + Err("_SECTION_HEADER_TABLE", + "EndOfFile", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable1), + Ctxt, + Input, + positionAfterSHTABLE); + positionAfterSectionHeaderTable = positionAfterSectionHeaderTable1; + } + } + } + } + } + if (EverParseIsSuccess(positionAfterSectionHeaderTable)) { + return positionAfterSectionHeaderTable; + } + Err("_SECTION_HEADER_TABLE", + "none", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTable), + Ctxt, + Input, + StartPosition); + return positionAfterSectionHeaderTable; +} + +static inline uint64_t +ValidateNoSectionHeaderTable( + uint64_t PhTableEnd, + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + uint64_t positionAfternone = StartPosition; + uint64_t positionAfterNoSectionHeaderTable; + if (EverParseIsError(positionAfternone)) { + positionAfterNoSectionHeaderTable = positionAfternone; + } else { + BOOLEAN + noneConstraintIsOk = PhTableEnd <= ElfFileSize && (ElfFileSize - PhTableEnd) <= (uint64_t)ELF____MAX_UINT32; + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterNoSectionHeaderTable = positionAfternone1; + } else { + /* Validating field Rest */ + BOOLEAN + hasEnoughBytes = (uint64_t)(uint32_t)(ElfFileSize - PhTableEnd) <= (InputLength - positionAfternone1); + uint64_t positionAfterNoSectionHeaderTable0; + if (!hasEnoughBytes) { + positionAfterNoSectionHeaderTable0 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } else { + uint8_t* truncatedInput = Input; + uint64_t truncatedInputLength = positionAfternone1 + (uint64_t)(uint32_t)(ElfFileSize - PhTableEnd); + uint64_t result = positionAfternone1; + while (TRUE) { + uint64_t position = *&result; + BOOLEAN ite; + if (!((uint64_t)1U <= (truncatedInputLength - position))) { + ite = TRUE; + } else { + /* Checking that we have enough space for a UINT8, i.e., + * 1 byte */ + BOOLEAN hasBytes = (uint64_t)1U <= (truncatedInputLength - position); + uint64_t positionAfterNoSectionHeaderTable; + if (hasBytes) { + positionAfterNoSectionHeaderTable = position + (uint64_t)1U; + } else { + positionAfterNoSectionHeaderTable = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, position); + } + uint64_t res; + if (EverParseIsSuccess(positionAfterNoSectionHeaderTable)) { + res = positionAfterNoSectionHeaderTable; + } else { + Err("_NO_SECTION_HEADER_TABLE", + "Rest.element", + EverParseErrorReasonOfResult(positionAfterNoSectionHeaderTable), + Ctxt, + truncatedInput, + position); + res = positionAfterNoSectionHeaderTable; + } + uint64_t result1 = res; + result = result1; + ite = EverParseIsError(result1); + } + if (ite) { + break; + } + } + uint64_t res = result; + positionAfterNoSectionHeaderTable0 = res; + } + if (EverParseIsSuccess(positionAfterNoSectionHeaderTable0)) { + positionAfterNoSectionHeaderTable = positionAfterNoSectionHeaderTable0; + } else { + Err("_NO_SECTION_HEADER_TABLE", + "Rest", + EverParseErrorReasonOfResult(positionAfterNoSectionHeaderTable0), + Ctxt, + Input, + positionAfternone1); + positionAfterNoSectionHeaderTable = positionAfterNoSectionHeaderTable0; + } + } + } + if (EverParseIsSuccess(positionAfterNoSectionHeaderTable)) { + return positionAfterNoSectionHeaderTable; + } + Err("_NO_SECTION_HEADER_TABLE", + "none", + EverParseErrorReasonOfResult(positionAfterNoSectionHeaderTable), + Ctxt, + Input, + StartPosition); + return positionAfterNoSectionHeaderTable; +} + +static inline uint64_t +ValidateSectionHeaderTableOpt( + uint64_t PhTableEnd, + uint64_t ShOff, + uint16_t ShNum, + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLen, + uint64_t StartPosition) +{ + if (ShNum == (uint16_t)(uint8_t)0U) { + /* ; When there is no Section Header table,; the following type ensures + * that there are at least ElfFileSize - PhTableEnd; bytes remaining in + * the file; */ + uint64_t positionAfterSectionHeaderTableOpt = + ValidateNoSectionHeaderTable(PhTableEnd, ElfFileSize, Ctxt, Err, Input, InputLen, StartPosition); + if (EverParseIsSuccess(positionAfterSectionHeaderTableOpt)) { + return positionAfterSectionHeaderTableOpt; + } + Err("_SECTION_HEADER_TABLE_OPT", + "missing", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableOpt), + Ctxt, + Input, + StartPosition); + return positionAfterSectionHeaderTableOpt; + } + /* Validating field Tbl */ + uint64_t positionAfterSectionHeaderTableOpt = + ValidateSectionHeaderTable(PhTableEnd, ShOff, ShNum, ElfFileSize, Ctxt, Err, Input, InputLen, StartPosition); + if (EverParseIsSuccess(positionAfterSectionHeaderTableOpt)) { + return positionAfterSectionHeaderTableOpt; + } + Err("_SECTION_HEADER_TABLE_OPT", + "missing", + EverParseErrorReasonOfResult(positionAfterSectionHeaderTableOpt), + Ctxt, + Input, + StartPosition); + return positionAfterSectionHeaderTableOpt; +} + +uint64_t +ElfValidateElf( + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition) +{ + /* ELF HEADER BEGIN */ + uint64_t positionAfterElf = ValidateEIdent(Ctxt, Err, Input, InputLength, StartPosition); + uint64_t positionAfterIDENT; + if (EverParseIsSuccess(positionAfterElf)) { + positionAfterIDENT = positionAfterElf; + } else { + Err("_ELF", "IDENT", EverParseErrorReasonOfResult(positionAfterElf), Ctxt, Input, StartPosition); + positionAfterIDENT = positionAfterElf; + } + if (EverParseIsError(positionAfterIDENT)) { + return positionAfterIDENT; + } + /* Checking that we have enough space for a UINT16, i.e., 2 bytes */ + BOOLEAN hasBytes0 = (uint64_t)2U <= (InputLength - positionAfterIDENT); + uint64_t positionAfternone; + if (hasBytes0) { + positionAfternone = positionAfterIDENT + (uint64_t)2U; + } else { + positionAfternone = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterIDENT); + } + uint64_t positionAfterElf0; + if (EverParseIsError(positionAfternone)) { + positionAfterElf0 = positionAfternone; + } else { + uint16_t r0 = Load16Le(Input + (uint32_t)positionAfterIDENT); + uint16_t none = (uint16_t)(uint32_t)r0; + BOOLEAN + noneConstraintIsOk = + none != ELF____ET_NONE && (ELF____ET_NONE == none || ELF____ET_REL == none || ELF____ET_EXEC == none || + ELF____ET_DYN == none || ELF____ET_CORE == none); + uint64_t positionAfternone1 = EverParseCheckConstraintOk(noneConstraintIsOk, positionAfternone); + if (EverParseIsError(positionAfternone1)) { + positionAfterElf0 = positionAfternone1; + } else { + /* ; We can restrict the values of E_MACHINE by making its type an + * enum, for example; The elf man page lists some possible values, + * but that list does not seem to be exhaustive; */ + /* Checking that we have enough space for a UINT16, i.e., 2 bytes */ + BOOLEAN hasBytes0 = (uint64_t)2U <= (InputLength - positionAfternone1); + uint64_t positionAfterElf; + if (hasBytes0) { + positionAfterElf = positionAfternone1 + (uint64_t)2U; + } else { + positionAfterElf = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone1); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterElf)) { + res0 = positionAfterElf; + } else { + Err("_ELF", + "E_MACHINE", + EverParseErrorReasonOfResult(positionAfterElf), + Ctxt, + Input, + positionAfternone1); + res0 = positionAfterElf; + } + uint64_t positionAfterEMachine = res0; + if (EverParseIsError(positionAfterEMachine)) { + positionAfterElf0 = positionAfterEMachine; + } else { + /* Checking that we have enough space for a UINT32, i.e., 4 + * bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - positionAfterEMachine); + uint64_t positionAfternone2; + if (hasBytes0) { + positionAfternone2 = positionAfterEMachine + (uint64_t)4U; + } else { + positionAfternone2 = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterEMachine); + } + uint64_t positionAfterElf; + if (EverParseIsError(positionAfternone2)) { + positionAfterElf = positionAfternone2; + } else { + uint32_t none1 = Load32Le(Input + (uint32_t)positionAfterEMachine); + BOOLEAN noneConstraintIsOk1 = none1 == (uint32_t)(uint8_t)1U; + uint64_t positionAfternone3 = EverParseCheckConstraintOk(noneConstraintIsOk1, positionAfternone2); + if (EverParseIsError(positionAfternone3)) { + positionAfterElf = positionAfternone3; + } else { + /* Validating field E_ENTRY */ + /* Checking that we have enough space for a UINT64, + * i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfternone3); + uint64_t positionAfterElf0; + if (hasBytes0) { + positionAfterElf0 = positionAfternone3 + (uint64_t)8U; + } else { + positionAfterElf0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone3); + } + uint64_t res0; + if (EverParseIsSuccess(positionAfterElf0)) { + res0 = positionAfterElf0; + } else { + Err("_ELF", + "E_ENTRY", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfternone3); + res0 = positionAfterElf0; + } + uint64_t positionAfterEEntry = res0; + if (EverParseIsError(positionAfterEEntry)) { + positionAfterElf = positionAfterEEntry; + } else { + /* Checking that we have enough space for a UINT64, + * i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterEEntry); + uint64_t positionAfterElf0; + if (hasBytes0) { + positionAfterElf0 = positionAfterEEntry + (uint64_t)8U; + } else { + positionAfterElf0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterEEntry); + } + uint64_t positionAfterEPhoff; + if (EverParseIsSuccess(positionAfterElf0)) { + positionAfterEPhoff = positionAfterElf0; + } else { + Err("_ELF", + "E_PHOFF", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfterEEntry); + positionAfterEPhoff = positionAfterElf0; + } + if (EverParseIsError(positionAfterEPhoff)) { + positionAfterElf = positionAfterEPhoff; + } else { + uint64_t ePhoff = Load64Le(Input + (uint32_t)positionAfterEEntry); + /* Checking that we have enough space for a + * UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes0 = (uint64_t)8U <= (InputLength - positionAfterEPhoff); + uint64_t positionAfterElf0; + if (hasBytes0) { + positionAfterElf0 = positionAfterEPhoff + (uint64_t)8U; + } else { + positionAfterElf0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterEPhoff); + } + uint64_t positionAfterEShoff; + if (EverParseIsSuccess(positionAfterElf0)) { + positionAfterEShoff = positionAfterElf0; + } else { + Err("_ELF", + "E_SHOFF", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfterEPhoff); + positionAfterEShoff = positionAfterElf0; + } + if (EverParseIsError(positionAfterEShoff)) { + positionAfterElf = positionAfterEShoff; + } else { + uint64_t eShoff = Load64Le(Input + (uint32_t)positionAfterEPhoff); + /* Validating field E_FLAGS */ + /* Checking that we have enough space for a + * UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes0 = (uint64_t)4U <= (InputLength - positionAfterEShoff); + uint64_t positionAfterElf0; + if (hasBytes0) { + positionAfterElf0 = positionAfterEShoff + (uint64_t)4U; + } else { + positionAfterElf0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterEShoff); + } + uint64_t res; + if (EverParseIsSuccess(positionAfterElf0)) { + res = positionAfterElf0; + } else { + Err("_ELF", + "E_FLAGS", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfterEShoff); + res = positionAfterElf0; + } + uint64_t positionAfterEFlags = res; + if (EverParseIsError(positionAfterEFlags)) { + positionAfterElf = positionAfterEFlags; + } else { + /* Checking that we have enough space + * for a UINT16, i.e., 2 bytes */ + BOOLEAN hasBytes0 = (uint64_t)2U <= (InputLength - positionAfterEFlags); + uint64_t positionAfternone4; + if (hasBytes0) { + positionAfternone4 = positionAfterEFlags + (uint64_t)2U; + } else { + positionAfternone4 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterEFlags); + } + uint64_t positionAfterElf0; + if (EverParseIsError(positionAfternone4)) { + positionAfterElf0 = positionAfternone4; + } else { + uint16_t r0 = Load16Le(Input + (uint32_t)positionAfterEFlags); + uint16_t none2 = (uint16_t)(uint32_t)r0; + BOOLEAN noneConstraintIsOk2 = (uint32_t)none2 == (uint32_t)64U; + uint64_t positionAfternone5 = + EverParseCheckConstraintOk(noneConstraintIsOk2, positionAfternone4); + if (EverParseIsError(positionAfternone5)) { + positionAfterElf0 = positionAfternone5; + } else { + /* Checking that we have enough + * space for a UINT16, i.e., 2 + * bytes */ + BOOLEAN hasBytes0 = (uint64_t)2U <= (InputLength - positionAfternone5); + uint64_t positionAfterElf; + if (hasBytes0) { + positionAfterElf = positionAfternone5 + (uint64_t)2U; + } else { + positionAfterElf = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfternone5); + } + uint64_t positionAfterEPhentsize; + if (EverParseIsSuccess(positionAfterElf)) { + positionAfterEPhentsize = positionAfterElf; + } else { + Err("_ELF", + "E_PHENTSIZE", + EverParseErrorReasonOfResult(positionAfterElf), + Ctxt, + Input, + positionAfternone5); + positionAfterEPhentsize = positionAfterElf; + } + if (EverParseIsError(positionAfterEPhentsize)) { + positionAfterElf0 = positionAfterEPhentsize; + } else { + uint16_t r0 = Load16Le(Input + (uint32_t)positionAfternone5); + uint16_t ePhentsize = (uint16_t)(uint32_t)r0; + /* Checking that we have + * enough space for a + * UINT16, i.e., 2 bytes */ + BOOLEAN + hasBytes0 = (uint64_t)2U <= (InputLength - positionAfterEPhentsize); + uint64_t positionAfternone6; + if (hasBytes0) { + positionAfternone6 = positionAfterEPhentsize + (uint64_t)2U; + } else { + positionAfternone6 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfterEPhentsize); + } + uint64_t positionAfterElf; + if (EverParseIsError(positionAfternone6)) { + positionAfterElf = positionAfternone6; + } else { + uint16_t r0 = + Load16Le(Input + (uint32_t)positionAfterEPhentsize); + uint16_t none3 = (uint16_t)(uint32_t)r0; + BOOLEAN + noneConstraintIsOk3 = + (none3 == (uint16_t)(uint8_t)0U && + ePhoff == (uint64_t)(uint8_t)0U) || + ((uint16_t)(uint8_t)0U < none3 && none3 < ELF____PN_XNUM && + (uint64_t)(uint32_t)64U == ePhoff && + (uint32_t)ePhentsize == (uint32_t)56U); + uint64_t positionAfternone7 = EverParseCheckConstraintOk( + noneConstraintIsOk3, positionAfternone6); + if (EverParseIsError(positionAfternone7)) { + positionAfterElf = positionAfternone7; + } else { + /* Checking that we + * have enough space + * for a UINT16, + * i.e., 2 bytes */ + BOOLEAN + hasBytes0 = + (uint64_t)2U <= (InputLength - positionAfternone7); + uint64_t positionAfterElf0; + if (hasBytes0) { + positionAfterElf0 = positionAfternone7 + (uint64_t)2U; + } else { + positionAfterElf0 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfternone7); + } + uint64_t positionAfterEShentsize; + if (EverParseIsSuccess(positionAfterElf0)) { + positionAfterEShentsize = positionAfterElf0; + } else { + Err("_ELF", + "E_" + "SHENTSIZE", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfternone7); + positionAfterEShentsize = positionAfterElf0; + } + if (EverParseIsError(positionAfterEShentsize)) { + positionAfterElf = positionAfterEShentsize; + } else { + uint16_t r0 = + Load16Le(Input + (uint32_t)positionAfternone7); + uint16_t eShentsize = (uint16_t)(uint32_t)r0; + /* Checking that + * we have + * enough space + * for a UINT16, + * i.e., 2 bytes + */ + BOOLEAN + hasBytes0 = (uint64_t)2U <= + (InputLength - positionAfterEShentsize); + uint64_t positionAfternone8; + if (hasBytes0) { + positionAfternone8 = + positionAfterEShentsize + (uint64_t)2U; + } else { + positionAfternone8 = EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfterEShentsize); + } + uint64_t positionAfterElf0; + if (EverParseIsError(positionAfternone8)) { + positionAfterElf0 = positionAfternone8; + } else { + uint16_t r0 = Load16Le( + Input + (uint32_t)positionAfterEShentsize); + uint16_t none4 = (uint16_t)(uint32_t)r0; + BOOLEAN + noneConstraintIsOk4 = + (none4 == (uint16_t)(uint8_t)0U && + eShoff == (uint64_t)(uint8_t)0U) || + ((uint16_t)(uint8_t)0U < none4 && + none4 < ELF____SHN_LORESERVE && + (uint32_t)eShentsize == (uint32_t)64U); + uint64_t positionAfternone9 = + EverParseCheckConstraintOk( + noneConstraintIsOk4, positionAfternone8); + if (EverParseIsError(positionAfternone9)) { + positionAfterElf0 = positionAfternone9; + } else { + /* Checking + * that + * we + * have + * enough + * space + * for a + * UINT16, + * i.e., + * 2 + * bytes + */ + BOOLEAN + hasBytes = (uint64_t)2U <= + (InputLength - positionAfternone9); + uint64_t positionAfternone10; + if (hasBytes) { + positionAfternone10 = + positionAfternone9 + (uint64_t)2U; + } else { + positionAfternone10 = + EverParseSetValidatorErrorPos( + EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + positionAfternone9); + } + uint64_t positionAfterElf; + if (EverParseIsError(positionAfternone10)) { + positionAfterElf = positionAfternone10; + } else { + uint16_t r = Load16Le( + Input + (uint32_t)positionAfternone9); + uint16_t none5 = (uint16_t)(uint32_t)r; + BOOLEAN + noneConstraintIsOk5 = + (none4 == (uint16_t)(uint8_t)0U && + none5 == (uint16_t)ELF____SHN_UNDEF) || + ((uint16_t)(uint8_t)0U < none4 && + none5 < none4); + uint64_t positionAfternone11 = + EverParseCheckConstraintOk( + noneConstraintIsOk5, + positionAfternone10); + if (EverParseIsError(positionAfternone11)) { + positionAfterElf = positionAfternone11; + } else { + /* ELF HEADER END; (Optional) Program + * Header table */ + uint64_t positionAfterElf0 = + ValidateProgramHeaderTableOpt( + none3, + ElfFileSize, + Ctxt, + Err, + Input, + InputLength, + positionAfternone11); + uint64_t positionAfterPhTable; + if (EverParseIsSuccess( + positionAfterElf0)) { + positionAfterPhTable = + positionAfterElf0; + } else { + Err("_ELF", + "PH_TABLE", + EverParseErrorReasonOfResult( + positionAfterElf0), + Ctxt, + Input, + positionAfternone11); + positionAfterPhTable = + positionAfterElf0; + } + if (EverParseIsError( + positionAfterPhTable)) { + positionAfterElf = + positionAfterPhTable; + } else { + /* (Optional) Section Header Table + */ + uint64_t ite; + if (none3 == + (uint16_t)(uint8_t)0U) { + ite = (uint64_t)none2; + } else { + ite = ePhoff; + } + uint64_t positionAfterElf0 = + ValidateSectionHeaderTableOpt( + ite + + (uint64_t)((uint32_t)56U * (uint32_t)none3), + eShoff, + none4, + ElfFileSize, + Ctxt, + Err, + Input, + InputLength, + positionAfterPhTable); + if (EverParseIsSuccess( + positionAfterElf0)) { + positionAfterElf = + positionAfterElf0; + } else { + Err("_ELF", + "SH_TABLE", + EverParseErrorReasonOfResult( + positionAfterElf0), + Ctxt, + Input, + positionAfterPhTable); + positionAfterElf = + positionAfterElf0; + } + } + } + } + if (EverParseIsSuccess(positionAfterElf)) { + positionAfterElf0 = positionAfterElf; + } else { + Err("_ELF", + "none", + EverParseErrorReasonOfResult( + positionAfterElf), + Ctxt, + Input, + positionAfternone9); + positionAfterElf0 = positionAfterElf; + } + } + } + if (EverParseIsSuccess(positionAfterElf0)) { + positionAfterElf = positionAfterElf0; + } else { + Err("_ELF", + "none", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfterEShentsize); + positionAfterElf = positionAfterElf0; + } + } + } + } + if (EverParseIsSuccess(positionAfterElf)) { + positionAfterElf0 = positionAfterElf; + } else { + Err("_ELF", + "none", + EverParseErrorReasonOfResult(positionAfterElf), + Ctxt, + Input, + positionAfterEPhentsize); + positionAfterElf0 = positionAfterElf; + } + } + } + } + if (EverParseIsSuccess(positionAfterElf0)) { + positionAfterElf = positionAfterElf0; + } else { + Err("_ELF", + "none", + EverParseErrorReasonOfResult(positionAfterElf0), + Ctxt, + Input, + positionAfterEFlags); + positionAfterElf = positionAfterElf0; + } + } + } + } + } + } + } + if (EverParseIsSuccess(positionAfterElf)) { + positionAfterElf0 = positionAfterElf; + } else { + Err("_ELF", + "none", + EverParseErrorReasonOfResult(positionAfterElf), + Ctxt, + Input, + positionAfterEMachine); + positionAfterElf0 = positionAfterElf; + } + } + } + } + if (EverParseIsSuccess(positionAfterElf0)) { + return positionAfterElf0; + } + Err("_ELF", "none", EverParseErrorReasonOfResult(positionAfterElf0), Ctxt, Input, positionAfterIDENT); + return positionAfterElf0; +} diff --git a/spec/elf/Elf.h b/spec/elf/Elf.h new file mode 100644 index 0000000000..41ff409f94 --- /dev/null +++ b/spec/elf/Elf.h @@ -0,0 +1,157 @@ + + +#ifndef __Elf_H +#define __Elf_H + +#if defined(__cplusplus) +extern "C" +{ +#endif + +#include "EverParse.h" + +#define ELF____MAX_UINT32 ((uint32_t)0xffffffffU) + +#define ELF____ELFMAG0 ((uint8_t)0x7fU) + +#define ELF____ELFMAG1 ((uint8_t)0x45U) + +#define ELF____ELFMAG2 ((uint8_t)0x4cU) + +#define ELF____ELFMAG3 ((uint8_t)0x46U) + +#define ELF____PN_XNUM ((uint16_t)0xffffU) + +#define ELF____SHN_LORESERVE ((uint16_t)0xff00U) + +#define ELF____SHN_UNDEF ((uint8_t)0U) + +/* +Enum constant +*/ +#define ELF____ELFCLASSNONE ((uint8_t)0U) + +/* +Enum constant +*/ +#define ELF____ELFCLASS32 ((uint8_t)1U) + +/* +Enum constant +*/ +#define ELF____ELFCLASS64 ((uint8_t)2U) + +/* +Enum constant +*/ +#define ELF____ELFDATANONE ((uint8_t)0U) + +/* +Enum constant +*/ +#define ELF____ELFDATA2LSB ((uint8_t)1U) + +/* +Enum constant +*/ +#define ELF____ELFDATA2MSB ((uint8_t)2U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_NONE ((uint8_t)0U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_SYSV ((uint8_t)1U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_HPUX ((uint8_t)2U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_NETBSD ((uint8_t)3U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_LINUX ((uint8_t)4U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_SOLARIS ((uint8_t)5U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_IRIX ((uint8_t)6U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_FREEBSD ((uint8_t)7U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_TRU64 ((uint8_t)8U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_ARM ((uint8_t)9U) + +/* +Enum constant +*/ +#define ELF____ELFOSABI_STANDALONE ((uint8_t)10U) + +#define ELF____E_IDENT_PADDING_SIZE ((uint8_t)7U) + +/* +Enum constant +*/ +#define ELF____ET_NONE ((uint16_t)0U) + +/* +Enum constant +*/ +#define ELF____ET_REL ((uint16_t)1U) + +/* +Enum constant +*/ +#define ELF____ET_EXEC ((uint16_t)2U) + +/* +Enum constant +*/ +#define ELF____ET_DYN ((uint16_t)3U) + +/* +Enum constant +*/ +#define ELF____ET_CORE ((uint16_t)4U) + +#define ELF____SH_NOBITS ((uint8_t)8U) + + uint64_t + ElfValidateElf( + uint64_t ElfFileSize, + uint8_t* Ctxt, + void (*Err)(EverParseString x0, EverParseString x1, EverParseString x2, uint8_t* x3, uint8_t* x4, uint64_t x5), + uint8_t* Input, + uint64_t InputLength, + uint64_t StartPosition); + +#if defined(__cplusplus) +} +#endif + +#define __Elf_H_DEFINED +#endif diff --git a/spec/elf/ElfWrapper.c b/spec/elf/ElfWrapper.c new file mode 100644 index 0000000000..0e0fc49bfb --- /dev/null +++ b/spec/elf/ElfWrapper.c @@ -0,0 +1,33 @@ +#include "ElfWrapper.h" +#include "EverParse.h" +#include "Elf.h" +void +ElfEverParseError(const char* StructName, const char* FieldName, const char* Reason); + +static void +DefaultErrorHandler( + const char* typename_s, + const char* fieldname, + const char* reason, + uint8_t* context, + EverParseInputBuffer input, + uint64_t start_pos) +{ + EverParseErrorFrame* frame = (EverParseErrorFrame*)context; + EverParseDefaultErrorHandler(typename_s, fieldname, reason, frame, input, start_pos); +} + +BOOLEAN +ElfCheckElf(uint64_t ___ElfFileSize, uint8_t* base, uint32_t len) +{ + EverParseErrorFrame frame; + frame.filled = FALSE; + uint64_t result = ElfValidateElf(___ElfFileSize, (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0); + if (EverParseIsError(result)) { + if (frame.filled) { + ElfEverParseError(frame.typename_s, frame.fieldname, frame.reason); + } + return FALSE; + } + return TRUE; +} diff --git a/spec/elf/ElfWrapper.h b/spec/elf/ElfWrapper.h new file mode 100644 index 0000000000..76e5583dcf --- /dev/null +++ b/spec/elf/ElfWrapper.h @@ -0,0 +1,10 @@ +#include "EverParseEndianness.h" +#ifdef __cplusplus +extern "C" +{ +#endif + BOOLEAN + ElfCheckElf(uint64_t ___ElfFileSize, uint8_t* base, uint32_t len); +#ifdef __cplusplus +} +#endif diff --git a/spec/elf/EverParse.h b/spec/elf/EverParse.h new file mode 100644 index 0000000000..6dd6367b76 --- /dev/null +++ b/spec/elf/EverParse.h @@ -0,0 +1,192 @@ +/*++ + +Copyright (c) Microsoft Corporation + +Module Name: + +EverParse.h + +Abstract: + +This is an EverParse-generated file that contains common auxiliary +functions for EverParse-generated verified data validators. + +This file was generated by EverParse v2022.02.02 + +Authors: + +nswamy, protz, taramana 5-Feb-2020 + +--*/ + +#ifndef __EverParse_H +#define __EverParse_H + +#if defined(__cplusplus) +extern "C" +{ +#endif + +#include "EverParseEndianness.h" + + static inline uint8_t + EverParseGetBitfield8(uint8_t Value, uint32_t BitsFrom, uint32_t BitsTo) + { + uint8_t op1 = Value << ((uint32_t)8U - BitsTo); + return op1 >> ((uint32_t)8U - BitsTo + BitsFrom); + } + + static inline uint16_t + EverParseGetBitfield16(uint16_t Value, uint32_t BitsFrom, uint32_t BitsTo) + { + uint16_t bf = Value << ((uint32_t)16U - BitsTo); + return bf >> ((uint32_t)16U - BitsTo + BitsFrom); + } + + static inline uint32_t + EverParseGetBitfield32(uint32_t Value, uint32_t BitsFrom, uint32_t BitsTo) + { + return Value << ((uint32_t)32U - BitsTo) >> ((uint32_t)32U - BitsTo + BitsFrom); + } + + static inline uint64_t + EverParseGetBitfield64(uint64_t Value, uint32_t BitsFrom, uint32_t BitsTo) + { + return Value << ((uint32_t)64U - BitsTo) >> ((uint32_t)64U - BitsTo + BitsFrom); + } + +#define EVERPARSE_VALIDATOR_MAX_LENGTH ((uint64_t)1152921504606846975U) + + static inline BOOLEAN + EverParseIsError(uint64_t PositionOrError) + { + return PositionOrError > EVERPARSE_VALIDATOR_MAX_LENGTH; + } + + static inline BOOLEAN + EverParseIsSuccess(uint64_t PositionOrError) + { + return PositionOrError <= EVERPARSE_VALIDATOR_MAX_LENGTH; + } + + static inline uint64_t + EverParseSetValidatorErrorPos(uint64_t Error, uint64_t Position) + { + return (Error & (uint64_t)17293822569102704640U) | Position << (uint32_t)0U; + } + + static inline uint64_t + EverParseGetValidatorErrorPos(uint64_t X) + { + return (X & (uint64_t)1152921504606846975U) >> (uint32_t)0U; + } + + static inline uint64_t + EverParseSetValidatorErrorKind(uint64_t Error, uint64_t Code) + { + return (Error & (uint64_t)1152921504606846975U) | Code << (uint32_t)60U; + } + + static inline uint64_t + EverParseGetValidatorErrorKind(uint64_t Error) + { + return (Error & (uint64_t)17293822569102704640U) >> (uint32_t)60U; + } + +#define EVERPARSE_VALIDATOR_ERROR_GENERIC ((uint64_t)1152921504606846976U) + +#define EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA ((uint64_t)2305843009213693952U) + +#define EVERPARSE_VALIDATOR_ERROR_IMPOSSIBLE ((uint64_t)3458764513820540928U) + +#define EVERPARSE_VALIDATOR_ERROR_LIST_SIZE_NOT_MULTIPLE ((uint64_t)4611686018427387904U) + +#define EVERPARSE_VALIDATOR_ERROR_ACTION_FAILED ((uint64_t)5764607523034234880U) + +#define EVERPARSE_VALIDATOR_ERROR_CONSTRAINT_FAILED ((uint64_t)6917529027641081856U) + +#define EVERPARSE_VALIDATOR_ERROR_UNEXPECTED_PADDING ((uint64_t)8070450532247928832U) + + static inline PrimsString + EverParseErrorReasonOfResult(uint64_t Code) + { + switch (EverParseGetValidatorErrorKind(Code)) { + case 1U: { + return "generic error"; + } + case 2U: { + return "not enough data"; + } + case 3U: { + return "impossible"; + } + case 4U: { + return "list size not multiple of element size"; + } + case 5U: { + return "action failed"; + } + case 6U: { + return "constraint failed"; + } + case 7U: { + return "unexpected padding"; + } + default: { + return "unspecified"; + } + } + } + + static inline uint64_t + EverParseCheckConstraintOk(BOOLEAN Ok, uint64_t Position) + { + if (Ok) { + return Position; + } + return EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_CONSTRAINT_FAILED, Position); + } + + static inline BOOLEAN + EverParseIsRangeOkay(uint32_t Size, uint32_t Offset, uint32_t AccessSize) + { + return Size >= AccessSize && (Size - AccessSize) >= Offset; + } + + typedef struct EverParseErrorFrame_s + { + BOOLEAN filled; + uint64_t start_pos; + PrimsString typename_s; + PrimsString fieldname; + PrimsString reason; + } EverParseErrorFrame; + + typedef uint8_t* EverParseInputBuffer; + + static inline void + EverParseDefaultErrorHandler( + PrimsString TypenameS, + PrimsString Fieldname, + PrimsString Reason, + EverParseErrorFrame* Context, + uint8_t* Input, + uint64_t StartPos) + { + if (!(*Context).filled) { + *Context = ((EverParseErrorFrame){ + .filled = TRUE, + .start_pos = StartPos, + .typename_s = TypenameS, + .fieldname = Fieldname, + .reason = Reason}); + return; + } + } + +#if defined(__cplusplus) +} +#endif + +#define __EverParse_H_DEFINED +#endif diff --git a/spec/elf/EverParseEndianness.h b/spec/elf/EverParseEndianness.h new file mode 100644 index 0000000000..9cad984fa0 --- /dev/null +++ b/spec/elf/EverParseEndianness.h @@ -0,0 +1,110 @@ +/*++ + +Copyright (c) Microsoft Corporation + +Module Name: + +EverParseEndianness.h + +Abstract: + +This is an EverParse-related file to read integer values from raw +bytes. + +Authors: + +nswamy, protz, taramana 5-Feb-2020 + +--*/ +/* This is a hand-written header that selectively includes relevant bits from + * kremlib.h -- it has to be updated manually to track upstream changes. */ + +#pragma once + +/***************************************************************************** + ********* Implementation of LowStar.Endianness (selected bits) ************** + *****************************************************************************/ + +#include + +/* ... for Windows (MSVC)... not targeting XBOX 360! */ + +#include +#include + +#include + +typedef const char* EverParseString; +typedef EverParseString PrimsString; + +#define htobe16(x) _byteswap_ushort(x) +#define htole16(x) (x) +#define be16toh(x) _byteswap_ushort(x) +#define le16toh(x) (x) + +#define htobe32(x) _byteswap_ulong(x) +#define htole32(x) (x) +#define be32toh(x) _byteswap_ulong(x) +#define le32toh(x) (x) + +#define htobe64(x) _byteswap_uint64(x) +#define htole64(x) (x) +#define be64toh(x) _byteswap_uint64(x) +#define le64toh(x) (x) + +inline static uint16_t +Load16(uint8_t* b) +{ + uint16_t x; + memcpy(&x, b, 2); + return x; +} + +inline static uint32_t +Load32(uint8_t* b) +{ + uint32_t x; + memcpy(&x, b, 4); + return x; +} + +inline static uint64_t +Load64(uint8_t* b) +{ + uint64_t x; + memcpy(&x, b, 8); + return x; +} + +inline static void +Store16(uint8_t* b, uint16_t i) +{ + memcpy(b, &i, 2); +} + +inline static void +Store32(uint8_t* b, uint32_t i) +{ + memcpy(b, &i, 4); +} + +inline static void +Store64(uint8_t* b, uint64_t i) +{ + memcpy(b, &i, 8); +} + +#define Load16Le(b) (le16toh(Load16(b))) +#define Store16Le(b, i) (Store16(b, htole16(i))) +#define Load16Be(b) (be16toh(Load16(b))) +#define Store16Be(b, i) (Store16(b, htobe16(i))) + +#define Load32Le(b) (le32toh(Load32(b))) +#define Store32Le(b, i) (Store32(b, htole32(i))) +#define Load32Be(b) (be32toh(Load32(b))) +#define Store32Be(b, i) (Store32(b, htobe32(i))) + +#define Load64Le(b) (le64toh(Load64(b))) +#define Store64Le(b, i) (Store64(b, htole64(i))) +#define Load64Be(b) (be64toh(Load64(b))) +#define Store64Be(b, i) (Store64(b, htobe64(i))) diff --git a/spec/elf/elf.vcxproj b/spec/elf/elf.vcxproj new file mode 100644 index 0000000000..637b5fd539 --- /dev/null +++ b/spec/elf/elf.vcxproj @@ -0,0 +1,158 @@ + + + + + Debug + Win32 + + + Release + Win32 + + + Debug + x64 + + + Release + x64 + + + + + + + + + + + + + + 16.0 + Win32Proj + {e2b1c5ce-99d2-4732-acfb-0133f31a450f} + elf + 10.0 + spec_elf + + + + StaticLibrary + true + v142 + Unicode + + + StaticLibrary + false + v142 + true + Unicode + + + StaticLibrary + true + v142 + Unicode + + + StaticLibrary + false + v142 + true + Unicode + + + + + + + + + + + + + + + + + + + + + true + + + false + + + true + + + false + + + + WIN32;_DEBUG;_LIB;%(PreprocessorDefinitions) + true + NotUsing + pch.h + + + + + true + + + + + true + WIN32;NDEBUG;_LIB;%(PreprocessorDefinitions) + true + NotUsing + pch.h + + + + + true + true + true + + + + + true + _AMD64_;_DEBUG;_LIB;%(PreprocessorDefinitions) + true + NotUsing + pch.h + + + + + true + + + + + true + _AMD64_;NDEBUG;_LIB;%(PreprocessorDefinitions) + true + NotUsing + pch.h + + + + + true + true + true + + + + + + \ No newline at end of file diff --git a/spec/elf/elf.vcxproj.filters b/spec/elf/elf.vcxproj.filters new file mode 100644 index 0000000000..6b8461a1e2 --- /dev/null +++ b/spec/elf/elf.vcxproj.filters @@ -0,0 +1,39 @@ + + + + + {4FC737F1-C7A5-4376-A066-2A32D752A2FF} + cpp;c;cc;cxx;c++;cppm;ixx;def;odl;idl;hpj;bat;asm;asmx + + + {93995380-89BD-4b04-88EB-625FBE52EBFB} + h;hh;hpp;hxx;h++;hm;inl;inc;ipp;xsd + + + {67DA6AB6-F800-4c08-8B7A-83BB121AAD01} + rc;ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe;resx;tiff;tif;png;wav;mfcribbon-ms + + + + + Source Files + + + Source Files + + + + + Header Files + + + Header Files + + + Header Files + + + Header Files + + + \ No newline at end of file diff --git a/spec/spec.md b/spec/spec.md new file mode 100644 index 0000000000..873f697c3c --- /dev/null +++ b/spec/spec.md @@ -0,0 +1,8 @@ +ELF file validator +================= + +All .h and .c files in this folder are generated from the .3d files. To regenerate them: +1) Download the latest drop of EverParse from https://github.com/project-everest/everparse/tags +2) Run ```everparse.cmd external\everparse\src\3d\tests\ELF.3d``` +3) Copy the resulting files into a subdirectory named after the .3d file. +4) Run the code formatting tool over the generated files. diff --git a/tests/bpf2c_tests/bpf2c_tests.vcxproj b/tests/bpf2c_tests/bpf2c_tests.vcxproj index 22f945b576..8e7c7decf5 100644 --- a/tests/bpf2c_tests/bpf2c_tests.vcxproj +++ b/tests/bpf2c_tests/bpf2c_tests.vcxproj @@ -113,7 +113,7 @@ _DEBUG;_CONSOLE;%(PreprocessorDefinitions) true - $(SolutionDir)include;$(SolutionDir)tests\libs\util;$(SolutionDir)tests\libs\common;$(OutDir);$(SolutionDir)tools\bpf2c;$(SolutionDir)external\ubpf\vm;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\catch2\src;$(SolutionDir)external\catch2\build\generated-includes;%(AdditionalIncludeDirectories) + $(SolutionDir)include;$(SolutionDir)tests\libs\util;$(SolutionDir)tests\libs\common;$(OutDir);$(SolutionDir)tools\bpf2c;$(SolutionDir)external\ubpf\vm;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\catch2\src;$(SolutionDir)external\catch2\build\generated-includes;$(SolutionDir)spec\elf;%(AdditionalIncludeDirectories) Console @@ -124,7 +124,7 @@ NDEBUG;_CONSOLE;%(PreprocessorDefinitions) true - $(SolutionDir)include;$(SolutionDir)tests\libs\util;$(SolutionDir)tests\libs\common;$(OutDir);$(SolutionDir)tools\bpf2c;$(SolutionDir)external\ubpf\vm;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\catch2\src;$(SolutionDir)external\catch2\build\generated-includes;%(AdditionalIncludeDirectories) + $(SolutionDir)include;$(SolutionDir)tests\libs\util;$(SolutionDir)tests\libs\common;$(OutDir);$(SolutionDir)tools\bpf2c;$(SolutionDir)external\ubpf\vm;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\catch2\src;$(SolutionDir)external\catch2\build\generated-includes;$(SolutionDir)spec\elf;%(AdditionalIncludeDirectories) Console diff --git a/tools/bpf2c/bpf2c.cpp b/tools/bpf2c/bpf2c.cpp index 800a33f021..0f1807c736 100644 --- a/tools/bpf2c/bpf2c.cpp +++ b/tools/bpf2c/bpf2c.cpp @@ -1,8 +1,8 @@ // Copyright (c) Microsoft Corporation // SPDX-License-Identifier: MIT +#include #include -#include #include #include #include @@ -11,6 +11,7 @@ #include #include "bpf_code_generator.h" #include "ebpf_api.h" +#include "elfwrapper.h" const char bpf2c_driver[] = #include "bpf2c_driver.template" @@ -20,12 +21,34 @@ const char bpf2c_dll[] = #include "bpf2c_dll.template" ; +#define elf_ever_parse_error ElfEverParseError + void emit_skeleton(const std::string& c_name, const std::string& code) { std::cout << std::regex_replace(code, std::regex(std::string("___METADATA_TABLE___")), c_name) << std::endl; } +extern "C" void +elf_ever_parse_error(const char* struct_name, const char* field_name, const char* reason) +{ + std::cerr << "Validation failure: struct_name=" << struct_name << " field_name=" << field_name + << " reason=" << reason << std::endl; +} + +std::unique_ptr +load_and_validate_elf(const std::filesystem::path& path) +{ + std::ifstream input(path, std::ios::binary); + std::vector data(std::filesystem::file_size(path)); + input.read(data.data(), data.size()); + if (!ElfCheckElf(data.size(), reinterpret_cast(data.data()), static_cast(data.size()))) { + throw std::runtime_error(std::string("ELF file ") + path.string() + " is malformed"); + } + std::string str(data.data(), data.size()); + return std::make_unique(str); +} + int main(int argc, char** argv) { @@ -86,7 +109,8 @@ main(int argc, char** argv) std::string c_name = file.substr(file.find_last_of("\\") + 1); c_name = c_name.substr(0, c_name.find(".")); - bpf_code_generator generator(file, c_name); + auto input_stream = load_and_validate_elf(file); + bpf_code_generator generator(*input_stream, c_name); // Special case of no section name. if (sections.size() == 0) { diff --git a/tools/bpf2c/bpf2c.vcxproj b/tools/bpf2c/bpf2c.vcxproj index e97e276b8e..b0d11b1c2c 100644 --- a/tools/bpf2c/bpf2c.vcxproj +++ b/tools/bpf2c/bpf2c.vcxproj @@ -113,9 +113,9 @@ - _DEBUG;_CONSOLE;%(PreprocessorDefinitions) + _DEBUG;_CONSOLE;_AMD64_;%(PreprocessorDefinitions) true - $(SolutionDir)include;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\ubpf\vm;$(OutDir);%(AdditionalIncludeDirectories) + $(SolutionDir)include;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\ubpf\vm;$(SolutionDir)spec\elf;$(OutDir);%(AdditionalIncludeDirectories) Console @@ -127,7 +127,7 @@ true NDEBUG;_CONSOLE;%(PreprocessorDefinitions) true - $(SolutionDir)include;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\ubpf\vm;$(OutDir);%(AdditionalIncludeDirectories) + $(SolutionDir)include;$(SolutionDir)external\ebpf-verifier\external\ELFIO;$(SolutionDir)external\ubpf\vm;$(OutDir);$(SolutionDir)spec\elf;%(AdditionalIncludeDirectories) Console @@ -186,6 +186,10 @@ {75fe223a-3e45-4b0e-a2e8-04285e52e440} + + + {e2b1c5ce-99d2-4732-acfb-0133f31a450f} + diff --git a/tools/bpf2c/bpf2c.vcxproj.filters b/tools/bpf2c/bpf2c.vcxproj.filters index baa2cc7f56..0934c9ffcf 100644 --- a/tools/bpf2c/bpf2c.vcxproj.filters +++ b/tools/bpf2c/bpf2c.vcxproj.filters @@ -51,4 +51,7 @@ Source Files + + + \ No newline at end of file diff --git a/tools/bpf2c/bpf_code_generator.cpp b/tools/bpf2c/bpf_code_generator.cpp index f87e6a5881..629de6b81d 100644 --- a/tools/bpf2c/bpf_code_generator.cpp +++ b/tools/bpf2c/bpf_code_generator.cpp @@ -108,11 +108,11 @@ bpf_code_generator::get_register_name(uint8_t id) } } -bpf_code_generator::bpf_code_generator(const std::string& path, const std::string& c_name) +bpf_code_generator::bpf_code_generator(std::istream& stream, const std::string& c_name) : current_section(nullptr), c_name(c_name), path(path) { - if (!reader.load(path)) { - throw std::runtime_error(std::string("Can't process ELF file ") + path); + if (!reader.load(stream)) { + throw std::runtime_error(std::string("Can't process ELF file ")); } extract_btf_information(); diff --git a/tools/bpf2c/bpf_code_generator.h b/tools/bpf2c/bpf_code_generator.h index 0d000e2be4..a64c70c857 100644 --- a/tools/bpf2c/bpf_code_generator.h +++ b/tools/bpf2c/bpf_code_generator.h @@ -21,10 +21,10 @@ class bpf_code_generator /** * @brief Construct a new bpf code generator object. * - * @param[in] path Path to the eBPF file to parse. + * @param[in] stream Stream containing the eBPF file to parse. * @param[in] c_name C compatible name to export this as. */ - bpf_code_generator(const std::string& path, const std::string& c_name); + bpf_code_generator(std::istream& stream, const std::string& c_name); /** * @brief Construct a new bpf code generator object from raw eBPF byte code.