15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

96.27

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

namespace prevail {

static bool check_require(const NumAbsDomain& inv, const LinearConstraint& 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 LinearConstraint&, const std::string&)>;

class EbpfChecker final {
  public:
    explicit EbpfChecker(EbpfDomain& 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 LinearConstraint& cst, const std::string& msg) const {
        on_require(inv, cst, create_warning(msg));
    }

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

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

  private:
    const Assertion assertion;
    const OnRequire on_require;

    EbpfDomain& dom;
    // shorthands:
    NumAbsDomain& m_inv;
    ArrayDomain& stack;
    TypeDomain& type_inv;
};

void ebpf_domain_assume(EbpfDomain& dom, const Assertion& assertion) {
    if (dom.is_bottom()) {
        return;
    }
    EbpfChecker{dom, assertion,
                [](NumAbsDomain& inv, const LinearConstraint& cst, const std::string&) {
                    // avoid redundant errors
                    inv.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 NumAbsDomain& inv, const LinearConstraint& cst, const std::string& msg) {
                            if (!check_require(inv, cst)) {
                                warnings.push_back(msg);
                            }
                        }};
    checker.visit(assertion);
    return warnings;
}

static LinearConstraint type_is_pointer(const RegPack& r) {
    using namespace dsl_syntax;
    return r.type >= T_CTX;
}

static LinearConstraint type_is_number(const RegPack& r) {
    using namespace dsl_syntax;
    return r.type == T_NUM;
}

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

static LinearConstraint type_is_not_stack(const RegPack& r) {
    using namespace dsl_syntax;
    return r.type != T_STACK;
}

void EbpfChecker::check_access_stack(NumAbsDomain& inv, const LinearExpression& lb, const LinearExpression& ub) const {
    using namespace dsl_syntax;
    const Variable 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 EbpfChecker::check_access_context(NumAbsDomain& inv, const LinearExpression& lb,
                                       const LinearExpression& ub) const {
    using namespace 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 EbpfChecker::check_access_packet(NumAbsDomain& inv, const LinearExpression& lb, const LinearExpression& ub,
                                      const std::optional<Variable> packet_size) const {
    using namespace dsl_syntax;
    require(inv, lb >= Variable::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 EbpfChecker::check_access_shared(NumAbsDomain& inv, const LinearExpression& lb, const LinearExpression& ub,
                                      const Variable shared_region_size) const {
    using namespace 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 EbpfChecker::operator()(const Comparable& s) const {
    using namespace 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 EbpfChecker::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 EbpfChecker::operator()(const ValidDivisor& s) const {
    using namespace 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 EbpfChecker::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 EbpfChecker::operator()(const TypeConstraint& s) const {
    if (!type_inv.is_in_group(m_inv, 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::loop_counter(to_string(s.name));
    require(m_inv, counter <= s.limit, "Loop counter is too large");
}

void EbpfChecker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (!m_inv) {
        return;
    }
    const RegPack& 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
                EbpfChecker{dom, sub_assertion, on_require}.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(m_inv, 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>();
    }

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

Alan-Jowett / ebpf-verifier / 15194704016

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