18658728485

Committed 18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%

Build # 18658728485

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

95.3

/src/crab/ebpf_checker.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT

// This file is eBPF-specific, not derived from CRAB.

#include <bitset>
#include <optional>
#include <utility>

#include "arith/dsl_syntax.hpp"
#include "asm_syntax.hpp"
#include "asm_unmarshal.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/var_registry.hpp"
#include "platform.hpp"
#include "program.hpp"

namespace prevail {

static bool check_require_value(const TypeToNumDomain& inv, const LinearConstraint& cst) {
    if (inv.is_bottom()) {
        return true;
    }
    if (cst.is_contradiction()) {
        return false;
    }
    if (inv.values.entail(cst)) {
        // XXX: add_redundant(s);
        return true;
    }
    if (inv.values.intersect(cst)) {
        // XXX: add_error() if imply negation
        return false;
    }
    return false;
}
static bool check_require_type(const TypeToNumDomain& inv, const LinearConstraint& cst) {
    if (inv.is_bottom()) {
        return true;
    }
    if (cst.is_contradiction()) {
        return false;
    }
    if (inv.types.inv.entail(cst)) {
        // XXX: add_redundant(s);
        return true;
    }
    if (inv.types.inv.intersect(cst)) {
        // XXX: add_error() if imply negation
        return false;
    }
    return false;
}

struct Check {
    LinearConstraint cst;
    std::string msg;
};

using OnRequire = std::function<void(TypeToNumDomain&, const LinearConstraint&, const std::string&)>;

class EbpfChecker final {
  public:
    explicit EbpfChecker(EbpfDomain& dom, Assertion assertion, OnRequire on_require_type, OnRequire on_require_value)
        : assertion{std::move(assertion)}, on_require_type{std::move(on_require_type)},
          on_require_value{std::move(on_require_value)}, dom(dom) {}

    void visit(const Assertion& assertion) { std::visit(*this, assertion); }

    void operator()(const Addable&) const;
    void operator()(const BoundedLoopCount&) const;
    void operator()(const Comparable&) const;
    void operator()(const FuncConstraint&) const;
    void operator()(const ValidDivisor&) const;
    void operator()(const TypeConstraint&) const;
    void operator()(const ValidAccess&) const;
    void operator()(const ValidCall&) const;
    void operator()(const ValidMapKeyValue&) const;
    void operator()(const ValidSize&) const;
    void operator()(const ValidStore&) const;
    void operator()(const ZeroCtxOffset&) const;

  private:
    [[nodiscard]]
    std::string create_warning(const std::string& s) const {
        return s + " (" + to_string(assertion) + ")";
    }

    void require_value(TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {
        on_require_value(inv, cst, create_warning(msg));
    }

    void require_type(TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {
        on_require_type(inv, cst, create_warning(msg));
    }

    void require(const std::string& msg) const { require_value(dom.rcp, LinearConstraint::false_const(), msg); }

    // memory check / load / store
    static std::vector<Check> check_access_stack(const LinearExpression& lb, const LinearExpression& ub);
    static std::vector<Check> check_access_context(const LinearExpression& lb, const LinearExpression& ub);
    static std::vector<Check> check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
                                                  std::optional<Variable> packet_size);
    static std::vector<Check> check_access_shared(const LinearExpression& lb, const LinearExpression& ub,
                                                  Variable shared_region_size);

  private:
    const Assertion assertion;
    const OnRequire on_require_type;
    const OnRequire on_require_value;

    EbpfDomain& dom;
};

void ebpf_domain_assume(EbpfDomain& dom, const Assertion& assertion) {
    if (dom.is_bottom()) {
        return;
    }
    EbpfChecker{dom, assertion,
                [](TypeToNumDomain& inv, const LinearConstraint& cst, const std::string&) {
                    // avoid redundant errors
                    inv.types.add_constraint(cst);
                },
                [](TypeToNumDomain& inv, const LinearConstraint& cst, const std::string&) {
                    // avoid redundant errors
                    inv.values.add_constraint(cst);
                }}
        .visit(assertion);
}

std::vector<std::string> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion) {
    if (dom.is_bottom()) {
        return {};
    }
    EbpfDomain copy = dom;
    std::vector<std::string> warnings;
    EbpfChecker checker{copy, assertion,
                        [&warnings](const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) {
                            if (!check_require_type(inv, cst)) {
                                warnings.push_back(msg);
                            }
                        },
                        [&warnings](const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) {
                            if (!check_require_value(inv, cst)) {
                                warnings.push_back(msg);
                            }
                        }};
    checker.visit(assertion);
    return warnings;
}

[[nodiscard]]
std::vector<Check> EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) {
    using namespace dsl_syntax;
    std::vector<Check> checks;
    checks.emplace_back(reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,
                        "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
    checks.emplace_back(ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
    return checks;
}

[[nodiscard]]
std::vector<Check> EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) {
    using namespace dsl_syntax;
    std::vector<Check> checks;
    checks.emplace_back(lb >= 0, "Lower bound must be at least 0");
    checks.emplace_back(ub <= thread_local_program_info->type.context_descriptor->size,
                        std::string("Upper bound must be at most ") +
                            std::to_string(thread_local_program_info->type.context_descriptor->size));
    return checks;
}

[[nodiscard]]
std::vector<Check> EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
                                                    const std::optional<Variable> packet_size) {
    using namespace dsl_syntax;
    std::vector<Check> checks;
    checks.emplace_back(lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");
    if (packet_size) {
        checks.emplace_back(ub <= *packet_size, "Upper bound must be at most packet_size");
    } else {
        checks.emplace_back(ub <= MAX_PACKET_SIZE,
                            std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
    }
    return checks;
}

[[nodiscard]]
std::vector<Check> EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,
                                                    const Variable shared_region_size) {
    using namespace dsl_syntax;
    std::vector<Check> checks;
    checks.emplace_back(lb >= 0, "Lower bound must be at least 0");
    checks.emplace_back(ub <= shared_region_size,
                        std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));
    return checks;
}

