diff --git a/docs/tutorial.md b/docs/tutorial.md index 9b44b15ed2..2bae68edbd 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -373,39 +373,58 @@ joins. **Step 4)** View verifier verbose output -(TODO: this section needs to be updated for netsh) We can view verbose output to see what the verifier is actually doing, -using the `-v` argument: +using the "level=verbose" option to "show verification": ``` -> Release\check.exe -v ..\bpf.o +> netsh ebpf show verification bpf.o level=verbose -{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0] -} -Numbers -> {} +Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[0] + } +Stack: Numbers -> {} +entry: + goto 0; + +Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[1] + } +Stack: Numbers -> {} + +Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[1] + } +Stack: Numbers -> {} 0: r0 = 0; goto 1; -{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4] -} -Numbers -> {} +Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[3], r0.value=[0], r0.type=number + } +Stack: Numbers -> {} -{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4] -} -Numbers -> {} +Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[3], r0.value=[0], r0.type=number + } +Stack: Numbers -> {} 1: - assert r0 : num; + assert r0 is number; exit; + goto exit; +Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[6], r0.value=[0], r0.type=number + } +Stack: Numbers -> {} + +Preconditions : {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[6], r0.value=[0], r0.type=number + } +Stack: Numbers -> {} +exit: -{r10 -> [512, +oo], off10 -> [512], t10 -> [-2], r1 -> [1, 2147418112], off1 -> [0], t1 -> [-3], packet_size -> [0, 65534], meta_offset -> [-4098, 0], r0 -> [0], t0 -> [-4] -} -Numbers -> {} +Postconditions: {r10.value=[512, 2147418112], r10.offset=[512], r10.type=stack_pointer, r1.value=[1, 2147418112], r1.offset=[0], r1.type=ctx_pointer, packet_size=[0, 65534], meta_offset=[-4098, 0], instruction_count=[7], r0.value=[0], r0.type=number + } +Stack: Numbers -> {} -0 warnings -1,0.029,6692 + +0 errors +Verification succeeded ``` Normally we wouldn't need to do this, but it is illustrative to see how the @@ -416,8 +435,7 @@ Each instruction is shown as before, but is preceded by its preconditions "oo" means infinity, "r0" through "r10" are registers (r10 is the stack pointer, r0 is used for return values, r1-5 are used to pass args to other -functions, r6 is the 'ctx' pointer, etc., "t0" through "t10" contains the -type of value in the associated register, where -4 means an integer, etc. +functions, r6 is the 'ctx' pointer, etc. "meta_offset" is the number of bytes of packet metadata preceding (i.e., with negative offset from) the start of the packet buffer. diff --git a/scripts/.check-license.ignore b/scripts/.check-license.ignore index 2f8ee66f2e..9e38617c23 100644 --- a/scripts/.check-license.ignore +++ b/scripts/.check-license.ignore @@ -2,6 +2,7 @@ # File extensions that don't support embedding license info .*\.md$ +.*\.rc$ .*\.sln$ # Other Files diff --git a/src/ebpf/include/ebpf_api.h b/src/ebpf/include/ebpf_api.h index 6e3c169b65..d825815dad 100644 --- a/src/ebpf/include/ebpf_api.h +++ b/src/ebpf/include/ebpf_api.h @@ -226,13 +226,15 @@ extern "C" * @brief Convert an eBPF program to human readable byte code. * @param[in] file Name of ELF file containing eBPF program. * @param[in] section The name of the section to query. + * @param[in] verbose Obtain additional information about the programs. * @param[out] report Points to a text section describing why the program * failed verification. * @param[out] error_message On failure points to a text description of * the error. */ uint32_t - ebpf_api_elf_verify_section(const char* file, const char* section, const char** report, const char** error_message); + ebpf_api_elf_verify_section( + const char* file, const char* section, bool verbose, const char** report, const char** error_message); /** * @brief Free a TLV returned from ebpf_api_elf_enumerate_sections diff --git a/src/ebpf/libs/api/Verifier.cpp b/src/ebpf/libs/api/Verifier.cpp index 9f0392e259..c152452fec 100644 --- a/src/ebpf/libs/api/Verifier.cpp +++ b/src/ebpf/libs/api/Verifier.cpp @@ -219,7 +219,8 @@ ebpf_api_elf_disassemble_section( } uint32_t -ebpf_api_elf_verify_section(const char* file, const char* section, const char** report, const char** error_message) +ebpf_api_elf_verify_section( + const char* file, const char* section, bool verbose, const char** report, const char** error_message) { std::ostringstream error; std::ostringstream output; @@ -227,6 +228,7 @@ ebpf_api_elf_verify_section(const char* file, const char* section, const char** const ebpf_platform_t* platform = &g_ebpf_platform_windows; ebpf_verifier_options_t verifier_options = ebpf_verifier_default_options; verifier_options.check_termination = true; + verifier_options.print_invariants = verbose; verifier_options.print_failures = true; verifier_options.mock_map_fds = true; diff --git a/src/test/end_to_end/end_to_end.cpp b/src/test/end_to_end/end_to_end.cpp index 5d3eed230b..5ed56d89d0 100644 --- a/src/test/end_to_end/end_to_end.cpp +++ b/src/test/end_to_end/end_to_end.cpp @@ -360,7 +360,7 @@ TEST_CASE("verify section", "[verify section]") REQUIRE(ebpf_api_initiate() == ERROR_SUCCESS); ec_initialized = true; - REQUIRE(ebpf_api_elf_verify_section(SAMPLE_PATH "droppacket.o", "xdp", &report, &error_message) == 0); + REQUIRE(ebpf_api_elf_verify_section(SAMPLE_PATH "droppacket.o", "xdp", false, &report, &error_message) == 0); REQUIRE(report != nullptr); REQUIRE(error_message == nullptr); } diff --git a/src/tools/netsh/ebpfnetsh.rc b/src/tools/netsh/ebpfnetsh.rc index f76de5be83..1a17cf3c7d 100644 --- a/src/tools/netsh/ebpfnetsh.rc +++ b/src/tools/netsh/ebpfnetsh.rc @@ -199,6 +199,7 @@ BEGIN "Shows results of trying to verify an eBPF program.\n" HLP_EBPF_SHOW_VERIFICATION_EX "\ \nUsage: %1!s! [filename=] [[section=]]\ +\n [[level=]normal|verbose]\ \n\ \nParameters:\ \n\ @@ -207,9 +208,12 @@ BEGIN \n section - Optionally the name of the section containing the\ \n program. If not specified, the default is to use the\ \n first code section.\ +\n level - One of the following values:\ +\n normal: Only display details of errors. This is the\ +\n default.\ +\n verbose: Display details on every instruction.\ \n\ -\nRemarks: Shows the verbose verifier results of the specified eBPF\ -\n program.\ +\nRemarks: Shows the verifier results of the specified eBPF program.\ \n" END diff --git a/src/tools/netsh/elf.cpp b/src/tools/netsh/elf.cpp index 51dd2fa54b..b19e172849 100644 --- a/src/tools/netsh/elf.cpp +++ b/src/tools/netsh/elf.cpp @@ -197,12 +197,14 @@ handle_ebpf_show_verification( TAG_TYPE tags[] = { {TOKEN_FILENAME, NS_REQ_PRESENT, FALSE}, {TOKEN_SECTION, NS_REQ_ZERO, FALSE}, + {TOKEN_LEVEL, NS_REQ_ZERO, FALSE}, }; ULONG tag_type[_countof(tags)] = {0}; ULONG status = PreprocessCommand(nullptr, argv, current_index, argc, tags, _countof(tags), 0, _countof(tags), tag_type); + VERBOSITY_LEVEL level = VL_NORMAL; std::string filename; std::string section = ""; // Use the first code section by default. for (int i = 0; (status == NO_ERROR) && ((i + current_index) < argc); i++) { @@ -217,6 +219,14 @@ handle_ebpf_show_verification( section = down_cast_from_wstring(std::wstring(argv[current_index + i])); break; } + case 2: // LEVEL + { + status = MatchEnumTag(NULL, argv[current_index + i], _countof(g_LevelEnum), g_LevelEnum, (PULONG)&level); + if (status != NO_ERROR) { + status = ERROR_INVALID_PARAMETER; + } + break; + } default: status = ERROR_INVALID_SYNTAX; break; @@ -229,9 +239,10 @@ handle_ebpf_show_verification( const char* report; const char* error_message; - status = ebpf_api_elf_verify_section(filename.c_str(), section.c_str(), &report, &error_message); + status = + ebpf_api_elf_verify_section(filename.c_str(), section.c_str(), level == VL_VERBOSE, &report, &error_message); if (status == ERROR_SUCCESS) { - std::cout << "\nVerification succeeded\n"; + std::cout << report; return NO_ERROR; } else { if (error_message) {