14231336081

Committed 02 Apr 2025 11:08PM UTC coverage: 87.272% (-0.9%) from 88.177%

Build # 14231336081

Build Type

push

github

Committed by

web-flow

Commit Message

Propogate ebpf_verifier_options_t to thread_local_options (#856)

Signed-off-by: Alan Jowett <alanjo@microsoft.com>

Run Details

5 of 5 new or added lines in 2 files covered. (100.0%)

58 existing lines in 19 files now uncovered.

8324 of 9538 relevant lines covered (87.27%)

4881701.3 hits per line

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

95.83

/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 "asm_syntax.hpp"
#include "asm_unmarshal.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/ebpf_domain.hpp"
#include "dsl_syntax.hpp"
#include "platform.hpp"
#include "program.hpp"
#include "string_constraints.hpp"

using crab::domains::NumAbsDomain;
namespace crab {

static bool check_require(const NumAbsDomain& inv, const linear_constraint_t& cst) {
    if (inv.is_bottom()) {
        return true;
    }
    if (cst.is_contradiction()) {
        return false;
    }
    if (inv.entail(cst)) {
        // XXX: add_redundant(s);
        return true;
    }
    if (inv.intersect(cst)) {
        // XXX: add_error() if imply negation
        return false;
    }
    return false;
}

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

class ebpf_checker final {
  public:
    explicit ebpf_checker(ebpf_domain_t& dom, const Assertion& assertion, const OnRequire& on_require)
        : assertion{assertion}, on_require{on_require}, dom(dom), m_inv(dom.m_inv), stack(dom.stack),
          type_inv(dom.type_inv) {}

    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:
    std::string create_warning(const std::string& s) const { return s + " (" + to_string(assertion) + ")"; }

    void require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& msg) const {
        on_require(inv, cst, create_warning(msg));
    }

    void require(const std::string& msg) const { require(m_inv, linear_constraint_t::false_const(), msg); }

    // memory check / load / store
    void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
    void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
    void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                             std::optional<variable_t> packet_size) const;
    void check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                             variable_t shared_region_size) const;

  public:
  private:
    const Assertion assertion;
    const OnRequire on_require;

    ebpf_domain_t& dom;
    // shorthands:
    NumAbsDomain& m_inv;
    domains::array_domain_t& stack;
    TypeDomain& type_inv;
};

void ebpf_domain_assume(ebpf_domain_t& dom, const Assertion& assertion) {
    if (dom.is_bottom()) {
        return;
    }
    ebpf_checker{dom, assertion,
                 [](NumAbsDomain& inv, const linear_constraint_t& cst, const std::string&) {
                     // avoid redundant errors
                     inv.add_constraint(cst);
                 }}
        .visit(assertion);
}

std::vector<std::string> ebpf_domain_check(const ebpf_domain_t& dom, const Assertion& assertion) {
    if (dom.is_bottom()) {
        return {};
    }
    ebpf_domain_t copy = dom;
    std::vector<std::string> warnings;
    ebpf_checker checker{copy, assertion,
                         [&warnings](const NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& msg) {
                             if (!check_require(inv, cst)) {
                                 warnings.push_back(msg);
                             }
                         }};
    checker.visit(assertion);
    return warnings;
}

static linear_constraint_t type_is_pointer(const reg_pack_t& r) {
    using namespace crab::dsl_syntax;
    return r.type >= T_CTX;
}

static linear_constraint_t type_is_number(const reg_pack_t& r) {
    using namespace crab::dsl_syntax;
    return r.type == T_NUM;
}

static linear_constraint_t type_is_number(const Reg& r) { return type_is_number(reg_pack(r)); }

static linear_constraint_t type_is_not_stack(const reg_pack_t& r) {
    using namespace crab::dsl_syntax;
    return r.type != T_STACK;
}

void ebpf_checker::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb,
                                      const linear_expression_t& ub) const {
    using namespace crab::dsl_syntax;
    const variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
    const auto interval = inv.eval_interval(r10_stack_offset);
    if (interval.is_singleton()) {
        const int64_t stack_offset = interval.singleton()->cast_to<int64_t>();
        require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE,
                "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
    }
    require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
}

void ebpf_checker::check_access_context(NumAbsDomain& inv, const linear_expression_t& lb,
                                        const linear_expression_t& ub) const {
    using namespace crab::dsl_syntax;
    require(inv, lb >= 0, "Lower bound must be at least 0");
    require(inv, 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));
}

void ebpf_checker::check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                                       const std::optional<variable_t> packet_size) const {
    using namespace crab::dsl_syntax;
    require(inv, lb >= variable_t::meta_offset(), "Lower bound must be at least meta_offset");
    if (packet_size) {
        require(inv, ub <= *packet_size, "Upper bound must be at most packet_size");
    } else {
        require(inv, ub <= MAX_PACKET_SIZE,
                std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
    }
}

void ebpf_checker::check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                                       const variable_t shared_region_size) const {
    using namespace crab::dsl_syntax;
    require(inv, lb >= 0, "Lower bound must be at least 0");
    require(inv, ub <= shared_region_size, std::string("Upper bound must be at most ") + shared_region_size.name());
}