void EbpfChecker::operator()(const Comparable& s) const {
    using namespace dsl_syntax;
    if (dom.rcp.types.same_type(s.r1, s.r2)) {
        // Same type. If both are numbers, that's okay. Otherwise:
        TypeDomain non_number_types = dom.rcp.types;
        non_number_types.add_constraint(type_is_not_number(s.r2));
        // We must check that they belong to a singleton region:
        if (!non_number_types.is_in_group(s.r1, TypeGroup::singleton_ptr) &&
            !non_number_types.is_in_group(s.r1, TypeGroup::map_fd)) {
            require("Cannot subtract pointers to non-singleton regions");
            return;
        }
        // And, to avoid wraparound errors, they must be within bounds.
        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});
        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});
    } else {
        // _Maybe_ different types, so r2 must be a number.
        // We checked in a previous assertion that r1 is a pointer or a number.
        require_type(dom.rcp, type_is_number(s.r2), "Cannot subtract pointers to different regions");
    }
}

void EbpfChecker::operator()(const Addable& s) const {
    if (!dom.rcp.types.implies(type_is_pointer(s.ptr), type_is_number(s.num))) {
        require("Only numbers can be added to pointers");
    }
}

void EbpfChecker::operator()(const ValidDivisor& s) const {
    using namespace dsl_syntax;
    if (!dom.rcp.types.implies(type_is_pointer(s.reg), type_is_number(s.reg))) {
        require("Only numbers can be used as divisors");
    }
    if (!thread_local_options.allow_division_by_zero) {
        const auto reg = reg_pack(s.reg);
        const auto v = s.is_signed ? reg.svalue : reg.uvalue;
        require_value(dom.rcp, v != 0, "Possible division by zero");
    }
}

void EbpfChecker::operator()(const ValidStore& s) const {
    if (!dom.rcp.types.implies(type_is_not_stack(s.mem), type_is_number(s.val))) {
        require("Only numbers can be stored to externally-visible regions");
    }
}

void EbpfChecker::operator()(const TypeConstraint& s) const {
    if (!dom.rcp.types.is_in_group(s.reg, s.types)) {
        require("Invalid type");
    }
}

void EbpfChecker::operator()(const BoundedLoopCount& s) const {
    // Enforces an upper bound on loop iterations by checking that the loop counter
    // does not exceed the specified limit
    using namespace dsl_syntax;
    const auto counter = variable_registry->loop_counter(to_string(s.name));
    require_value(dom.rcp, counter <= BoundedLoopCount::limit, "Loop counter is too large");
}

void EbpfChecker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (!dom.rcp.values) {
        return;
    }
    const RegPack& reg = reg_pack(s.reg);
    const auto src_interval = dom.rcp.values.eval_interval(reg.svalue);
    if (const auto sn = src_interval.singleton()) {
        if (sn->fits<int32_t>()) {
            // We can now process it as if the id was immediate.
            const int32_t imm = sn->cast_to<int32_t>();
            if (!thread_local_program_info->platform->is_helper_usable(imm)) {
                require("invalid helper function id " + std::to_string(imm));
                return;
            }
            const Call call = make_call(imm, *thread_local_program_info->platform);
            for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {
                // TODO: create explicit sub assertions elsewhere
                EbpfChecker{dom, sub_assertion, on_require_type, on_require_value}.visit(sub_assertion);
            }
            return;
        }
    }
    require("callx helper function id is not a valid singleton");
}

