Add option to control the level of verbosity emitted by verifier. (#3570)

* Add option to control the level of verbosity emitted by verifier.

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

* Re-order enums to make normal < informational < verbose

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

* Apply suggestions from code review

Co-authored-by: Dave Thaler <dthaler1968@gmail.com>

* PR feedback

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

* Workaround for verifier failure #643

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

* Revert change in ebpf-service verification path

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

---------

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>
Co-authored-by: Alan Jowett <alan.jowett@microsoft.com>
Co-authored-by: Dave Thaler <dthaler1968@gmail.com>
This commit is contained in:
Alan Jowett 2024-05-23 07:02:34 -07:00 коммит произвёл GitHub
Родитель 98b7495119
Коммит aed27b488b
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: B5690EEEBB952194
10 изменённых файлов: 146 добавлений и 77 удалений

Просмотреть файл

@ -81,10 +81,16 @@ r0 and r1, where r0 is for the return value and r1 holds
the hook context (ctx) structure pointer that is
passed to the program as its first argument.
**Step 4)** To understand what went wrong, we can ask netsh for the verbose output by using "level=verbose":
**Step 4)** To understand what went wrong, we can ask netsh for the informational or verbose output by using
"level=informational" or "level=verbose":
Note: Informational level will only show the first failure the verifier encounters on a specific path and not show
dependent failures. Verbose level will show both the initial failures as well as failures arising from that initial
failure. Informational is usually sufficient to understand the root cause of a failure, while verbose is useful to
gain a deeper understanding of what the impact of this failure is.
```
> netsh ebpf show ver droppacket_unsafe.o .text level=verbose
> netsh ebpf show ver droppacket_unsafe.o .text level=informational
Verification failed
Verification report:
@ -328,10 +334,10 @@ The destination of jumps are shown after the goto. For example, instruction
3 will jump to instruction 19 if the condition is true.
**Step 7)** Let's now look at the verification failures of xdp_test using level=verbose:
**Step 7)** Let's now look at the verification failures of xdp_test using level=informational:
```
> netsh ebpf show ver droppacket_unsafe.o xdp_test level=verbose
> netsh ebpf show ver droppacket_unsafe.o xdp_test level=informational
...
Pre-invariant : [
instruction_count=3,
@ -599,7 +605,7 @@ which is passed as the map_key to `bpf_map_lookup_elem`. Let's see how the veri
understands this.
```
> netsh ebpf show ver droppacket_unsafe.o xdp_test level=verbose
> netsh ebpf show ver droppacket_unsafe.o xdp_test level=informational
...
Pre-invariant : [
instruction_count=28,

Просмотреть файл

@ -109,13 +109,20 @@ extern "C"
int max_loop_count;
} ebpf_api_verifier_stats_t;
typedef enum _ebpf_verification_verbosity
{
EBPF_VERIFICATION_VERBOSITY_NORMAL = 0,
EBPF_VERIFICATION_VERBOSITY_INFORMATIONAL = 1,
EBPF_VERIFICATION_VERBOSITY_VERBOSE = 2,
} ebpf_verification_verbosity_t;
/**
* @brief Verify that the program is safe to execute.
* @param[in] file Name of ELF file containing eBPF program.
* @param[in] section The name of the section to query.
* @param[in] program_type Optional program type.
* If NULL, the program type is derived from the section name.
* @param[in] verbose Obtain additional info about the programs.
* @param[in] verbosity How much additional info about the programs to obtain.
* @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
@ -128,7 +135,7 @@ extern "C"
_In_z_ const char* file,
_In_z_ const char* section,
_In_opt_ const ebpf_program_type_t* program_type,
bool verbose,
ebpf_verification_verbosity_t verbosity,
_Outptr_result_maybenull_z_ const char** report,
_Outptr_result_maybenull_z_ const char** error_message,
_Out_opt_ ebpf_api_verifier_stats_t* stats) EBPF_NO_EXCEPT;
@ -140,7 +147,7 @@ extern "C"
* @param[in] section The name of the section to query.
* @param[in] program_type Optional program type.
* If NULL, the program type is derived from the section name.
* @param[in] verbose Obtain additional info about the programs.
* @param[in] verbosity How much additional info about the programs to obtain.
* @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
@ -154,7 +161,7 @@ extern "C"
size_t data_length,
_In_z_ const char* section,
_In_opt_ const ebpf_program_type_t* program_type,
bool verbose,
ebpf_verification_verbosity_t verbosity,
_Outptr_result_maybenull_z_ const char** report,
_Outptr_result_maybenull_z_ const char** error_message,
_Out_opt_ ebpf_api_verifier_stats_t* stats) EBPF_NO_EXCEPT;

Просмотреть файл

@ -683,7 +683,7 @@ _ebpf_api_elf_verify_section_from_stream(
std::istream& stream,
const char* stream_name,
const char* section,
bool verbose,
ebpf_verification_verbosity_t verbosity,
const char** report,
const char** error_message,
ebpf_api_verifier_stats_t* stats) noexcept
@ -696,8 +696,9 @@ _ebpf_api_elf_verify_section_from_stream(
try {
const ebpf_platform_t* platform = &g_ebpf_platform_windows;
ebpf_verifier_options_t verifier_options = ebpf_verifier_default_options;
verifier_options.assume_assertions = verbosity < EBPF_VERIFICATION_VERBOSITY_VERBOSE;
verifier_options.check_termination = true;
verifier_options.print_invariants = verbose;
verifier_options.print_invariants = verbosity >= EBPF_VERIFICATION_VERBOSITY_INFORMATIONAL;
verifier_options.print_failures = true;
verifier_options.mock_map_fds = true;
verifier_options.print_line_info = true;
@ -771,7 +772,7 @@ static _Success_(return == 0) uint32_t _verify_section_from_string(
_In_z_ const char* name,
_In_z_ const char* section,
_In_opt_ const ebpf_program_type_t* program_type,
bool verbose,
ebpf_verification_verbosity_t verbosity,
_Outptr_result_maybenull_z_ const char** report,
_Outptr_result_maybenull_z_ const char** error_message,
_Out_opt_ ebpf_api_verifier_stats_t* stats) noexcept
@ -798,14 +799,14 @@ static _Success_(return == 0) uint32_t _verify_section_from_string(
set_global_program_and_attach_type(program_type, nullptr);
_verification_in_progress_helper helper;
return _ebpf_api_elf_verify_section_from_stream(stream, name, section, verbose, report, error_message, stats);
return _ebpf_api_elf_verify_section_from_stream(stream, name, section, verbosity, report, error_message, stats);
}
_Success_(return == 0) uint32_t ebpf_api_elf_verify_section_from_file(
_In_z_ const char* file,
_In_z_ const char* section,
_In_opt_ const ebpf_program_type_t* program_type,
bool verbose,
ebpf_verification_verbosity_t verbosity,
_Outptr_result_maybenull_z_ const char** report,
_Outptr_result_maybenull_z_ const char** error_message,
_Out_opt_ ebpf_api_verifier_stats_t* stats) noexcept
@ -817,7 +818,7 @@ _Success_(return == 0) uint32_t ebpf_api_elf_verify_section_from_file(
if (error) {
return error;
}
return _verify_section_from_string(data, file, section, program_type, verbose, report, error_message, stats);
return _verify_section_from_string(data, file, section, program_type, verbosity, report, error_message, stats);
}
_Success_(return == 0) uint32_t ebpf_api_elf_verify_section_from_memory(
@ -825,11 +826,11 @@ _Success_(return == 0) uint32_t ebpf_api_elf_verify_section_from_memory(
size_t data_length,
_In_z_ const char* section,
_In_opt_ const ebpf_program_type_t* program_type,
bool verbose,
ebpf_verification_verbosity_t verbosity,
_Outptr_result_maybenull_z_ const char** report,
_Outptr_result_maybenull_z_ const char** error_message,
_Out_opt_ ebpf_api_verifier_stats_t* stats) noexcept
{
return _verify_section_from_string(
std::string(data, data_length), "memory", section, program_type, verbose, report, error_message, stats);
std::string(data, data_length), "memory", section, program_type, verbosity, report, error_message, stats);
}

Просмотреть файл

@ -6,11 +6,13 @@
#include "tokens.h"
#include "utilities.h"
#include <cassert>
#include <iomanip>
#include <locale>
TOKEN_VALUE g_LevelEnum[2] = {
TOKEN_VALUE g_LevelEnum[3] = {
{L"normal", VL_NORMAL},
{L"informational", VL_INFORMATIONAL},
{L"verbose", VL_VERBOSE},
};
@ -325,8 +327,25 @@ handle_ebpf_show_verification(
}
}
ebpf_verification_verbosity_t verbosity = EBPF_VERIFICATION_VERBOSITY_NORMAL;
switch (level) {
case VL_NORMAL:
verbosity = EBPF_VERIFICATION_VERBOSITY_NORMAL;
break;
case VL_INFORMATIONAL:
verbosity = EBPF_VERIFICATION_VERBOSITY_INFORMATIONAL;
break;
case VL_VERBOSE:
verbosity = EBPF_VERIFICATION_VERBOSITY_VERBOSE;
break;
default:
// Assert this never happens.
assert(!"Invalid verbosity level");
break;
}
status = ebpf_api_elf_verify_section_from_file(
filename.c_str(), section.c_str(), &program_type, level == VL_VERBOSE, &report, &error_message, &stats);
filename.c_str(), section.c_str(), &program_type, verbosity, &report, &error_message, &stats);
if (status == ERROR_SUCCESS) {
std::cout << report;
std::cout << "\nProgram terminates within " << stats.max_loop_count << " loop iterations\n";

Просмотреть файл

@ -17,7 +17,8 @@
typedef enum
{
VL_NORMAL = 0,
VL_VERBOSE = 1,
VL_INFORMATIONAL = 1,
VL_VERBOSE = 2,
} VERBOSITY_LEVEL;
extern TOKEN_VALUE g_LevelEnum[2];
extern TOKEN_VALUE g_LevelEnum[3];

Просмотреть файл

@ -34,6 +34,7 @@ _analyze(raw_program& raw_prog, const char** error_message, uint32_t* error_mess
std::ostringstream oss;
options.no_simplify = true;
options.print_failures = true;
// Until https://github.com/vbpf/ebpf-verifier/issues/643 is fixed, don't set options.assume_assertions to true.
(void)ebpf_verify_program(oss, prog, raw_prog.info, &options, &stats);
*error_message = allocate_string(oss.str(), error_message_size);

Просмотреть файл

@ -38,7 +38,13 @@ verify_program(_In_z_ const char* file, uint32_t expected_section_count)
const char* report = nullptr;
REQUIRE(
(result = ebpf_api_elf_verify_section_from_file(
file, section_name, &EBPF_PROGRAM_TYPE_XDP, false, &report, &log_buffer, &stats),
file,
section_name,
&EBPF_PROGRAM_TYPE_XDP,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&log_buffer,
&stats),
ebpf_free_string(log_buffer),
log_buffer = nullptr,
result == 0));

Просмотреть файл

@ -1051,7 +1051,13 @@ TEST_CASE("verify section", "[end_to_end]")
ebpf_api_verifier_stats_t stats;
REQUIRE(
(result = ebpf_api_elf_verify_section_from_file(
SAMPLE_PATH "test_sample_ebpf.o", "sample_ext", nullptr, false, &report, &error_message, &stats),
SAMPLE_PATH "test_sample_ebpf.o",
"sample_ext",
nullptr,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&error_message,
&stats),
ebpf_free_string(error_message),
error_message = nullptr,
result == 0));
@ -1075,7 +1081,7 @@ TEST_CASE("verify section with invalid program type", "[end_to_end]")
SAMPLE_PATH "test_sample_ebpf.o",
"sample_ext",
&EBPF_PROGRAM_TYPE_UNSPECIFIED,
false,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&error_message,
&stats);
@ -1192,7 +1198,13 @@ TEST_CASE("verify_test0", "[sample_extension]")
ebpf_api_verifier_stats_t stats;
REQUIRE(
(result = ebpf_api_elf_verify_section_from_file(
SAMPLE_PATH "test_sample_ebpf.o", "sample_ext", nullptr, false, &report, &error_message, &stats),
SAMPLE_PATH "test_sample_ebpf.o",
"sample_ext",
nullptr,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&error_message,
&stats),
ebpf_free_string(error_message),
error_message = nullptr,
result == 0));
@ -1215,7 +1227,13 @@ TEST_CASE("verify_test1", "[sample_extension]")
REQUIRE(
(result = ebpf_api_elf_verify_section_from_file(
SAMPLE_PATH "test_sample_ebpf.o", "sample_ext", nullptr, false, &report, &error_message, &stats),
SAMPLE_PATH "test_sample_ebpf.o",
"sample_ext",
nullptr,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&error_message,
&stats),
ebpf_free_string(error_message),
error_message = nullptr,
result == 0));

Просмотреть файл

@ -66,6 +66,27 @@ strip_paths(const std::string& original_string)
return output_stream.str();
}
void
test_expected_output_line_by_line(const std::string& expected_output, const std::string& actual_output)
{
// If the expected and actual output are the same, the test passes.
if (expected_output == actual_output)
return;
std::cerr << "Expected output:\n" << expected_output << "\n";
std::cerr << "Actual output:\n" << actual_output << "\n";
// If the expected and actual output are not the same, compare them line by line.
std::istringstream expected_output_stream(expected_output);
std::istringstream actual_output_stream(actual_output);
std::string expected_line;
std::string actual_line;
while (std::getline(expected_output_stream, expected_line) && std::getline(actual_output_stream, actual_line)) {
REQUIRE(expected_line == actual_line);
}
}
TEST_CASE("show disassembly bpf_call.o", "[netsh][disassembly]")
{
// Start the test helper so the netsh command can get helper prototypes.
@ -415,45 +436,31 @@ TEST_CASE("show verification xdp_datasize_unsafe.o", "[netsh][verification]")
_run_netsh_command(handle_ebpf_show_verification, L"xdp_datasize_unsafe.o", L"xdp", nullptr, &result);
REQUIRE(result == ERROR_SUPPRESS_OUTPUT);
output = strip_paths(output);
REQUIRE(
output == "Verification failed\n"
"\n"
"Verification report:\n"
"\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"4: Invalid type (r3.type in {number, ctx, stack, packet, shared})\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"5: Invalid type (valid_access(r3.offset) for comparison/subtraction)\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"5: Invalid type (r3.type == non_map_fd)\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"5: Cannot subtract pointers to different regions (r3.type == r1.type in {ctx, stack, packet})\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:38\n"
"; if (ethernet_header->Type != ntohs(ETHERNET_TYPE_IPV4) && ethernet_header->Type != "
"ntohs(ETHERNET_TYPE_IPV6)) {\n"
"6: Invalid type (r2.type in {ctx, stack, packet, shared})\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:38\n"
"; if (ethernet_header->Type != ntohs(ETHERNET_TYPE_IPV4) && ethernet_header->Type != "
"ntohs(ETHERNET_TYPE_IPV6)) {\n"
"6: Invalid type (valid_access(r2.offset+12, width=2) for read)\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:38\n"
"; if (ethernet_header->Type != ntohs(ETHERNET_TYPE_IPV4) && ethernet_header->Type != "
"ntohs(ETHERNET_TYPE_IPV6)) {\n"
"7: Invalid type (r1.type == number)\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:38\n"
"; if (ethernet_header->Type != ntohs(ETHERNET_TYPE_IPV4) && ethernet_header->Type != "
"ntohs(ETHERNET_TYPE_IPV6)) {\n"
"8: Invalid type (r1.type == number)\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:43\n"
"; return rc;\n"
"10: Invalid type (r0.type == number)\n"
"\n"
"9 errors\n"
"\n");
// Perform a line by line comparison to detect any differences.
std::string expected_output = "Verification failed\n"
"\n"
"Verification report:\n"
"\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"4: Invalid type (r3.type in {number, ctx, stack, packet, shared})\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:32\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"4: Code is unreachable after 4\n"
"\n"
"1 errors\n"
"\n";
// Split both output and expected_output into lines.
std::istringstream output_stream(output);
std::istringstream expected_output_stream(expected_output);
std::string output_line;
std::string expected_output_line;
while (std::getline(output_stream, output_line) && std::getline(expected_output_stream, expected_output_line)) {
REQUIRE(output_line == expected_output_line);
}
}
TEST_CASE("show verification printk_unsafe.o", "[netsh][verification]")
@ -466,17 +473,20 @@ TEST_CASE("show verification printk_unsafe.o", "[netsh][verification]")
_run_netsh_command(handle_ebpf_show_verification, L"printk_unsafe.o", L"bind", nullptr, &result);
REQUIRE(result == ERROR_SUPPRESS_OUTPUT);
output = strip_paths(output);
REQUIRE(
output == "Verification failed\n"
"\n"
"Verification report:\n"
"\n"
"; ./tests/sample/unsafe/printk_unsafe.c:22\n"
"; bpf_printk(\"ctx: %u\", (uint64_t)ctx);\n"
"7: Invalid type (r3.type == number)\n"
"\n"
"1 errors\n"
"\n");
std::string expected_output = "Verification failed\n"
"\n"
"Verification report:\n"
"\n"
"; ./tests/sample/unsafe/printk_unsafe.c:22\n"
"; bpf_printk(\"ctx: %u\", (uint64_t)ctx);\n"
"7: Invalid type (r3.type == number)\n"
"; ./tests/sample/unsafe/printk_unsafe.c:22\n"
"; bpf_printk(\"ctx: %u\", (uint64_t)ctx);\n"
"7: Code is unreachable after 7\n"
"\n"
"1 errors\n"
"\n";
test_expected_output_line_by_line(expected_output, output);
}
void

Просмотреть файл

@ -311,7 +311,7 @@ main(int argc, char** argv)
data.size(),
section.raw().c_str(),
&program_type,
false,
EBPF_VERIFICATION_VERBOSITY_NORMAL,
&report,
&error_message,
&stats) != 0) {