diff --git a/ebpf-samples b/ebpf-samples index 220d4767b..1749ea702 160000 --- a/ebpf-samples +++ b/ebpf-samples @@ -1 +1 @@ -Subproject commit 220d4767b2dce2eb8a49d62c64a4c9350b860248 +Subproject commit 1749ea702f85b67e0f13b1e356711313e923c31b diff --git a/src/config.cpp b/src/config.cpp index bc984563b..00ccab43b 100644 --- a/src/config.cpp +++ b/src/config.cpp @@ -14,5 +14,4 @@ const ebpf_verifier_options_t ebpf_verifier_default_options = { .allow_division_by_zero = true, .setup_constraints = true, .big_endian = false, - .use_value_partitioning = true, }; diff --git a/src/config.hpp b/src/config.hpp index 3917937b2..b4d5eb85d 100644 --- a/src/config.hpp +++ b/src/config.hpp @@ -2,6 +2,9 @@ // SPDX-License-Identifier: MIT #pragma once +#include +#include + struct ebpf_verifier_options_t { bool check_termination; bool assume_assertions; @@ -21,7 +24,7 @@ struct ebpf_verifier_options_t { bool big_endian; bool dump_btf_types_json; - bool use_value_partitioning; + std::vector partition_keys; }; struct ebpf_verifier_stats_t { diff --git a/src/crab/ebpf_value_partition_domain.cpp b/src/crab/ebpf_value_partition_domain.cpp index ab354baca..c23394635 100644 --- a/src/crab/ebpf_value_partition_domain.cpp +++ b/src/crab/ebpf_value_partition_domain.cpp @@ -23,8 +23,6 @@ namespace crab { -static std::string partition_key = "packet_size"; - ebpf_value_partition_domain_t::ebpf_value_partition_domain_t() : partitions(1) {} ebpf_value_partition_domain_t::ebpf_value_partition_domain_t(crab::domains::NumAbsDomain inv, crab::domains::array_domain_t stack) @@ -98,23 +96,7 @@ ebpf_value_partition_domain_t ebpf_value_partition_domain_t::join(const ebpf_val // For some reason, the <= operator on is not valid for sort, so we need to use a lambda and explicitly specify the // ordering predicate. std::sort(partitions.begin(), partitions.end(), [](const auto& lhs, const auto& rhs) { - auto lhs_interval = lhs.m_inv[variable_t::make(partition_key)]; - auto rhs_interval = rhs.m_inv[variable_t::make(partition_key)]; - - if (lhs_interval.is_bottom()) { - return false; - } - if (rhs_interval.is_bottom()) { - return true; - } - - if (lhs_interval.lb() < rhs_interval.lb()) { - return true; - } else if (lhs_interval.lb() > rhs_interval.lb()) { - return false; - } else { - return lhs_interval.ub() < rhs_interval.ub(); - } + return compare_partitions(lhs, rhs) == partition_comparison_t::LESS_THAN; }); // Perform a single pass over the partitions to merge them. @@ -122,18 +104,17 @@ ebpf_value_partition_domain_t ebpf_value_partition_domain_t::join(const ebpf_val // If the packet size interval is different, we start a new partition. std::vector merged_partitions; - // First partition is always added. - auto packet_size_interval = partitions[0].m_inv[variable_t::make(partition_key)]; - merged_partitions.push_back(std::move(partitions[0])); + // Start with the first partition. + auto current_partition = 0; + merged_partitions.push_back(partitions[current_partition]); for (size_t i = 1; i < partitions.size(); i++) { - if (partitions[i].m_inv[variable_t::make(partition_key)] == packet_size_interval) { + if (compare_partitions(partitions[i], merged_partitions.back()) == partition_comparison_t::EQUAL) { // This partition has the same packet size interval as the previous one, merge them. merged_partitions.back() |= partitions[i]; } else { - // This partition has a different packet size interval, add it to the list. - packet_size_interval = partitions[i].m_inv[variable_t::make(partition_key)]; - merged_partitions.push_back(std::move(partitions[i])); + // Start a new partition. + merged_partitions.push_back(partitions[i]); } } @@ -157,7 +138,8 @@ ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& ot return join(*this, other); } -ebpf_value_partition_domain_t ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& other) const && { +ebpf_value_partition_domain_t +ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& other) const&& { return std::move(join(*this, other)); } @@ -222,9 +204,6 @@ string_invariant ebpf_value_partition_domain_t::to_set() { } void ebpf_value_partition_domain_t::initialize_loop_counter(label_t label) { - // Do we really need to merge all partitions here? - merge_all_partitions(); - for (auto& partition : partitions) { partition.initialize_loop_counter(label); } @@ -263,7 +242,7 @@ bool ebpf_value_partition_domain_t::has_same_partitions(const ebpf_value_partiti } for (size_t i = 0; i < partitions.size(); i++) { - if (partitions[i].m_inv[variable_t::make(partition_key)] != other.partitions[i].m_inv[variable_t::make(partition_key)]) { + if (compare_partitions(partitions[i], other.partitions[i]) != partition_comparison_t::EQUAL) { return false; } } @@ -288,4 +267,37 @@ void ebpf_value_partition_domain_t::merge_or_apply_to_all_partitions( } } +ebpf_value_partition_domain_t::partition_comparison_t +ebpf_value_partition_domain_t::compare_partitions(const ebpf_domain_t& lhs, const ebpf_domain_t& rhs) { + if (!partition_keys.has_value()) { + return partition_comparison_t::EQUAL; + } + // Loop over the partition key and compare each the corresponding interval in the two partitions. + for (const auto& partition_key : partition_keys.value()) { + auto lhs_interval = lhs.m_inv[variable_t::make(partition_key)]; + auto rhs_interval = rhs.m_inv[variable_t::make(partition_key)]; + + if (lhs_interval.is_bottom()) { + if (!rhs_interval.is_bottom()) { + return partition_comparison_t::LESS_THAN; + } + } else if (rhs_interval.is_bottom()) { + return partition_comparison_t::GREATER_THAN; + } else { + if (lhs_interval.lb() < rhs_interval.lb()) { + return partition_comparison_t::LESS_THAN; + } else if (lhs_interval.lb() > rhs_interval.lb()) { + return partition_comparison_t::GREATER_THAN; + } else { + if (lhs_interval.ub() < rhs_interval.ub()) { + return partition_comparison_t::LESS_THAN; + } else if (lhs_interval.ub() > rhs_interval.ub()) { + return partition_comparison_t::GREATER_THAN; + } + } + } + } + return partition_comparison_t::EQUAL; +} + } // namespace crab diff --git a/src/crab/ebpf_value_partition_domain.hpp b/src/crab/ebpf_value_partition_domain.hpp index b814f746f..e0c87871b 100644 --- a/src/crab/ebpf_value_partition_domain.hpp +++ b/src/crab/ebpf_value_partition_domain.hpp @@ -31,6 +31,9 @@ class ebpf_value_partition_domain_t { ebpf_value_partition_domain_t(ebpf_domain_t ebpf_domain); ebpf_value_partition_domain_t(std::vector&& partitions); + static void set_partition_keys(const std::vector& keys) { partition_keys = {keys}; } + static void clear_partition_keys() { partition_keys.reset(); } + // Generic abstract domain operations static ebpf_value_partition_domain_t top(); static ebpf_value_partition_domain_t bottom(); @@ -130,7 +133,24 @@ class ebpf_value_partition_domain_t { void merge_or_apply_to_all_partitions(const ebpf_value_partition_domain_t& other, std::function f) const; + + enum class partition_comparison_t { + LESS_THAN, + EQUAL, + GREATER_THAN, + }; + + /** + * @brief Compare two partitions based on the partition keys. + * + * @param[in] lhs Left-hand side of the comparison. + * @param[in] rhs Right-hand side of the comparison. + * @return partition_comparison_t The result of the comparison. + */ + static partition_comparison_t compare_partitions(const ebpf_domain_t& lhs, const ebpf_domain_t& rhs); + std::vector partitions; + inline static thread_local std::optional> partition_keys = {}; }; } // namespace crab diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 12aab40ea..44be7d57e 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -219,7 +219,8 @@ std::tuple ebpf_analyze_program_for_test(std::ostream& o const program_info& info, const ebpf_verifier_options_t& options) { - if (options.use_value_partitioning) { + if (!options.partition_keys.empty()) { + ebpf_value_partition_domain_t::set_partition_keys(options.partition_keys); return ebpf_analyze_program_for_test_variant(os, prog, entry_invariant, info, options); } else { @@ -239,7 +240,8 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro cfg_t cfg = prepare_cfg(prog, info, !options->no_simplify); checks_db report; - if (options->use_value_partitioning) { + if (!options->partition_keys.empty()) { + ebpf_value_partition_domain_t::set_partition_keys(options->partition_keys); report = get_ebpf_report(os, cfg, info, options); } else { @@ -263,4 +265,5 @@ void ebpf_verifier_clear_thread_local_state() { global_program_info.clear(); crab::domains::clear_thread_local_state(); crab::domains::SplitDBM::clear_thread_local_state(); + crab::ebpf_value_partition_domain_t::clear_partition_keys(); } diff --git a/src/ebpf_yaml.cpp b/src/ebpf_yaml.cpp index dfdf6ef3e..61d0e0429 100644 --- a/src/ebpf_yaml.cpp +++ b/src/ebpf_yaml.cpp @@ -106,6 +106,7 @@ struct RawTestCase { vector>> raw_blocks; vector post; std::set messages; + vector partition_keys; }; static vector parse_block(const YAML::Node& block_node) { @@ -139,6 +140,7 @@ static RawTestCase parse_case(const YAML::Node& case_node) { .raw_blocks = parse_code(case_node["code"]), .post = case_node["post"].as>(), .messages = as_set_empty_default(case_node["messages"]), + .partition_keys = case_node["partition_keys"].IsDefined() ? case_node["partition_keys"].as>() : vector(), }; } @@ -206,7 +208,8 @@ static TestCase read_case(const RawTestCase& raw_case) { .assumed_pre_invariant = read_invariant(raw_case.pre), .instruction_seq = raw_cfg_to_instruction_seq(raw_case.raw_blocks), .expected_post_invariant = read_invariant(raw_case.post), - .expected_messages = raw_case.messages + .expected_messages = raw_case.messages, + .partition_keys = raw_case.partition_keys, }; } @@ -247,6 +250,8 @@ std::optional run_yaml_test_case(TestCase test_case, bool debug) { test_case.options.no_simplify = true; } + test_case.options.partition_keys = test_case.partition_keys; + ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1}; EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor); diff --git a/src/ebpf_yaml.hpp b/src/ebpf_yaml.hpp index 183ea3daa..8abe3ddb5 100644 --- a/src/ebpf_yaml.hpp +++ b/src/ebpf_yaml.hpp @@ -14,6 +14,7 @@ struct TestCase { InstructionSeq instruction_seq; string_invariant expected_post_invariant; std::set expected_messages; + std::vector partition_keys; }; void foreach_suite(const std::string& path, const std::function& f); diff --git a/src/main/check.cpp b/src/main/check.cpp index 25e571293..bd0617686 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -132,6 +132,9 @@ int main(int argc, char** argv) { app.add_flag("--line-info", ebpf_verifier_options.print_line_info, "Print line information"); app.add_flag("--print-btf-types", ebpf_verifier_options.dump_btf_types_json, "Print BTF types"); + std::string partition_variable; + app.add_option("--partition-variable", partition_variable, "Partition variable")->type_name("VARIABLE"); + std::string asmfile; app.add_option("--asm", asmfile, "Print disassembly to FILE")->type_name("FILE"); std::string dotfile; @@ -144,6 +147,11 @@ int main(int argc, char** argv) { ebpf_verifier_options.print_invariants = ebpf_verifier_options.print_failures = true; ebpf_verifier_options.allow_division_by_zero = !no_division_by_zero; + if (!partition_variable.empty()) { + // partition_variable is a comma-separated list of variables. + boost::split(ebpf_verifier_options.partition_keys, partition_variable, boost::is_any_of(",")); + } + // Enable default conformance groups, which don't include callx or packet. ebpf_platform_t platform = g_ebpf_platform_linux; platform.supported_conformance_groups = bpf_conformance_groups_t::default_groups; diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp index 70af6d2ba..3c09bae2b 100644 --- a/src/test/test_verify.cpp +++ b/src/test/test_verify.cpp @@ -71,6 +71,13 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") VERIFY_SECTION(project, filename, section, nullptr, &g_ebpf_platform_linux, true); \ } +#define TEST_SECTION_WITH_PARTITION_KEY(project, filename, section, partition_key) \ + TEST_CASE("./check ebpf-samples/" project "/" filename " " section, "[verify][samples][" project "]") { \ + ebpf_verifier_options_t options = ebpf_verifier_default_options; \ + options.partition_keys.push_back(partition_key); \ + VERIFY_SECTION(project, filename, section, &options, &g_ebpf_platform_linux, true); \ + } + #define TEST_PROGRAM(project, filename, section_name, program_name) \ TEST_CASE("./check ebpf-samples/" project "/" filename " " program_name, "[verify][samples][" project "]") { \ VERIFY_PROGRAM(project, filename, section_name, program_name, nullptr, &g_ebpf_platform_linux, true); \ @@ -558,11 +565,11 @@ TEST_SECTION_FAIL("cilium", "bpf_xdp_dsr_linux.o", "2/18") TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/10") TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/18") -TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/19") -TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/21") +TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/19", "packet_size") +TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/20", "packet_size") +TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/21", "packet_size") -TEST_SECTION("cilium", "bpf_xdp_snat_linux.o", "2/19") -TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/20") +TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_snat_linux.o", "2/19", "packet_size") TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/7") TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/15") diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index da124a8bf..368194c61 100644 --- a/src/test/test_yaml.cpp +++ b/src/test/test_yaml.cpp @@ -9,7 +9,10 @@ #define YAML_CASE(path) \ TEST_CASE("YAML suite: " path, "[yaml]") { \ - foreach_suite(path, [&](const TestCase& test_case){ \ + foreach_suite(path, [&](TestCase test_case){ \ + if (test_case.partition_keys.size() == 1 && test_case.partition_keys[0] == "none") { \ + test_case.partition_keys.clear(); \ + } \ std::optional failure = run_yaml_test_case(test_case); \ if (failure) { \ std::cout << "test case: " << test_case.name << "\n"; \ @@ -19,6 +22,24 @@ }); \ } +#define YAML_CASE_WITH_PARTITION(path, partition) \ + TEST_CASE("YAML suite: " path " with partition " partition, "[yaml]") { \ + foreach_suite(path, [&](TestCase test_case){ \ + if (test_case.partition_keys.size() == 1 && test_case.partition_keys[0] == "none") { \ + /* Skip test cases that are not partitioned */ \ + return; \ + } \ + test_case.partition_keys = {partition}; \ + std::optional failure = run_yaml_test_case(test_case); \ + if (failure) { \ + std::cout << "test case: " << test_case.name << "\n"; \ + print_failure(*failure, std::cout); \ + } \ + REQUIRE(!failure); \ + }); \ + } + + YAML_CASE("test-data/add.yaml") YAML_CASE("test-data/assign.yaml") YAML_CASE("test-data/atomic.yaml") @@ -39,3 +60,24 @@ YAML_CASE("test-data/stack.yaml") YAML_CASE("test-data/subtract.yaml") YAML_CASE("test-data/unop.yaml") YAML_CASE("test-data/unsigned.yaml") + +YAML_CASE_WITH_PARTITION("test-data/add.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/assign.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/atomic.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/bitop.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/call.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/callx.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/udivmod.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/sdivmod.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/full64.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/jump.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/loop.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/movsx.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/packet.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/parse.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/sext.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/shift.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/stack.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/subtract.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/unop.yaml", "packet_size"); +YAML_CASE_WITH_PARTITION("test-data/unsigned.yaml", "packet_size"); diff --git a/test-data/jump.yaml b/test-data/jump.yaml index 8fc5fcd71..7448d173e 100644 --- a/test-data/jump.yaml +++ b/test-data/jump.yaml @@ -536,6 +536,50 @@ post: messages: - "7:9: Code is unreachable after 7:9" --- +test-case: lost implications in correlated branches - with packet_size partition + +partition_keys: ["packet_size"] + +pre: ["meta_offset=0", "packet_size=[36, 65534]", + "r1.type=packet", "r1.packet_offset=54", + "r2.type=packet", "r2.packet_offset=packet_size"] + +code: + : | + r0 = 0 + if r1 > r2 goto + r4 = 0 ; r1 is within packet + goto + : | + r4 = 1 ; r1 is past end of packet + goto + : | + if r4 == 1 goto ; skip to end if r1 is past end of packet + r0 = *(u64 *)(r1 - 8) ; this should be safe to dereference but the verifier fails it + : | + exit + +post: + - meta_offset=0 + - packet_size=[36, 65534] + - packet_size=r2.packet_offset + - packet_size-r1.packet_offset<=65480 + - r0.type=number + - r1.type=packet + - r1.packet_offset=54 + - r1.packet_offset-packet_size<=18 + - r1.packet_offset-r2.packet_offset<=18 + - r2.type=packet + - r2.packet_offset=[36, 65534] + - r2.packet_offset-r1.packet_offset<=65480 + - r4.type=number + - r4.svalue=[0, 1] + - r4.uvalue=[0, 1] + - r4.svalue=r4.uvalue + +messages: +--- +partition_keys: ["none"] test-case: lost implications in correlated branches pre: ["meta_offset=0", "packet_size=[36, 65534]", @@ -576,6 +620,7 @@ post: - r4.svalue=r4.uvalue messages: + - "7: Upper bound must be at most packet_size (valid_access(r1.offset-8, width=8) for read)" --- test-case: 32-bit compare