void EbpfChecker::operator()(const ValidSize& s) const {
    using namespace dsl_syntax;
    const auto r = reg_pack(s.reg);
    require_value(dom.rcp, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");
}

void EbpfChecker::operator()(const ValidCall& s) const {
    if (!s.stack_frame_prefix.empty()) {
        const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func);
        if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) {
            require("tail call not supported in subprogram");
        }
    }
}

void EbpfChecker::operator()(const ValidMapKeyValue& s) const {
    using namespace dsl_syntax;

    const auto fd_type = dom.get_map_type(s.map_fd_reg);

    const auto access_reg = reg_pack(s.access_reg);
    int width;
    if (s.key) {
        const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();
        if (!key_size.has_value()) {
            require("Map key size is not singleton");
            return;
        }
        width = key_size->narrow<int>();
    } else {
        const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();
        if (!value_size.has_value()) {
            require("Map value size is not singleton");
            return;
        }
        width = value_size->narrow<int>();
    }

    dom.rcp = dom.rcp.join_over_types(s.access_reg, [&](TypeToNumDomain& rcp, TypeEncoding access_reg_type) {
        if (access_reg_type == T_STACK) {
            Interval offset = rcp.values.eval_interval(access_reg.stack_offset);
            if (!dom.stack.all_num_width(offset, Interval{width})) {
                auto lb_is = offset.lb().number();
                std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";
                Interval ub = offset + Interval{width};
                auto ub_is = ub.ub().number();
                std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";
                require_value(rcp, LinearConstraint::false_const(),
                              "Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");
            } else if (thread_local_options.strict && fd_type.has_value()) {
                EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);
                if (map_type.is_array) {
                    // Get offset value.
                    Variable key_ptr = access_reg.stack_offset;
                    std::optional<Number> offset = rcp.values.eval_interval(key_ptr).singleton();
                    if (!offset.has_value()) {
                        require("Pointer must be a singleton");
                    } else if (s.key) {
                        // Look up the value pointed to by the key pointer.
                        Variable key_value =
                            variable_registry->cell_var(DataKind::svalues, offset.value(), sizeof(uint32_t));

                        if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {
                            require_value(rcp, key_value < *max_entries, "Array index overflow");
                        } else {
                            require("Max entries is not finite");
                        }
                        require_value(rcp, key_value >= 0, "Array index underflow");
                    }
                }
            }
        } else if (access_reg_type == T_PACKET) {
            Variable lb = access_reg.packet_offset;
            LinearExpression ub = lb + width;
            for (const auto& [cst, msg] : check_access_packet(lb, ub, {})) {
                require_value(rcp, cst, msg);
            }
            // Packet memory is both readable and writable.
        } else if (access_reg_type == T_SHARED) {
            Variable lb = access_reg.shared_offset;
            LinearExpression ub = lb + width;
            for (const auto& [cst, msg] : check_access_shared(lb, ub, access_reg.shared_region_size)) {
                require_value(rcp, cst, msg);
            }
            require_value(rcp, access_reg.svalue > 0, "Possible null access");
            // Shared memory is zero-initialized when created so is safe to read and write.
        } else {
            require("Only stack or packet can be used as a parameter");
        }
    });
}

static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,
                                                                        const Variable offset_var) {
    using namespace dsl_syntax;
    LinearExpression lb = offset_var + s.offset;
    LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v
                                                               : lb + reg_pack(std::get<Reg>(s.width)).svalue;
    return {lb, ub};
}

