From 39874a145c3edde534a91f58cf2b062273384e1b Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 15 Jan 2025 12:22:03 -0800 Subject: [PATCH 1/4] First pass Signed-off-by: Alan Jowett --- external/ebpf-verifier | 2 +- libfuzzer/libfuzz_harness.cc | 197 ++++++++++++++++++----------------- 2 files changed, 104 insertions(+), 95 deletions(-) diff --git a/external/ebpf-verifier b/external/ebpf-verifier index e92408ce0..c752a2efd 160000 --- a/external/ebpf-verifier +++ b/external/ebpf-verifier @@ -1 +1 @@ -Subproject commit e92408ce0fc8c26a6c8b2e1bc0ef59ea9f8d3072 +Subproject commit c752a2efd89a782f3226642c151c6b0e6b514272 diff --git a/libfuzzer/libfuzz_harness.cc b/libfuzzer/libfuzz_harness.cc index 6384c27e8..5841a64a0 100644 --- a/libfuzzer/libfuzz_harness.cc +++ b/libfuzzer/libfuzz_harness.cc @@ -359,20 +359,29 @@ try { // Enable termination checking and pre-invariant storage. options.cfg_opts.check_for_termination = true; - options.cfg_opts.simplify = false; - options.print_invariants = g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT"); - options.print_failures = g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT"); - options.store_pre_invariants = g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK"); + options.verbosity_opts.simplify = false; + options.verbosity_opts.print_invariants = g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT"); + options.verbosity_opts.print_failures = g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT"); ebpf_verifier_stats_t stats; std::ostringstream error_stream; + // Convert the instruction sequence to a control-flow graph. + auto program = Program::from_sequence(prog, info, options.cfg_opts); + // Verify the program. This will return false or throw an exception if the program is invalid. - bool result = ebpf_verify_program(error_stream, prog, raw_prog.info, options, &stats); + auto invariants = analyze(program); + + bool result = invariants.verified(program); + if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT")) { + auto report = invariants.check_assertions(program); + print_warnings(error_stream, report); + + print_invariants(error_stream, program, false, invariants); + std::cout << "verifier stats:" << std::endl; - std::cout << "total_unreachable: " << stats.total_unreachable << std::endl; std::cout << "total_warnings: " << stats.total_warnings << std::endl; std::cout << "max_loop_count: " << stats.max_loop_count << std::endl; std::cout << "result: " << result << std::endl; @@ -526,94 +535,94 @@ ubpf_debug_function( } - if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK")) { - ubpf_context_t* ubpf_context = reinterpret_cast(context); - UNREFERENCED_PARAMETER(stack_start); - UNREFERENCED_PARAMETER(stack_length); - UNREFERENCED_PARAMETER(stack_mask); - - // Check if this is an local call or exit instruction. - const ebpf_inst* inst = reinterpret_cast(ubpf_context->program_start); - inst += program_counter; - - std::string label; - - for (size_t i = 0; i < g_pc_stack.size(); i++) { - label += std::to_string(g_pc_stack[i]) + "/"; - } - - label += std::to_string(program_counter) + ":-1"; - - // Local call. - if (inst->opcode == EBPF_OP_CALL && inst->src == 1) { - g_pc_stack.push_back(program_counter); - } - - // Exit. - if (inst->opcode == EBPF_OP_EXIT) { - if (!g_pc_stack.empty()) { - g_pc_stack.pop_back(); - } - } - - - if (program_counter == 0) { - return; - } - - // Build set of string constraints from the register values. - std::set constraints; - constraints.insert("packet_size=" + std::to_string(ubpf_context->original_data_end - ubpf_context->original_data)); - for (int i = 0; i < 10; i++) { - if ((register_mask & (1 << i)) == 0) { - continue; - } - uint64_t reg = registers[i]; - std::string register_name = "r" + std::to_string(i); - - // Given the register value, classify it as packet, context, stack, or unknown and add the appropriate - // constraint. - address_type_t type = ubpf_classify_address(ubpf_context, reg); - switch (type) { - case address_type_t::Packet: - constraints.insert(register_name + ".type=packet"); - constraints.insert(register_name + ".packet_offset=" + std::to_string(reg - ubpf_context->data)); - constraints.insert( - register_name + ".packet_size=" + std::to_string(ubpf_context->data_end - ubpf_context->data)); - break; - - case address_type_t::Context: - constraints.insert(register_name + ".type=ctx"); - constraints.insert( - register_name + ".ctx_offset=" + std::to_string(reg - reinterpret_cast(ubpf_context))); - break; - - case address_type_t::Stack: - constraints.insert(register_name + ".type=stack"); - constraints.insert(register_name + ".stack_offset=" + std::to_string(reg - ubpf_context->stack_start)); - break; - - case address_type_t::Unknown: - constraints.insert("r" + std::to_string(i) + ".uvalue=" + std::to_string(registers[i])); - constraints.insert( - "r" + std::to_string(i) + ".svalue=" + std::to_string(static_cast(registers[i]))); - break; - case address_type_t::Map: - constraints.insert(register_name + ".type=shared"); - break; - } - } - - // Call ebpf_check_constraints_at_label with the set of string constraints at this label. - - std::ostringstream os; - - if (!ebpf_check_constraints_at_label(os, label, constraints)) { - std::cerr << "Label: " << label << std::endl; - std::cerr << os.str() << std::endl; - throw std::runtime_error("ebpf_check_constraints_at_label failed"); - } - } + // if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK")) { + // ubpf_context_t* ubpf_context = reinterpret_cast(context); + // UNREFERENCED_PARAMETER(stack_start); + // UNREFERENCED_PARAMETER(stack_length); + // UNREFERENCED_PARAMETER(stack_mask); + + // // Check if this is an local call or exit instruction. + // const ebpf_inst* inst = reinterpret_cast(ubpf_context->program_start); + // inst += program_counter; + + // std::string label; + + // for (size_t i = 0; i < g_pc_stack.size(); i++) { + // label += std::to_string(g_pc_stack[i]) + "/"; + // } + + // label += std::to_string(program_counter) + ":-1"; + + // // Local call. + // if (inst->opcode == EBPF_OP_CALL && inst->src == 1) { + // g_pc_stack.push_back(program_counter); + // } + + // // Exit. + // if (inst->opcode == EBPF_OP_EXIT) { + // if (!g_pc_stack.empty()) { + // g_pc_stack.pop_back(); + // } + // } + + + // if (program_counter == 0) { + // return; + // } + + // // Build set of string constraints from the register values. + // std::set constraints; + // constraints.insert("packet_size=" + std::to_string(ubpf_context->original_data_end - ubpf_context->original_data)); + // for (int i = 0; i < 10; i++) { + // if ((register_mask & (1 << i)) == 0) { + // continue; + // } + // uint64_t reg = registers[i]; + // std::string register_name = "r" + std::to_string(i); + + // // Given the register value, classify it as packet, context, stack, or unknown and add the appropriate + // // constraint. + // address_type_t type = ubpf_classify_address(ubpf_context, reg); + // switch (type) { + // case address_type_t::Packet: + // constraints.insert(register_name + ".type=packet"); + // constraints.insert(register_name + ".packet_offset=" + std::to_string(reg - ubpf_context->data)); + // constraints.insert( + // register_name + ".packet_size=" + std::to_string(ubpf_context->data_end - ubpf_context->data)); + // break; + + // case address_type_t::Context: + // constraints.insert(register_name + ".type=ctx"); + // constraints.insert( + // register_name + ".ctx_offset=" + std::to_string(reg - reinterpret_cast(ubpf_context))); + // break; + + // case address_type_t::Stack: + // constraints.insert(register_name + ".type=stack"); + // constraints.insert(register_name + ".stack_offset=" + std::to_string(reg - ubpf_context->stack_start)); + // break; + + // case address_type_t::Unknown: + // constraints.insert("r" + std::to_string(i) + ".uvalue=" + std::to_string(registers[i])); + // constraints.insert( + // "r" + std::to_string(i) + ".svalue=" + std::to_string(static_cast(registers[i]))); + // break; + // case address_type_t::Map: + // constraints.insert(register_name + ".type=shared"); + // break; + // } + // } + + // // Call ebpf_check_constraints_at_label with the set of string constraints at this label. + + // std::ostringstream os; + + // if (!ebpf_check_constraints_at_label(os, label, constraints)) { + // std::cerr << "Label: " << label << std::endl; + // std::cerr << os.str() << std::endl; + // throw std::runtime_error("ebpf_check_constraints_at_label failed"); + // } + // } } /** From cf8254a6b78f183444321e9e30bc44730ed5f773 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Thu, 16 Jan 2025 09:11:19 -0800 Subject: [PATCH 2/4] Re-implement UBPF_FUZZER_CONSTRAINT_CHECK Signed-off-by: Alan Jowett --- external/ebpf-verifier | 2 +- libfuzzer/libfuzz_harness.cc | 195 ++++++++++++++++++----------------- 2 files changed, 104 insertions(+), 93 deletions(-) diff --git a/external/ebpf-verifier b/external/ebpf-verifier index c752a2efd..7cbf769f2 160000 --- a/external/ebpf-verifier +++ b/external/ebpf-verifier @@ -1 +1 @@ -Subproject commit c752a2efd89a782f3226642c151c6b0e6b514272 +Subproject commit 7cbf769f237475c0491cc56fd0c8ffb3b0ce7a55 diff --git a/libfuzzer/libfuzz_harness.cc b/libfuzzer/libfuzz_harness.cc index 5841a64a0..b117d961f 100644 --- a/libfuzzer/libfuzz_harness.cc +++ b/libfuzzer/libfuzz_harness.cc @@ -116,6 +116,8 @@ EbpfProgramType g_ubpf_program_type = { .is_privileged = false, }; +std::optional stored_invariants; + /** * @brief This function is called by the verifier when parsing an ELF file to determine the type of the program being * loaded based on the section and path. @@ -371,15 +373,15 @@ try { auto program = Program::from_sequence(prog, info, options.cfg_opts); // Verify the program. This will return false or throw an exception if the program is invalid. - auto invariants = analyze(program); + stored_invariants.emplace(analyze(program)); - bool result = invariants.verified(program); + bool result = stored_invariants->verified(program); if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT")) { - auto report = invariants.check_assertions(program); + auto report = stored_invariants->check_assertions(program); print_warnings(error_stream, report); - print_invariants(error_stream, program, false, invariants); + print_invariants(error_stream, program, false, *stored_invariants); std::cout << "verifier stats:" << std::endl; std::cout << "total_warnings: " << stats.total_warnings << std::endl; @@ -534,95 +536,104 @@ ubpf_debug_function( std::cout << std::endl; } + if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK")) { + ubpf_context_t* ubpf_context = reinterpret_cast(context); + UNREFERENCED_PARAMETER(stack_start); + UNREFERENCED_PARAMETER(stack_length); + UNREFERENCED_PARAMETER(stack_mask); + + // Check if this is an local call or exit instruction. + const ebpf_inst* inst = reinterpret_cast(ubpf_context->program_start); + inst += program_counter; + + std::string stack_frame_prefix; + + for (size_t i = 1; i < g_pc_stack.size(); i++) { + stack_frame_prefix += std::to_string(g_pc_stack[i]) + "/"; + } + + crab::label_t label{program_counter, -1, stack_frame_prefix}; + + // Local call. + if (inst->opcode == EBPF_OP_CALL && inst->src == 1) { + g_pc_stack.push_back(program_counter); + } + + // Exit. + if (inst->opcode == EBPF_OP_EXIT) { + if (!g_pc_stack.empty()) { + g_pc_stack.pop_back(); + } + } + + + if (program_counter == 0) { + return; + } - // if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK")) { - // ubpf_context_t* ubpf_context = reinterpret_cast(context); - // UNREFERENCED_PARAMETER(stack_start); - // UNREFERENCED_PARAMETER(stack_length); - // UNREFERENCED_PARAMETER(stack_mask); - - // // Check if this is an local call or exit instruction. - // const ebpf_inst* inst = reinterpret_cast(ubpf_context->program_start); - // inst += program_counter; - - // std::string label; - - // for (size_t i = 0; i < g_pc_stack.size(); i++) { - // label += std::to_string(g_pc_stack[i]) + "/"; - // } - - // label += std::to_string(program_counter) + ":-1"; - - // // Local call. - // if (inst->opcode == EBPF_OP_CALL && inst->src == 1) { - // g_pc_stack.push_back(program_counter); - // } - - // // Exit. - // if (inst->opcode == EBPF_OP_EXIT) { - // if (!g_pc_stack.empty()) { - // g_pc_stack.pop_back(); - // } - // } - - - // if (program_counter == 0) { - // return; - // } - - // // Build set of string constraints from the register values. - // std::set constraints; - // constraints.insert("packet_size=" + std::to_string(ubpf_context->original_data_end - ubpf_context->original_data)); - // for (int i = 0; i < 10; i++) { - // if ((register_mask & (1 << i)) == 0) { - // continue; - // } - // uint64_t reg = registers[i]; - // std::string register_name = "r" + std::to_string(i); - - // // Given the register value, classify it as packet, context, stack, or unknown and add the appropriate - // // constraint. - // address_type_t type = ubpf_classify_address(ubpf_context, reg); - // switch (type) { - // case address_type_t::Packet: - // constraints.insert(register_name + ".type=packet"); - // constraints.insert(register_name + ".packet_offset=" + std::to_string(reg - ubpf_context->data)); - // constraints.insert( - // register_name + ".packet_size=" + std::to_string(ubpf_context->data_end - ubpf_context->data)); - // break; - - // case address_type_t::Context: - // constraints.insert(register_name + ".type=ctx"); - // constraints.insert( - // register_name + ".ctx_offset=" + std::to_string(reg - reinterpret_cast(ubpf_context))); - // break; - - // case address_type_t::Stack: - // constraints.insert(register_name + ".type=stack"); - // constraints.insert(register_name + ".stack_offset=" + std::to_string(reg - ubpf_context->stack_start)); - // break; - - // case address_type_t::Unknown: - // constraints.insert("r" + std::to_string(i) + ".uvalue=" + std::to_string(registers[i])); - // constraints.insert( - // "r" + std::to_string(i) + ".svalue=" + std::to_string(static_cast(registers[i]))); - // break; - // case address_type_t::Map: - // constraints.insert(register_name + ".type=shared"); - // break; - // } - // } - - // // Call ebpf_check_constraints_at_label with the set of string constraints at this label. - - // std::ostringstream os; - - // if (!ebpf_check_constraints_at_label(os, label, constraints)) { - // std::cerr << "Label: " << label << std::endl; - // std::cerr << os.str() << std::endl; - // throw std::runtime_error("ebpf_check_constraints_at_label failed"); - // } - // } + // Build set of string constraints from the register values. + std::set constraints; + constraints.insert("packet_size=" + std::to_string(ubpf_context->original_data_end - ubpf_context->original_data)); + for (int i = 0; i < 10; i++) { + if ((register_mask & (1 << i)) == 0) { + continue; + } + uint64_t reg = registers[i]; + std::string register_name = "r" + std::to_string(i); + + // Given the register value, classify it as packet, context, stack, or unknown and add the appropriate + // constraint. + address_type_t type = ubpf_classify_address(ubpf_context, reg); + switch (type) { + case address_type_t::Packet: + constraints.insert(register_name + ".type=packet"); + constraints.insert(register_name + ".packet_offset=" + std::to_string(reg - ubpf_context->data)); + constraints.insert( + register_name + ".packet_size=" + std::to_string(ubpf_context->data_end - ubpf_context->data)); + break; + + case address_type_t::Context: + constraints.insert(register_name + ".type=ctx"); + constraints.insert( + register_name + ".ctx_offset=" + std::to_string(reg - reinterpret_cast(ubpf_context))); + break; + + case address_type_t::Stack: + constraints.insert(register_name + ".type=stack"); + constraints.insert(register_name + ".stack_offset=" + std::to_string(reg - ubpf_context->stack_start)); + break; + + case address_type_t::Unknown: + constraints.insert("r" + std::to_string(i) + ".uvalue=" + std::to_string(registers[i])); + constraints.insert( + "r" + std::to_string(i) + ".svalue=" + std::to_string(static_cast(registers[i]))); + break; + case address_type_t::Map: + constraints.insert(register_name + ".type=shared"); + break; + } + } + + std::ostringstream os; + string_invariant inv; + inv.maybe_inv = constraints; + + // Call the verifier to check the constraints at the given label. + if (!stored_invariants->is_valid_before(label, inv)) { + std::cerr << "Label: " << label << std::endl; + std::cerr << "Verifier state: " << std::endl; + std::cerr << stored_invariants->invariant_at(label); + std::cerr << std::endl; + + std::cerr << "Actual state: " << std::endl; + std::cerr << inv << std::endl; + + throw std::runtime_error("ebpf_check_constraints_at_label failed"); + } + + // if (!ebpf_check_constraints_at_label(os, label, constraints)) { + // } + } } /** From 7b537c9697e092e9f428184d7668c1313f86e87e Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 21 Jan 2025 13:23:15 -0800 Subject: [PATCH 3/4] Switch to updated verifier Signed-off-by: Alan Jowett --- external/ebpf-verifier | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/external/ebpf-verifier b/external/ebpf-verifier index 7cbf769f2..b3b36e1b7 160000 --- a/external/ebpf-verifier +++ b/external/ebpf-verifier @@ -1 +1 @@ -Subproject commit 7cbf769f237475c0491cc56fd0c8ffb3b0ce7a55 +Subproject commit b3b36e1b7a2be4ee203351f4555db3981af691f6 From 780b0101ef2b2a99659fd07d1d0fd0d827cac920 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 21 Jan 2025 13:51:46 -0800 Subject: [PATCH 4/4] Switch to latest ebpf-verifier Signed-off-by: Alan Jowett --- external/ebpf-verifier | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/external/ebpf-verifier b/external/ebpf-verifier index b3b36e1b7..0d2ce9ee1 160000 --- a/external/ebpf-verifier +++ b/external/ebpf-verifier @@ -1 +1 @@ -Subproject commit b3b36e1b7a2be4ee203351f4555db3981af691f6 +Subproject commit 0d2ce9ee1376db10826eb7650cb568883628d43a