Skip to content

Commit

Permalink
fail hard when a non-Assume instruction turns an invariant into bottom
Browse files Browse the repository at this point in the history 
makes #679 visible.

Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg committed Nov 12, 2024
1 parent 455555b commit 2c0826e
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 18 deletions.
15 changes: 14 additions & 1 deletion src/crab/ebpf_transformer.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,20 @@ class ebpf_transformer final {
const linear_expression_t& val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);
}; // end ebpf_domain_t

void ebpf_domain_transform(ebpf_domain_t& inv, const Instruction& ins) { std::visit(ebpf_transformer{inv}, ins); }
void ebpf_domain_transform(ebpf_domain_t& inv, const Instruction& ins) {
if (inv.is_bottom()) {
return;
}
std::visit(ebpf_transformer{inv}, ins);
if (inv.is_bottom() && !std::holds_alternative<Assume>(ins)) {
// Fail. raise an exception to stop the analysis.
std::stringstream msg;
msg << "Bug! pre-invariant:\n"
<< inv.to_set() << "\n followed by instruction: " << ins << "\n"
<< "leads to bottom";
throw std::logic_error(msg.str());
}
}

/** Linear constraint for a pointer comparison.
*/
Expand Down
23 changes: 14 additions & 9 deletions src/crab_verifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -226,16 +226,21 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro
prog_opt = prog;
}

const checks_db report = get_ebpf_report(os, cfg, info, options, prog_opt);
if (options.print_failures) {
print_report(os, report, prog, options.print_line_info);
}
if (stats) {
stats->total_unreachable = report.total_unreachable;
stats->total_warnings = report.total_warnings;
stats->max_loop_count = report.get_max_loop_count();
try {
const checks_db report = get_ebpf_report(os, cfg, info, options, prog_opt);
if (options.print_failures) {
print_report(os, report, prog, options.print_line_info);
}
if (stats) {
stats->total_unreachable = report.total_unreachable;
stats->total_warnings = report.total_warnings;
stats->max_loop_count = report.get_max_loop_count();
}
return report.total_warnings == 0;
} catch (std::logic_error& e) {
std::cerr << e.what();
return false;
}
return report.total_warnings == 0;
}

void ebpf_verifier_clear_thread_local_state() {
Expand Down
24 changes: 16 additions & 8 deletions src/test/test_verify.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,8 +104,7 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text")
VERIFY_SECTION(project, filename, section, {}, &g_ebpf_platform_linux, false); \
}

#define TEST_SECTION_LEGACY(dirname, filename, sectionname) \
TEST_SECTION(dirname, filename, sectionname) \
#define TEST_LEGACY(dirname, filename, sectionname) \
TEST_CASE("Fail unmarshalling: " dirname "/" filename " " sectionname, "[unmarshal]") { \
ebpf_platform_t platform = g_ebpf_platform_linux; \
platform.supported_conformance_groups &= ~bpf_conformance_groups_t::packet; \
Expand All @@ -115,6 +114,13 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text")
std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog); \
REQUIRE(std::holds_alternative<std::string>(prog_or_error)); \
}
#define TEST_SECTION_LEGACY(dirname, filename, sectionname) \
TEST_SECTION(dirname, filename, sectionname) \
TEST_LEGACY(dirname, filename, sectionname)

#define TEST_SECTION_LEGACY_FAIL(dirname, filename, sectionname) \
TEST_SECTION_FAIL(dirname, filename, sectionname) \
TEST_LEGACY(dirname, filename, sectionname)

TEST_SECTION("bpf_cilium_test", "bpf_lxc_jit.o", "1/0xdc06")
TEST_SECTION("bpf_cilium_test", "bpf_lxc_jit.o", "2/1")
Expand Down Expand Up @@ -152,7 +158,6 @@ TEST_SECTION("bpf_cilium_test", "bpf_netdev.o", "2/3")
TEST_SECTION("bpf_cilium_test", "bpf_netdev.o", "2/4")
TEST_SECTION("bpf_cilium_test", "bpf_netdev.o", "2/5")
TEST_SECTION("bpf_cilium_test", "bpf_netdev.o", "2/7")
TEST_SECTION_LEGACY("bpf_cilium_test", "bpf_netdev.o", "from-netdev")

TEST_SECTION("bpf_cilium_test", "bpf_overlay.o", "2/1")
TEST_SECTION("bpf_cilium_test", "bpf_overlay.o", "2/2")
Expand Down Expand Up @@ -184,20 +189,15 @@ TEST_SECTION("cilium", "bpf_lxc.o", "2/3")
TEST_SECTION("cilium", "bpf_lxc.o", "2/4")
TEST_SECTION("cilium", "bpf_lxc.o", "2/5")
TEST_SECTION("cilium", "bpf_lxc.o", "2/6")
TEST_SECTION("cilium", "bpf_lxc.o", "2/7")
TEST_SECTION("cilium", "bpf_lxc.o", "2/8")
TEST_SECTION("cilium", "bpf_lxc.o", "2/9")
TEST_SECTION_LEGACY("cilium", "bpf_lxc.o", "2/10")
TEST_SECTION("cilium", "bpf_lxc.o", "2/11")
TEST_SECTION("cilium", "bpf_lxc.o", "2/12")
TEST_SECTION("cilium", "bpf_lxc.o", "from-container")

TEST_SECTION("cilium", "bpf_netdev.o", "2/1")
TEST_SECTION("cilium", "bpf_netdev.o", "2/3")
TEST_SECTION("cilium", "bpf_netdev.o", "2/4")
TEST_SECTION("cilium", "bpf_netdev.o", "2/5")
TEST_SECTION("cilium", "bpf_netdev.o", "2/7")
TEST_SECTION_LEGACY("cilium", "bpf_netdev.o", "from-netdev")

TEST_SECTION("cilium", "bpf_overlay.o", "2/1")
TEST_SECTION("cilium", "bpf_overlay.o", "2/3")
Expand Down Expand Up @@ -586,6 +586,14 @@ TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/16")
// False positive, unknown cause
TEST_SECTION_FAIL("linux", "test_map_in_map_kern.o", "kprobe/sys_connect")

// Failures due to #679: sign extension (r1 s32= r1) leading to bottom
TEST_SECTION_LEGACY_FAIL("cilium", "bpf_netdev.o", "from-netdev")
TEST_SECTION_LEGACY_FAIL("bpf_cilium_test", "bpf_netdev.o", "from-netdev")
TEST_SECTION_FAIL("cilium", "bpf_lxc.o", "2/7")
TEST_SECTION_LEGACY_FAIL("cilium", "bpf_lxc.o", "2/10")
TEST_SECTION_FAIL("cilium", "bpf_lxc.o", "2/11")
TEST_SECTION_FAIL("cilium", "bpf_lxc.o", "2/12")

void test_analyze_thread(const cfg_t* cfg, program_info* info, bool* res) {
*res = run_ebpf_analysis(std::cout, *cfg, *info, {}, nullptr);
}
Expand Down

0 comments on commit 2c0826e

Please sign in to comment.