void EbpfChecker::operator()(const ValidAccess& s) const {
    using namespace dsl_syntax;

    const bool is_comparison_check = s.width == Value{Imm{0}};

    const auto reg = reg_pack(s.reg);
    // join_over_types instead of simple iteration is only needed for assume-assert
    dom.rcp = dom.rcp.join_over_types(s.reg, [&](TypeToNumDomain& rcp, TypeEncoding type) {
        switch (type) {
        case T_PACKET: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);
            const std::optional<Variable> packet_size =
                is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();
            for (const auto& [cst, msg] : check_access_packet(lb, ub, packet_size)) {
                require_value(rcp, cst, msg);
            }
            // if within bounds, it can never be null
            // Context memory is both readable and writable.
            break;
        }
        case T_STACK: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);
            for (const auto& [cst, msg] : check_access_stack(lb, ub)) {
                require_value(rcp, cst, msg);
            }
            // if within bounds, it can never be null
            if (s.access_type == AccessType::read &&
                !dom.stack.all_num_lb_ub(rcp.values.eval_interval(lb), rcp.values.eval_interval(ub))) {

                if (s.offset < 0) {
                    require("Stack content is not numeric");
                } else {
                    using namespace dsl_syntax;
                    LinearExpression w = std::holds_alternative<Imm>(s.width)
                                             ? LinearExpression{std::get<Imm>(s.width).v}
                                             : reg_pack(std::get<Reg>(s.width)).svalue;

                    require_value(rcp, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");
                }
            }
            break;
        }
        case T_CTX: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);
            for (const auto& [cst, msg] : check_access_context(lb, ub)) {
                require_value(rcp, cst, msg);
            }
            // if within bounds, it can never be null
            // The context is both readable and writable.
            break;
        }
        case T_SHARED: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);
            for (const auto& [cst, msg] : check_access_shared(lb, ub, reg.shared_region_size)) {
                require_value(rcp, cst, msg);
            }
            if (!is_comparison_check && !s.or_null) {
                require_value(rcp, reg.svalue > 0, "Possible null access");
            }
            // Shared memory is zero-initialized when created so is safe to read and write.
            break;
        }
        case T_NUM:
            if (!is_comparison_check) {
                if (s.or_null) {
                    require_value(rcp, reg.svalue == 0, "Non-null number");
                } else {
                    require("Only pointers can be dereferenced");
                }
            }
            break;
        case T_MAP:
        case T_MAP_PROGRAMS:
            if (!is_comparison_check) {
                require("FDs cannot be dereferenced directly");
            }
            break;
        default: require("Invalid type"); break;
        }
    });
}

