Skip to content

Commit

Permalink
Update version of ebpf-verifier being fuzzed (#632)
Browse files Browse the repository at this point in the history 
Signed-off-by: Alan Jowett <[email protected]>
  • Loading branch information
@Alan-Jowett
Alan-Jowett authored Jan 30, 2025
1 parent 16d52a4 commit d682377
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 17 deletions.
2 changes: 1 addition & 1 deletion external/ebpf-verifier
Submodule ebpf-verifier updated 88 files
+4 −3 .github/workflows/coverage.yml
+5 −1 README.md
+1 −1 ebpf-samples
+1 −1 external/bpf_conformance
+1 −1 external/libbtf
+260 −185 src/asm_cfg.cpp
+172 −84 src/asm_files.cpp
+5 −0 src/asm_files.hpp
+13 −7 src/asm_marshal.cpp
+176 −124 src/asm_ostream.cpp
+0 −58 src/asm_ostream.hpp
+20 −23 src/asm_parse.cpp
+1 −20 src/asm_parse.hpp
+40 −163 src/asm_syntax.hpp
+22 −17 src/asm_unmarshal.cpp
+16 −15 src/assertions.cpp
+27 −19 src/config.hpp
+3 −14 src/crab/array_domain.cpp
+0 −4 src/crab/array_domain.hpp
+84 −532 src/crab/cfg.hpp
+441 −0 src/crab/ebpf_checker.cpp
+67 −2,686 src/crab/ebpf_domain.cpp
+35 −140 src/crab/ebpf_domain.hpp
+2,462 −0 src/crab/ebpf_transformer.cpp
+57 −88 src/crab/fwd_analyzer.cpp
+7 −3 src/crab/fwd_analyzer.hpp
+2 −1 src/crab/interval.hpp
+94 −0 src/crab/label.hpp
+86 −58 src/crab/split_dbm.cpp
+5 −8 src/crab/split_dbm.hpp
+9 −10 src/crab/thresholds.cpp
+1 −1 src/crab/thresholds.hpp
+1 −1 src/crab/type_domain.cpp
+2 −0 src/crab/type_domain.hpp
+1 −1 src/crab/type_encoding.hpp
+5 −4 src/crab/var_factory.cpp
+1 −0 src/crab/variable.hpp
+26 −8 src/crab/wto.cpp
+12 −4 src/crab/wto.hpp
+8 −7 src/crab_utils/debug.hpp
+96 −145 src/crab_utils/graph_ops.hpp
+7 −7 src/crab_utils/heap.hpp
+0 −5 src/crab_utils/stats.cpp
+23 −4 src/crab_utils/stats.hpp
+80 −284 src/crab_verifier.cpp
+65 −49 src/crab_verifier.hpp
+1 −1 src/ebpf_verifier.hpp
+4 −0 src/ebpf_vm_isa.hpp
+1 −1 src/linux/gpl/spec_prototypes.cpp
+20 −18 src/linux/linux_platform.cpp
+2 −0 src/linux/linux_platform.hpp
+52 −30 src/main/check.cpp
+22 −19 src/main/linux_verifier.cpp
+1 −1 src/main/run_yaml.cpp
+0 −16 src/main/utils.hpp
+73 −0 src/program.hpp
+17 −11 src/spec_type_descriptors.hpp
+1 −1 src/string_constraints.hpp
+58 −109 src/test/ebpf_yaml.cpp
+1 −2 src/test/ebpf_yaml.hpp
+1 −1 src/test/test_conformance.cpp
+17 −12 src/test/test_marshal.cpp
+0 −1 src/test/test_print.cpp
+83 −63 src/test/test_verify.cpp
+25 −61 src/test/test_wto.cpp
+2 −1 src/test/test_yaml.cpp
+6 −79 test-data/add.yaml
+35 −46 test-data/assign.yaml
+86 −86 test-data/atomic.yaml
+7 −14 test-data/call.yaml
+4 −4 test-data/calllocal.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
+26 −0 test-data/map.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
+12 −14 test-data/stack.yaml
+3 −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
49 changes: 33 additions & 16 deletions libfuzzer/libfuzz_harness.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,8 @@ EbpfProgramType g_ubpf_program_type = {
.is_privileged = false,
};

std::optional<Invariants> 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.
Expand Down Expand Up @@ -359,20 +361,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);
stored_invariants.emplace(analyze(program));

bool result = stored_invariants->verified(program);

if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_PRINT_VERIFIER_REPORT")) {
auto report = stored_invariants->check_assertions(program);
print_warnings(error_stream, report);

print_invariants(error_stream, program, false, *stored_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;
Expand Down Expand Up @@ -525,7 +536,6 @@ ubpf_debug_function(
std::cout << std::endl;
}


if (g_ubpf_fuzzer_options.get("UBPF_FUZZER_CONSTRAINT_CHECK")) {
ubpf_context_t* ubpf_context = reinterpret_cast<ubpf_context_t*>(context);
UNREFERENCED_PARAMETER(stack_start);
Expand All @@ -536,13 +546,13 @@ ubpf_debug_function(
const ebpf_inst* inst = reinterpret_cast<const ebpf_inst*>(ubpf_context->program_start);
inst += program_counter;

std::string label;
std::string stack_frame_prefix;

for (size_t i = 0; i < g_pc_stack.size(); i++) {
label += std::to_string(g_pc_stack[i]) + "/";
for (size_t i = 1; i < g_pc_stack.size(); i++) {
stack_frame_prefix += std::to_string(g_pc_stack[i]) + "/";
}

label += std::to_string(program_counter) + ":-1";
crab::label_t label{program_counter, -1, stack_frame_prefix};

// Local call.
if (inst->opcode == EBPF_OP_CALL && inst->src == 1) {
Expand All @@ -555,7 +565,7 @@ ubpf_debug_function(
g_pc_stack.pop_back();
}
}


if (program_counter == 0) {
return;
Expand Down Expand Up @@ -604,15 +614,22 @@ ubpf_debug_function(
}
}

// Call ebpf_check_constraints_at_label with the set of string constraints at this label.

std::ostringstream os;
string_invariant inv{constraints};
auto abstract_constraints = stored_invariants->invariant_at(label);

if (!ebpf_check_constraints_at_label(os, label, constraints)) {
if (!stored_invariants->is_valid_before(label, inv)) {
std::cerr << "Label: " << label << std::endl;
std::cerr << os.str() << std::endl;
std::cerr << "Verifier state: " << std::endl;
std::cerr << abstract_constraints << std::endl;
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");
}

}
}

Expand Down

0 comments on commit d682377

Please sign in to comment.