void ebpf_checker::operator()(const Comparable& s) const {
    using namespace crab::dsl_syntax;
    if (type_inv.same_type(m_inv, s.r1, s.r2)) {
        // Same type. If both are numbers, that's okay. Otherwise:
        const auto inv = m_inv.when(reg_pack(s.r2).type != T_NUM);
        // We must check that they belong to a singleton region:
        if (!type_inv.is_in_group(inv, s.r1, TypeGroup::singleton_ptr) &&
            !type_inv.is_in_group(inv, 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(m_inv, reg_pack(s.r2).type == T_NUM, "Cannot subtract pointers to different regions");
    };
}

void ebpf_checker::operator()(const Addable& s) const {
    if (!type_inv.implies_type(m_inv, type_is_pointer(reg_pack(s.ptr)), type_is_number(s.num))) {
        require("Only numbers can be added to pointers");
    }
}

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

void ebpf_checker::operator()(const ValidStore& s) const {
    if (!type_inv.implies_type(m_inv, type_is_not_stack(reg_pack(s.mem)), type_is_number(s.val))) {
        require("Only numbers can be stored to externally-visible regions");
    }
}

void ebpf_checker::operator()(const TypeConstraint& s) const {
    if (!type_inv.is_in_group(m_inv, s.reg, s.types)) {
        require("Invalid type");
    }
}

void ebpf_checker::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 crab::dsl_syntax;
    const auto counter = variable_t::loop_counter(to_string(s.name));
    require(m_inv, counter <= s.limit, "Loop counter is too large");
}

void ebpf_checker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (!m_inv) {
        return;
    }
    const reg_pack_t& reg = reg_pack(s.reg);
    const auto src_interval = m_inv.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
                ebpf_checker{dom, sub_assertion, on_require}.visit(sub_assertion);
            }
            return;
        }
    }
    require("callx helper function id is not a valid singleton");
}

void ebpf_checker::operator()(const ValidSize& s) const {
    using namespace crab::dsl_syntax;
    const auto r = reg_pack(s.reg);
    require(m_inv, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");
}

void ebpf_checker::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");
            return;
        }
    }
}

void ebpf_checker::operator()(const ValidMapKeyValue& s) const {
    using namespace crab::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>();
    }

    m_inv = type_inv.join_over_types(m_inv, s.access_reg, [&](NumAbsDomain& inv, type_encoding_t access_reg_type) {
        if (access_reg_type == T_STACK) {
            variable_t lb = access_reg.stack_offset;
            linear_expression_t ub = lb + width;
            if (!stack.all_num(inv, lb, ub)) {
                auto lb_is = inv.eval_interval(lb).lb().number();
                std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";
                auto ub_is = inv.eval_interval(ub).ub().number();
                std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";
                require(inv, linear_constraint_t::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_t key_ptr = access_reg.stack_offset;
                    std::optional<number_t> offset = inv.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_t key_value =
                            variable_t::cell_var(data_kind_t::svalues, offset.value(), sizeof(uint32_t));

                        if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {
                            require(inv, key_value < *max_entries, "Array index overflow");
                        } else {
                            require("Max entries is not finite");
                        }
                        require(inv, key_value >= 0, "Array index underflow");
                    }
                }
            }
        } else if (access_reg_type == T_PACKET) {
            variable_t lb = access_reg.packet_offset;
            linear_expression_t ub = lb + width;
            check_access_packet(inv, lb, ub, {});
            // Packet memory is both readable and writable.
        } else if (access_reg_type == T_SHARED) {
            variable_t lb = access_reg.shared_offset;
            linear_expression_t ub = lb + width;
            check_access_shared(inv, lb, ub, access_reg.shared_region_size);
            require(inv, 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<linear_expression_t, linear_expression_t> lb_ub_access_pair(const ValidAccess& s,
                                                                              const variable_t offset_var) {
    using namespace crab::dsl_syntax;
    linear_expression_t lb = offset_var + s.offset;
    linear_expression_t 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 ebpf_checker::operator()(const ValidAccess& s) const {
    using namespace crab::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
    m_inv = type_inv.join_over_types(m_inv, s.reg, [&](NumAbsDomain& inv, type_encoding_t type) {
        switch (type) {
        case T_PACKET: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);
            check_access_packet(inv, lb, ub,
                                is_comparison_check ? std::optional<variable_t>{} : variable_t::packet_size());
            // 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);
            check_access_stack(inv, lb, ub);
            // if within bounds, it can never be null
            if (s.access_type == AccessType::read) {
                // Require that the stack range contains numbers.
                if (!stack.all_num(inv, lb, ub)) {
                    if (s.offset < 0) {
                        require("Stack content is not numeric");
                    } else if (const auto pimm = std::get_if<Imm>(&s.width)) {
                        if (!inv.entail(gsl::narrow<int>(pimm->v) <= reg.stack_numeric_size - s.offset)) {
                            require("Stack content is not numeric");
                        }
                    } else {
                        if (!inv.entail(reg_pack(std::get<Reg>(s.width)).svalue <= reg.stack_numeric_size - s.offset)) {
                            require("Stack content is not numeric");
                        }
                    }
                }
            }
            break;
        }
        case T_CTX: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);
            check_access_context(inv, lb, ub);
            // 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);
            check_access_shared(inv, lb, ub, reg.shared_region_size);
            if (!is_comparison_check && !s.or_null) {
                require(inv, 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(inv, 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 ebpf_checker::operator()(const ZeroCtxOffset& s) const {
    using namespace crab::dsl_syntax;
    const auto reg = reg_pack(s.reg);
    require(m_inv, reg.ctx_offset == 0, "Nonzero context offset");
}

} // namespace crab

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

vbpf / ebpf-verifier / 14231336081

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