void EbpfChecker::operator()(const ZeroCtxOffset& s) const {
    using namespace dsl_syntax;
    const auto reg = reg_pack(s.reg);
    require_value(dom.rcp, reg.ctx_offset == 0, "Nonzero context offset");
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	// This file is eBPF-specific, not derived from CRAB.
5
6	#include <bitset>
7	#include <optional>
8	#include <utility>
9
10	#include "arith/dsl_syntax.hpp"
11	#include "asm_syntax.hpp"
12	#include "asm_unmarshal.hpp"
13	#include "config.hpp"
14	#include "crab/array_domain.hpp"
15	#include "crab/ebpf_domain.hpp"
16	#include "crab/var_registry.hpp"
17	#include "platform.hpp"
18	#include "program.hpp"
19
20	namespace prevail {
21
22	static bool check_require_value(const TypeToNumDomain& inv, const LinearConstraint& cst) {	60,916✔
23	if (inv.is_bottom()) {	60,916✔
24	return true;
25	}
26	if (cst.is_contradiction()) {	60,916✔
27	return false;	132✔
28	}
29	if (inv.values.entail(cst)) {	90,978✔
30	// XXX: add_redundant(s);
31	return true;	60,474✔
32	}
33	if (inv.values.intersect(cst)) {	178✔
34	// XXX: add_error() if imply negation
35	return false;	67✔
36	}
37	return false;	22✔
38	}
39	static bool check_require_type(const TypeToNumDomain& inv, const LinearConstraint& cst) {	10✔
40	if (inv.is_bottom()) {	10✔
41	return true;
42	}
43	if (cst.is_contradiction()) {	10✔
44	return false;
45	}
46	if (inv.types.inv.entail(cst)) {	15✔
47	// XXX: add_redundant(s);
48	return true;	4✔
49	}
50	if (inv.types.inv.intersect(cst)) {	6✔
51	// XXX: add_error() if imply negation
52	return false;	2✔
53	}
54	return false;	1✔
55	}
56
57	struct Check {	32,307✔
58	LinearConstraint cst;
59	std::string msg;
60	};
61
62	using OnRequire = std::function<void(TypeToNumDomain&, const LinearConstraint&, const std::string&)>;
63
64	class EbpfChecker final {
65	public:
66	explicit EbpfChecker(EbpfDomain& dom, Assertion assertion, OnRequire on_require_type, OnRequire on_require_value)	146,486✔
67	: assertion{std::move(assertion)}, on_require_type{std::move(on_require_type)},	146,486✔
68	on_require_value{std::move(on_require_value)}, dom(dom) {}	146,486✔
69
70	void visit(const Assertion& assertion) { std::visit(*this, assertion); }	146,486✔
71
72	void operator()(const Addable&) const;
73	void operator()(const BoundedLoopCount&) const;
74	void operator()(const Comparable&) const;
75	void operator()(const FuncConstraint&) const;
76	void operator()(const ValidDivisor&) const;
77	void operator()(const TypeConstraint&) const;
78	void operator()(const ValidAccess&) const;
79	void operator()(const ValidCall&) const;
80	void operator()(const ValidMapKeyValue&) const;
81	void operator()(const ValidSize&) const;
82	void operator()(const ValidStore&) const;
83	void operator()(const ZeroCtxOffset&) const;
84
85	private:
86	[[nodiscard]]
87	std::string create_warning(const std::string& s) const {	61,000✔
88	return s + " (" + to_string(assertion) + ")";	91,500✔
89	}
90
91	void require_value(TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	60,990✔
92	on_require_value(inv, cst, create_warning(msg));	60,990✔
93	}	60,990✔
94
95	void require_type(TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	10✔
96	on_require_type(inv, cst, create_warning(msg));	10✔
97	}	10✔
98
99	void require(const std::string& msg) const { require_value(dom.rcp, LinearConstraint::false_const(), msg); }	435✔
100
101	// memory check / load / store
102	static std::vector<Check> check_access_stack(const LinearExpression& lb, const LinearExpression& ub);
103	static std::vector<Check> check_access_context(const LinearExpression& lb, const LinearExpression& ub);
104	static std::vector<Check> check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
105	std::optional<Variable> packet_size);
106	static std::vector<Check> check_access_shared(const LinearExpression& lb, const LinearExpression& ub,
107	Variable shared_region_size);
108
109	private:
110	const Assertion assertion;
111	const OnRequire on_require_type;
112	const OnRequire on_require_value;
113
114	EbpfDomain& dom;
115	};
116
117	void ebpf_domain_assume(EbpfDomain& dom, const Assertion& assertion) {	128✔
118	if (dom.is_bottom()) {	128✔
119	return;	32✔
120	}
121	EbpfChecker{dom, assertion,	160✔
122	[](TypeToNumDomain& inv, const LinearConstraint& cst, const std::string&) {	32✔
123	// avoid redundant errors
124	inv.types.add_constraint(cst);	×
125	},
126	[](TypeToNumDomain& inv, const LinearConstraint& cst, const std::string&) {	69✔
127	// avoid redundant errors
128	inv.values.add_constraint(cst);	74✔
129	}}	37✔
130	.visit(assertion);	64✔
131	}
132
133	std::vector<std::string> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion) {	146,170✔
134	if (dom.is_bottom()) {	146,170✔
135	return {};	×
136	}
137	EbpfDomain copy = dom;	146,170✔
138	std::vector<std::string> warnings;	146,170✔
139	EbpfChecker checker{copy, assertion,	73,085✔
140	[&warnings](const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) {	219,265✔
141	if (!check_require_type(inv, cst)) {	10✔
142	warnings.push_back(msg);	6✔
143	}
144	},	10✔
145	[&warnings](const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) {	249,713✔
146	if (!check_require_value(inv, cst)) {	60,916✔
147	warnings.push_back(msg);	442✔
148	}
149	}};	146,170✔
150	checker.visit(assertion);	146,170✔
151	return warnings;	146,170✔
152	}	219,255✔
153
154	[[nodiscard]]
155	std::vector<Check> EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) {	4,374✔
156	using namespace dsl_syntax;	2,187✔
157	std::vector<Check> checks;	4,374✔
158	checks.emplace_back(reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,	8,748✔
159	"Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
160	checks.emplace_back(ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");	6,561✔
161	return checks;	4,374✔
162	}	×
163
164	[[nodiscard]]
165	std::vector<Check> EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) {	3,232✔
166	using namespace dsl_syntax;	1,616✔
167	std::vector<Check> checks;	3,232✔
168	checks.emplace_back(lb >= 0, "Lower bound must be at least 0");	4,848✔
169	checks.emplace_back(ub <= thread_local_program_info->type.context_descriptor->size,	6,464✔
170	std::string("Upper bound must be at most ") +	6,464✔
171	std::to_string(thread_local_program_info->type.context_descriptor->size));	8,080✔
172	return checks;	3,232✔
173	}	×
174
175	[[nodiscard]]
176	std::vector<Check> EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,	5,088✔
177	const std::optional<Variable> packet_size) {
178	using namespace dsl_syntax;	2,544✔
179	std::vector<Check> checks;	5,088✔
180	checks.emplace_back(lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");	10,176✔
181	if (packet_size) {	5,088✔
182	checks.emplace_back(ub <= *packet_size, "Upper bound must be at most packet_size");	4,530✔
183	} else {
184	checks.emplace_back(ub <= MAX_PACKET_SIZE,	3,102✔
185	std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));	6,204✔
186	}
187	return checks;	5,088✔
188	}	×
189
190	[[nodiscard]]
191	std::vector<Check> EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,	8,844✔
192	const Variable shared_region_size) {
193	using namespace dsl_syntax;	4,422✔
194	std::vector<Check> checks;	8,844✔
195	checks.emplace_back(lb >= 0, "Lower bound must be at least 0");	13,266✔
196	checks.emplace_back(ub <= shared_region_size,	17,688✔
197	std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));	26,532✔
198	return checks;	8,844✔
199	}	×
200
201	void EbpfChecker::operator()(const Comparable& s) const {	3,720✔
202	using namespace dsl_syntax;	1,860✔
203	if (dom.rcp.types.same_type(s.r1, s.r2)) {	3,720✔
204	// Same type. If both are numbers, that's okay. Otherwise:
205	TypeDomain non_number_types = dom.rcp.types;	3,710✔
206	non_number_types.add_constraint(type_is_not_number(s.r2));	5,565✔
207	// We must check that they belong to a singleton region:
208	if (!non_number_types.is_in_group(s.r1, TypeGroup::singleton_ptr) &&	3,720✔
209	!non_number_types.is_in_group(s.r1, TypeGroup::map_fd)) {	10✔
210	require("Cannot subtract pointers to non-singleton regions");	2✔
211	return;	2✔
212	}
213	// And, to avoid wraparound errors, they must be within bounds.
214	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});	3,708✔
215	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});	3,708✔
216	} else {	3,710✔
217	// _Maybe_ different types, so r2 must be a number.
218	// We checked in a previous assertion that r1 is a pointer or a number.
219	require_type(dom.rcp, type_is_number(s.r2), "Cannot subtract pointers to different regions");	20✔
220	}
221	}
222
223	void EbpfChecker::operator()(const Addable& s) const {	2,076✔
224	if (!dom.rcp.types.implies(type_is_pointer(s.ptr), type_is_number(s.num))) {	2,076✔
225	require("Only numbers can be added to pointers");	8✔
226	}
227	}	2,076✔
228
229	void EbpfChecker::operator()(const ValidDivisor& s) const {	220✔
230	using namespace dsl_syntax;	110✔
231	if (!dom.rcp.types.implies(type_is_pointer(s.reg), type_is_number(s.reg))) {	220✔
232	require("Only numbers can be used as divisors");	24✔
233	}
234	if (!thread_local_options.allow_division_by_zero) {	220✔
235	const auto reg = reg_pack(s.reg);	64✔
236	const auto v = s.is_signed ? reg.svalue : reg.uvalue;	64✔
237	require_value(dom.rcp, v != 0, "Possible division by zero");	160✔
238	}
239	}	220✔
240
241	void EbpfChecker::operator()(const ValidStore& s) const {	476✔
242	if (!dom.rcp.types.implies(type_is_not_stack(s.mem), type_is_number(s.val))) {	476✔
243	require("Only numbers can be stored to externally-visible regions");	4✔
244	}
245	}	476✔
246
247	void EbpfChecker::operator()(const TypeConstraint& s) const {	89,756✔
248	if (!dom.rcp.types.is_in_group(s.reg, s.types)) {	89,756✔
249	require("Invalid type");	460✔
250	}
251	}	89,756✔
252
253	void EbpfChecker::operator()(const BoundedLoopCount& s) const {	32✔
254	// Enforces an upper bound on loop iterations by checking that the loop counter
255	// does not exceed the specified limit
256	using namespace dsl_syntax;	16✔
257	const auto counter = variable_registry->loop_counter(to_string(s.name));	32✔
258	require_value(dom.rcp, counter <= BoundedLoopCount::limit, "Loop counter is too large");	64✔
259	}	32✔
260
261	void EbpfChecker::operator()(const FuncConstraint& s) const {	48✔
262	// Look up the helper function id.
263	if (!dom.rcp.values) {	48✔
264	return;	46✔
265	}
266	const RegPack& reg = reg_pack(s.reg);	48✔
267	const auto src_interval = dom.rcp.values.eval_interval(reg.svalue);	48✔
268	if (const auto sn = src_interval.singleton()) {	48✔
269	if (sn->fits<int32_t>()) {	46✔
270	// We can now process it as if the id was immediate.
271	const int32_t imm = sn->cast_to<int32_t>();	46✔
272	if (!thread_local_program_info->platform->is_helper_usable(imm)) {	46✔
273	require("invalid helper function id " + std::to_string(imm));	6✔
274	return;	4✔
275	}
276	const Call call = make_call(imm, *thread_local_program_info->platform);	42✔
277	for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {	294✔
278	// TODO: create explicit sub assertions elsewhere
279	EbpfChecker{dom, sub_assertion, on_require_type, on_require_value}.visit(sub_assertion);	378✔
280	}	42✔
281	return;	42✔
282	}	42✔
283	}	47✔
284	require("callx helper function id is not a valid singleton");	3✔
285	}	48✔
286
287	void EbpfChecker::operator()(const ValidSize& s) const {	4,206✔
288	using namespace dsl_syntax;	2,103✔
289	const auto r = reg_pack(s.reg);	4,206✔
290	require_value(dom.rcp, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");	8,412✔
291	}	4,206✔
292
293	void EbpfChecker::operator()(const ValidCall& s) const {	8,186✔
294	if (!s.stack_frame_prefix.empty()) {	8,186✔
295	const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func);	2✔
296	if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) {	2✔
297	require("tail call not supported in subprogram");	4✔
298	}
299	}
300	}	8,186✔
301
302	void EbpfChecker::operator()(const ValidMapKeyValue& s) const {	2,368✔
303	using namespace dsl_syntax;	1,184✔
304
305	const auto fd_type = dom.get_map_type(s.map_fd_reg);	2,368✔
306
307	const auto access_reg = reg_pack(s.access_reg);	2,368✔
308	int width;	1,184✔
309	if (s.key) {	2,368✔
310	const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();	1,994✔
311	if (!key_size.has_value()) {	1,994✔
312	require("Map key size is not singleton");	×
313	return;	×
314	}
315	width = key_size->narrow<int>();	1,994✔
316	} else {	1,994✔
317	const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();	374✔
318	if (!value_size.has_value()) {	374✔
319	require("Map value size is not singleton");	×
320	return;	×
321	}
322	width = value_size->narrow<int>();	374✔
323	}	374✔
324
325	dom.rcp = dom.rcp.join_over_types(s.access_reg, [&](TypeToNumDomain& rcp, TypeEncoding access_reg_type) {	4,736✔
326	if (access_reg_type == T_STACK) {	2,368✔
327	Interval offset = rcp.values.eval_interval(access_reg.stack_offset);	2,326✔
328	if (!dom.stack.all_num_width(offset, Interval{width})) {	3,489✔
329	auto lb_is = offset.lb().number();	28✔
330	std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";	17✔
331	Interval ub = offset + Interval{width};	14✔
332	auto ub_is = ub.ub().number();	28✔
333	std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";	17✔
334	require_value(rcp, LinearConstraint::false_const(),	21✔
335	"Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");	42✔
336	} else if (thread_local_options.strict && fd_type.has_value()) {	2,333✔
337	EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);	4✔
338	if (map_type.is_array) {	4✔
339	// Get offset value.
340	Variable key_ptr = access_reg.stack_offset;	4✔
341	std::optional<Number> offset = rcp.values.eval_interval(key_ptr).singleton();	6✔
342	if (!offset.has_value()) {	4✔
343	require("Pointer must be a singleton");	×
344	} else if (s.key) {	4✔
345	// Look up the value pointed to by the key pointer.
346	Variable key_value =	2✔
347	variable_registry->cell_var(DataKind::svalues, offset.value(), sizeof(uint32_t));	4✔
348
349	if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {	10✔
350	require_value(rcp, key_value < *max_entries, "Array index overflow");	12✔
351	} else {
352	require("Max entries is not finite");	×
353	}	2✔
354	require_value(rcp, key_value >= 0, "Array index underflow");	14✔
355	}
356	}	4✔
357	}	4✔
358	} else if (access_reg_type == T_PACKET) {	2,368✔
359	Variable lb = access_reg.packet_offset;	8✔
360	LinearExpression ub = lb + width;	12✔
361	for (const auto& [cst, msg] : check_access_packet(lb, ub, {})) {	24✔
362	require_value(rcp, cst, msg);	16✔
363	}	8✔
364	// Packet memory is both readable and writable.
365	} else if (access_reg_type == T_SHARED) {	42✔
366	Variable lb = access_reg.shared_offset;	30✔
367	LinearExpression ub = lb + width;	45✔
368	for (const auto& [cst, msg] : check_access_shared(lb, ub, access_reg.shared_region_size)) {	90✔
369	require_value(rcp, cst, msg);	60✔
370	}	30✔
371	require_value(rcp, access_reg.svalue > 0, "Possible null access");	90✔
372	// Shared memory is zero-initialized when created so is safe to read and write.
373	} else {	30✔
374	require("Only stack or packet can be used as a parameter");	10✔
375	}
376	});	4,736✔
377	}
378
379	static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,	21,500✔
380	const Variable offset_var) {
381	using namespace dsl_syntax;	10,750✔
382	LinearExpression lb = offset_var + s.offset;	32,250✔
383	LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v	30,259✔
384	: lb + reg_pack(std::get<Reg>(s.width)).svalue;	30,259✔
385	return {lb, ub};	43,000✔
386	}	21,500✔
387
388	void EbpfChecker::operator()(const ValidAccess& s) const {	37,578✔
389	using namespace dsl_syntax;	18,789✔
390
391	const bool is_comparison_check = s.width == Value{Imm{0}};	37,578✔
392
393	const auto reg = reg_pack(s.reg);	37,578✔
394	// join_over_types instead of simple iteration is only needed for assume-assert
395	dom.rcp = dom.rcp.join_over_types(s.reg, [&](TypeToNumDomain& rcp, TypeEncoding type) {	75,156✔
396	switch (type) {	37,598✔
397	case T_PACKET: {	5,080✔
398	auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);	5,080✔
399	const std::optional<Variable> packet_size =	2,540✔
400	is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();	5,080✔
401	for (const auto& [cst, msg] : check_access_packet(lb, ub, packet_size)) {	15,240✔
402	require_value(rcp, cst, msg);	10,160✔
403	}	5,080✔
404	// if within bounds, it can never be null
405	// Context memory is both readable and writable.
406	break;	5,080✔
407	}	5,080✔
408	case T_STACK: {	4,374✔
409	auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);	4,374✔
410	for (const auto& [cst, msg] : check_access_stack(lb, ub)) {	13,122✔
411	require_value(rcp, cst, msg);	8,748✔
412	}	4,374✔
413	// if within bounds, it can never be null
414	if (s.access_type == AccessType::read &&	7,680✔
415	!dom.stack.all_num_lb_ub(rcp.values.eval_interval(lb), rcp.values.eval_interval(ub))) {	10,986✔
416
417	if (s.offset < 0) {	40✔
418	require("Stack content is not numeric");	×
419	} else {
420	using namespace dsl_syntax;	20✔
421	LinearExpression w = std::holds_alternative<Imm>(s.width)	40✔
422	? LinearExpression{std::get<Imm>(s.width).v}	40✔
423	: reg_pack(std::get<Reg>(s.width)).svalue;	40✔
424
425	require_value(rcp, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");	100✔
426	}	40✔
427	}
428	break;	4,374✔
429	}	4,374✔
430	case T_CTX: {	3,232✔
431	auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);	3,232✔
432	for (const auto& [cst, msg] : check_access_context(lb, ub)) {	9,696✔
433	require_value(rcp, cst, msg);	6,464✔
434	}	3,232✔
435	// if within bounds, it can never be null
436	// The context is both readable and writable.
437	break;	3,232✔
438	}	3,232✔
439	case T_SHARED: {	8,814✔
440	auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);	8,814✔
441	for (const auto& [cst, msg] : check_access_shared(lb, ub, reg.shared_region_size)) {	26,442✔
442	require_value(rcp, cst, msg);	17,628✔
443	}	8,814✔
444	if (!is_comparison_check && !s.or_null) {	8,814✔
445	require_value(rcp, reg.svalue > 0, "Possible null access");	27,195✔
446	}
447	// Shared memory is zero-initialized when created so is safe to read and write.
448	break;	8,814✔
449	}	8,814✔
450	case T_NUM:	16,032✔
451	if (!is_comparison_check) {	16,032✔
452	if (s.or_null) {	226✔
453	require_value(rcp, reg.svalue == 0, "Non-null number");	672✔
454	} else {
455	require("Only pointers can be dereferenced");	5✔
456	}
457	}
458	break;	8,016✔
459	case T_MAP:	40✔
460	case T_MAP_PROGRAMS:	20✔
461	if (!is_comparison_check) {	40✔
462	require("FDs cannot be dereferenced directly");	×
463	}
464	break;	20✔
465	default: require("Invalid type"); break;	65✔
466	}
467	});	75,176✔
468	}	37,578✔
469
470	void EbpfChecker::operator()(const ZeroCtxOffset& s) const {	5,236✔
471	using namespace dsl_syntax;	2,618✔
472	const auto reg = reg_pack(s.reg);	5,236✔
473	require_value(dom.rcp, reg.ctx_offset == 0, "Nonzero context offset");	10,472✔
474	}	5,236✔
475
476	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18658728485

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous