Skip to content

Commit

Permalink
Update verifier to latest (#4033)
Browse files Browse the repository at this point in the history
* Update verifier

Signed-off-by: Dave Thaler <[email protected]>

* Make some more tests pass

Signed-off-by: Dave Thaler <[email protected]>

* More test fixes

---------

Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
dthaler authored Nov 23, 2024
1 parent c514000 commit 726a856
Show file tree
Hide file tree
Showing 10 changed files with 97 additions and 33 deletions.
2 changes: 1 addition & 1 deletion external/ebpf-verifier
Submodule ebpf-verifier updated 72 files
+1 −1 external/bpf_conformance
+1 −1 external/libbtf
+123 −173 src/asm_cfg.cpp
+37 −37 src/asm_files.cpp
+5 −0 src/asm_files.hpp
+1 −2 src/asm_marshal.cpp
+112 −104 src/asm_ostream.cpp
+0 −58 src/asm_ostream.hpp
+6 −2 src/asm_parse.cpp
+29 −77 src/asm_syntax.hpp
+5 −5 src/asm_unmarshal.cpp
+15 −7 src/assertions.cpp
+21 −15 src/config.hpp
+3 −9 src/crab/array_domain.cpp
+0 −2 src/crab/array_domain.hpp
+211 −342 src/crab/cfg.hpp
+440 −0 src/crab/ebpf_checker.cpp
+98 −2,719 src/crab/ebpf_domain.cpp
+35 −139 src/crab/ebpf_domain.hpp
+2,442 −0 src/crab/ebpf_transformer.cpp
+28 −20 src/crab/fwd_analyzer.cpp
+6 −2 src/crab/fwd_analyzer.hpp
+2 −1 src/crab/interval.hpp
+94 −0 src/crab/label.hpp
+53 −38 src/crab/split_dbm.cpp
+1 −1 src/crab/split_dbm.hpp
+5 −4 src/crab/thresholds.cpp
+1 −1 src/crab/thresholds.hpp
+1 −1 src/crab/type_domain.cpp
+4 −2 src/crab/var_factory.cpp
+1 −0 src/crab/variable.hpp
+8 −7 src/crab_utils/debug.hpp
+0 −5 src/crab_utils/stats.cpp
+23 −4 src/crab_utils/stats.hpp
+129 −196 src/crab_verifier.cpp
+36 −9 src/crab_verifier.hpp
+1 −1 src/linux/gpl/spec_prototypes.cpp
+20 −18 src/linux/linux_platform.cpp
+2 −0 src/linux/linux_platform.hpp
+48 −24 src/main/check.cpp
+18 −16 src/main/linux_verifier.cpp
+1 −1 src/main/run_yaml.cpp
+0 −16 src/main/utils.hpp
+13 −11 src/spec_type_descriptors.hpp
+48 −61 src/test/ebpf_yaml.cpp
+1 −1 src/test/ebpf_yaml.hpp
+1 −1 src/test/test_conformance.cpp
+0 −1 src/test/test_marshal.cpp
+0 −1 src/test/test_print.cpp
+70 −53 src/test/test_verify.cpp
+30 −30 src/test/test_wto.cpp
+1 −1 src/test/test_yaml.cpp
+6 −24 test-data/add.yaml
+35 −46 test-data/assign.yaml
+86 −86 test-data/atomic.yaml
+7 −14 test-data/call.yaml
+7 −14 test-data/callx.yaml
+11 −20 test-data/full64.yaml
+61 −136 test-data/jump.yaml
+62 −106 test-data/loop.yaml
+34 −53 test-data/movsx.yaml
+43 −16 test-data/packet.yaml
+41 −60 test-data/pointer.yaml
+11 −20 test-data/sdivmod.yaml
+7 −10 test-data/sext.yaml
+70 −309 test-data/shift.yaml
+11 −13 test-data/stack.yaml
+2 −4 test-data/subtract.yaml
+12 −22 test-data/udivmod.yaml
+38 −41 test-data/uninit.yaml
+6 −6 test-data/unop.yaml
+196 −224 test-data/unsigned.yaml
11 changes: 5 additions & 6 deletions libs/api/Verifier.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -652,10 +652,10 @@ _ebpf_api_elf_verify_program_from_stream(
ebpf_verifier_options_t verifier_options{};
verifier_options.assume_assertions = verbosity < EBPF_VERIFICATION_VERBOSITY_VERBOSE;
verifier_options.cfg_opts.check_for_termination = true;
verifier_options.print_invariants = verbosity >= EBPF_VERIFICATION_VERBOSITY_INFORMATIONAL;
verifier_options.print_failures = true;
verifier_options.verbosity_opts.print_invariants = verbosity >= EBPF_VERIFICATION_VERBOSITY_INFORMATIONAL;
verifier_options.verbosity_opts.print_failures = true;
verifier_options.mock_map_fds = true;
verifier_options.print_line_info = true;
verifier_options.verbosity_opts.print_line_info = true;
if (!stream) {
throw std::runtime_error(std::string("No such file or directory opening ") + stream_name);
}
Expand Down Expand Up @@ -683,9 +683,8 @@ _ebpf_api_elf_verify_program_from_stream(
}
auto& program = std::get<InstructionSeq>(programOrError);

verifier_options.cfg_opts.simplify = false;
bool res =
ebpf_verify_program(output, program, raw_program.info, verifier_options, (ebpf_verifier_stats_t*)stats);
verifier_options.verbosity_opts.simplify = false;
bool res = ebpf_verify_program(output, program, raw_program.info, verifier_options, stats);
if (!res) {
error << "Verification failed";
*error_message = allocate_string(error.str());
Expand Down
1 change: 1 addition & 0 deletions libs/api/crab_verifier_wrapper.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#pragma warning(disable : 4100) // 'identifier' : unreferenced formal parameter
#pragma warning(disable : 4244) // 'conversion' conversion from 'type1' to
// 'type2', possible loss of data
#pragma warning(disable : 4267) // conversion from 'size_t' to 'int', possible loss of data
#pragma warning(disable : 26451) // Arithmetic overflow
#pragma warning(disable : 26450) // Arithmetic overflow
#pragma warning(disable : 26450) // Arithmetic overflow
Expand Down
39 changes: 39 additions & 0 deletions libs/api_common/api_common.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -156,3 +156,42 @@ ebpf_clear_thread_local_storage() noexcept
set_verification_in_progress(false);
clean_up_sync_device_handle();
}

// Returned value is true if the program passes verification.
bool
ebpf_verify_program(
std::ostream& os,
_In_ const InstructionSeq& prog,
_In_ const program_info& info,
_In_ const ebpf_verifier_options_t& options,
_Out_ ebpf_api_verifier_stats_t* stats)
{
stats->total_unreachable = 0;
stats->total_warnings = 0;
stats->max_loop_count = 0;

// Convert the instruction sequence to a control-flow graph.
try {
const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts);
auto invariants = analyze(cfg);
if (options.verbosity_opts.print_invariants) {
invariants.print_invariants(os, cfg);
}
bool pass;
if (options.verbosity_opts.print_failures) {
auto report = invariants.check_assertions(cfg);
thread_local_options.verbosity_opts.print_line_info = true;
report.print_warnings(os);
pass = report.verified();
stats->total_warnings = (int)report.warning_set().size();
stats->total_unreachable = (int)report.reachability_set().size();
} else {
pass = invariants.verified(cfg);
}
stats->max_loop_count = invariants.max_loop_count();
return pass;
} catch (UnmarshalError& e) {
os << "error: " << e.what() << std::endl;
return false;
}
}
8 changes: 8 additions & 0 deletions libs/api_common/api_common.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -238,3 +238,11 @@ set_program_under_verification(ebpf_handle_t program);
*/
void
ebpf_clear_thread_local_storage() noexcept;

bool
ebpf_verify_program(
std::ostream& os,
_In_ const InstructionSeq& prog,
_In_ const program_info& info,
_In_ const ebpf_verifier_options_t& options,
_Out_ ebpf_api_verifier_stats_t* stats);
1 change: 1 addition & 0 deletions libs/api_common/ebpf_verifier_wrapper.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#pragma warning(disable : 4100) // 'identifier' : unreferenced formal parameter
#pragma warning(disable : 4244) // 'conversion' conversion from 'type1' to
// 'type2', possible loss of data
#pragma warning(disable : 4267) // conversion from 'size_t' to 'int', possible loss of data
#pragma warning(disable : 26451) // Arithmetic overflow
#pragma warning(disable : 26450) // Arithmetic overflow
#pragma warning(disable : 26439) // This kind of function may not
Expand Down
2 changes: 1 addition & 1 deletion libs/api_common/windows_platform_common.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -775,7 +775,7 @@ clear_ebpf_provider_data()
_Success_(return == EBPF_SUCCESS) ebpf_result_t
get_program_type_info_from_tls(_Outptr_ const ebpf_program_info_t** info)
{
const GUID* program_type = reinterpret_cast<const GUID*>(global_program_info->type.platform_specific_data);
const GUID* program_type = reinterpret_cast<const GUID*>(thread_local_program_info->type.platform_specific_data);
ebpf_result_t result = EBPF_SUCCESS;

_load_ebpf_provider_data();
Expand Down
6 changes: 3 additions & 3 deletions libs/service/verifier_service.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,14 @@ _analyze(raw_program& raw_prog, const char** error_message, uint32_t* error_mess

// First try optimized for the success case.
ebpf_verifier_options_t options{};
ebpf_verifier_stats_t stats;
ebpf_api_verifier_stats_t stats;
options.cfg_opts.check_for_termination = true;
bool res = ebpf_verify_program(std::cout, prog, raw_prog.info, options, &stats);
if (!res) {
// On failure, retry to get the more detailed error message.
std::ostringstream oss;
options.cfg_opts.simplify = false;
options.print_failures = true;
options.verbosity_opts.simplify = false;
options.verbosity_opts.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);

Expand Down
56 changes: 36 additions & 20 deletions tests/end_to_end/netsh_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,7 @@ TEST_CASE("show sections bpf.o .text", "[netsh][sections]")
"arith32 : 0\n"
"arith64 : 1\n"
"assign : 1\n"
"basic_blocks : 2\n"
"basic_blocks : 4\n"
"call_1 : 0\n"
"call_mem : 0\n"
"call_nomem : 0\n"
Expand All @@ -204,7 +204,7 @@ TEST_CASE("show sections bpf.o .text", "[netsh][sections]")
"load : 0\n"
"load_store : 0\n"
"map_in_map : 0\n"
"other : 1\n"
"other : 3\n"
"packet_access: 0\n"
"reallocate : 0\n"
"store : 0\n"
Expand Down Expand Up @@ -406,7 +406,6 @@ TEST_CASE("show verification bpf.o", "[netsh][verification]")
REQUIRE(result == NO_ERROR);
REQUIRE(
output == "\n"
"\n"
"Verification succeeded\n"
"Program terminates within 0 loop iterations\n");
}
Expand All @@ -421,7 +420,6 @@ TEST_CASE("show verification droppacket.o", "[netsh][verification]")
REQUIRE(result == NO_ERROR);
REQUIRE(
output == "\n"
"\n"
"Verification succeeded\n"
"Program terminates within 0 loop iterations\n");
}
Expand All @@ -443,6 +441,7 @@ TEST_CASE("show verification xdp_adjust_head_unsafe.o", "[netsh][verification]")
"\n"
"; ./tests/sample/unsafe/xdp_adjust_head_unsafe.c:43\n"
"; ethernet_header->Type = 0x0800;\n"
"\n"
"17: Upper bound must be at most packet_size (valid_access(r1.offset+12, width=2) for write)\n"
"\n"
"1 errors\n"
Expand All @@ -466,9 +465,12 @@ TEST_CASE("show verification droppacket_unsafe.o", "[netsh][verification]")
"\n"
"; ./tests/sample/unsafe/droppacket_unsafe.c:42\n"
"; if (ip_header->Protocol == IPPROTO_UDP) {\n"
"\n"
"2: Upper bound must be at most packet_size (valid_access(r1.offset+9, width=1) for read)\n"
"\n"
"; ./tests/sample/unsafe/droppacket_unsafe.c:43\n"
"; if (ntohs(udp_header->length) <= sizeof(UDP_HEADER)) {\n"
"\n"
"4: Upper bound must be at most packet_size (valid_access(r1.offset+24, width=2) for read)\n"
"\n"
"2 errors\n"
Expand All @@ -487,19 +489,35 @@ TEST_CASE("show verification xdp_datasize_unsafe.o", "[netsh][verification]")
output = strip_paths(output);

// 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:33\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:33\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"4: Code is unreachable after 4\n"
"\n"
"1 errors\n"
"\n";
std::string expected_output =
"Verification failed\n"
"\n"
"Verification report:\n"
"\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:33\n"
"; if (next_header + sizeof(ETHERNET_HEADER) > (char*)ctx->data_end) {\n"
"\n"
"4: Invalid type (r3.type in {number, ctx, stack, packet, shared})\n"
"5: Invalid type (valid_access(r3.offset) for comparison/subtraction)\n"
"5: Invalid type (r3.type in {number, ctx, stack, packet, shared})\n"
"5: Cannot subtract pointers to different regions (r3.type == r1.type in {ctx, stack, packet})\n"
"\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:39\n"
"; if (ethernet_header->Type != ntohs(ETHERNET_TYPE_IPV4) && ethernet_header->Type != "
"ntohs(ETHERNET_TYPE_IPV6)) {\n"
"\n"
"6: Invalid type (r2.type in {ctx, stack, packet, shared})\n"
"6: Invalid type (valid_access(r2.offset+12, width=2) for read)\n"
"8: Invalid type (r1.type == number)\n"
"10: Invalid type (r1.type == number)\n"
"\n"
"; ./tests/sample/unsafe/xdp_datasize_unsafe.c:44\n"
"; return rc;\n"
"\n"
"12: Invalid type (r0.type == number)\n"
"\n"
"9 errors\n"
"\n";

// Split both output and expected_output into lines.
std::istringstream output_stream(output);
Expand Down Expand Up @@ -528,10 +546,8 @@ TEST_CASE("show verification printk_unsafe.o", "[netsh][verification]")
"\n"
"; ./tests/sample/unsafe/printk_unsafe.c:22\n"
"; bpf_printk(\"ctx: %u\", (uint64_t)ctx);\n"
"\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";
Expand Down
4 changes: 2 additions & 2 deletions tests/unit/libbpf_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ TEST_CASE("invalid bpf_load_program", "[libbpf][deprecated]")
REQUIRE(program_fd < 0);
#if !defined(CONFIG_BPF_JIT_DISABLED)
REQUIRE(errno == EACCES);
REQUIRE(strcmp(log_buffer, "\n0: Invalid type (r0.type == number)\n\n") == 0);
REQUIRE(strcmp(log_buffer, "0: Invalid type (r0.type == number)\n\n") == 0);
#else
REQUIRE(errno == ENOTSUP);
#endif
Expand All @@ -244,7 +244,7 @@ TEST_CASE("invalid bpf_prog_load", "[libbpf]")
REQUIRE(program_fd < 0);
#if !defined(CONFIG_BPF_JIT_DISABLED)
REQUIRE(errno == EACCES);
REQUIRE(strcmp(log_buffer, "\n0: Invalid type (r0.type == number)\n\n") == 0);
REQUIRE(strcmp(log_buffer, "0: Invalid type (r0.type == number)\n\n") == 0);
#else
REQUIRE(errno == ENOTSUP);
#endif
Expand Down

0 comments on commit 726a856

Please sign in to comment.