22235569093

Committed 20 Feb 2026 02:12AM UTC coverage: 88.002% (-0.2%) from 88.157%

Build # 22235569093

Build Type

push

github

Committed by

web-flow

Commit Message

Handle Call builtins: fix handling of Falco tests  (#1025)

* falco: fix raw_tracepoint privilege and group expected failures

Mark raw_tracepoint/raw_tracepoint_writable as privileged program types so Falco raw-tracepoint sections are not treated as unprivileged argument checks.

Update Falco sample matrix to move now-passing sections out of TEST_SECTION_FAIL and group the remaining expected failures by root-cause class (offset lower-bound loss vs size lower-bound loss at correlated joins).

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

* elf/unmarshal: gate builtin relocations via platform call model

Add platform hooks to resolve builtin symbols and provide builtin call contracts, thread relocation-gated builtin call offsets through ProgramInfo, and only treat static helper IDs as builtins at gated call sites.

Also extend platform-table, marshal, and YAML-platform tests to cover builtin resolver wiring and call unmarshal behavior.
* crab: canonicalize unsigned intervals in bitwise_and
When uvalue intervals temporarily carry signed lower bounds (e.g. after joins), Interval::bitwise_and asserted in debug builds. Canonicalize both operands via zero_extend(64) before unsigned bitwise reasoning, preserving soundness and avoiding debug aborts.

Validated by reproducing SIGABRT on reverted code in [falco][verify] and confirming the patched build completes with expected 73 pass / 20 failed-as-expected.

* Fix unsound bitwise_and case for non-singleton all-ones rhs

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

Run Details

239 of 252 new or added lines in 9 files covered. (94.84%)

602 existing lines in 16 files now uncovered.

11743 of 13344 relevant lines covered (88.0%)

3262592.78 hits per line

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

91.53

/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 <variant>

#include "arith/dsl_syntax.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/var_registry.hpp"
#include "ir/program.hpp"
#include "ir/syntax.hpp"
#include "ir/unmarshal.hpp"
#include "platform.hpp"

namespace prevail {

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

    void visit() { 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 ValidCallbackTarget&) const;
    void operator()(const ValidMapKeyValue&) const;
    void operator()(const ValidSize&) const;
    void operator()(const ValidStore&) const;
    void operator()(const ZeroCtxOffset&) const;

  private:
    void require_value(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {
        if (!inv.values.entail(cst)) {
            throw_fail(msg);
        }
    }

    [[noreturn]]
    void throw_fail(const std::string& msg) const {
        throw VerificationError(msg + " (" + to_string(assertion) + ")");
    }

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

  private:
    const Assertion assertion;

    const EbpfDomain& dom;
};

std::optional<VerificationError> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion,
                                                   const Label& where) {
    if (dom.is_bottom()) {
        return {};
    }
    try {
        EbpfChecker{dom, assertion}.visit();
    } catch (VerificationError& error) {
        error.where = where;
        return {error};
    }
    return {};
}

void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {
    using namespace dsl_syntax;
    require_value(dom.state, 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");
    require_value(dom.state, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
}

void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.state, 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(const LinearExpression& lb, const LinearExpression& ub,
                                      const std::optional<Variable> packet_size) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");
    if (packet_size) {
        require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");
    } else {
        require_value(dom.state, ub <= MAX_PACKET_SIZE,
                      std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
    }
}

void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,
                                      const Variable shared_region_size) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.state, ub <= shared_region_size,
                  std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));
}

void EbpfChecker::operator()(const Comparable& s) const {
    using namespace dsl_syntax;
    if (dom.state.same_type(s.r1, s.r2)) {
        // Same type. If both are numbers, that's okay. Otherwise:
        TypeDomain non_number_types = dom.state.types;
        non_number_types.remove_type(reg_type(s.r2), T_NUM);
        // We must check that they belong to a singleton region:
        if (!non_number_types.is_in_group(s.r1, TS_SINGLETON_PTR) && !non_number_types.is_in_group(s.r1, TS_MAP)) {
            throw_fail("Cannot subtract pointers to non-singleton regions");
        }
        // 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.
        if (!dom.state.entail_type(reg_type(s.r2), T_NUM)) {
            throw_fail("Cannot subtract pointers to different regions");
        }
    }
}

void EbpfChecker::operator()(const Addable& s) const {
    if (!dom.state.implies_superset(s.ptr, TS_POINTER, s.num, TS_NUM)) {
        throw_fail("Only numbers can be added to pointers");
    }
}

void EbpfChecker::operator()(const ValidDivisor& s) const {
    using namespace dsl_syntax;
    if (!dom.state.implies_superset(s.reg, TS_POINTER, s.reg, TS_NUM)) {
        throw_fail("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.state, v != 0, "Possible division by zero");
    }
}

void EbpfChecker::operator()(const ValidStore& s) const {
    if (!dom.state.implies_not_type(s.mem, T_STACK, s.val, TS_NUM)) {
        throw_fail("Only numbers can be stored to externally-visible regions");
    }
}

void EbpfChecker::operator()(const TypeConstraint& s) const {
    if (!dom.state.is_in_group(s.reg, to_typeset(s.types))) {
        throw_fail("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.state, counter <= BoundedLoopCount::limit, "Loop counter is too large");
}

void EbpfChecker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (dom.state.is_bottom()) {
        return;
    }
    const auto src_interval = dom.state.values.eval_interval(reg_pack(s.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)) {
                throw_fail("invalid helper function id " + std::to_string(imm));
            }
            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}.visit();
            }
            return;
        }
    }
    throw_fail("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.state, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");
}

void EbpfChecker::operator()(const ValidCallbackTarget& s) const {
    const auto callback_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);
    const auto callback_target = callback_interval.singleton();
    if (!callback_target.has_value() || !callback_target->fits<int32_t>()) {
        throw_fail("callback function pointer must be a singleton code address");
    }

    const int32_t callback_label = callback_target->cast_to<int32_t>();
    if (!thread_local_program_info->callback_target_labels.contains(callback_label)) {
        throw_fail("callback function pointer does not reference a valid callback entry");
    }
    if (!thread_local_program_info->callback_targets_with_exit.contains(callback_label)) {
        throw_fail("callback function does not have a reachable exit");
    }
}

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()) {
            throw_fail("Map key size is not singleton");
        }
        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()) {
            throw_fail("Map value size is not singleton");
        }
        width = value_size->narrow<int>();
    }

    for (const auto access_reg_type : dom.state.enumerate_types(s.access_reg)) {
        if (access_reg_type == T_STACK) {
            Interval offset = dom.state.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(dom.state, 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_num = dom.state.values.eval_interval(key_ptr).singleton();
                    if (!offset_num.has_value()) {
                        throw_fail("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_num.value(), sizeof(uint32_t));

                        if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {
                            require_value(dom.state, key_value < *max_entries, "Array index overflow");
                        } else {
                            throw_fail("Max entries is not finite");
                        }
                        require_value(dom.state, 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(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(lb, ub, access_reg.shared_region_size);
            require_value(dom.state, access_reg.svalue > 0, "Possible null access");
            // Shared memory is zero-initialized when created so is safe to read and write.
        } else {
            throw_fail("Only stack, packet, or shared 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);
    for (const auto type : dom.state.enumerate_types(s.reg)) {
        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();
            check_access_packet(lb, ub, 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(lb, ub);
            // if within bounds, it can never be null
            if (s.access_type == AccessType::read &&
                !dom.stack.all_num_lb_ub(dom.state.values.eval_interval(lb), dom.state.values.eval_interval(ub))) {

                if (s.offset < 0) {
                    throw_fail("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(dom.state, 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);
            check_access_context(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(lb, ub, reg.shared_region_size);
            if (!is_comparison_check && !s.or_null) {
                require_value(dom.state, 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(dom.state, reg.svalue == 0, "Non-null number");
                } else {
                    throw_fail("Only pointers can be dereferenced");
                }
            }
            break;
        case T_MAP:
        case T_MAP_PROGRAMS:
            if (!is_comparison_check) {
                throw_fail("FDs cannot be dereferenced directly");
            }
            break;
        case T_SOCKET:
        case T_BTF_ID:
            // TODO: implement proper access checks for these pointer types.
            if (!is_comparison_check) {
                throw_fail("Unsupported pointer type for memory access");
            }
            break;
        case T_ALLOC_MEM: {
            // Treat like shared: offset-bounded access with null check.
            auto [lb, ub] = lb_ub_access_pair(s, reg.alloc_mem_offset);
            check_access_shared(lb, ub, reg.alloc_mem_size);
            if (!is_comparison_check && !s.or_null) {
                require_value(dom.state, reg.svalue > 0, "Possible null access");
            }
            break;
        }
        case T_FUNC:
            if (!is_comparison_check) {
                throw_fail("Function pointers cannot be dereferenced");
            }
            break;
        default: throw_fail("Invalid type");
        }
    }
}

void EbpfChecker::operator()(const ZeroCtxOffset& s) const {
    using namespace dsl_syntax;
    const auto reg = reg_pack(s.reg);
    // The domain is not expressive enough to handle join of null and non-null ctx,
    // Since non-null ctx pointers are nonzero numbers.
    if (s.or_null && dom.state.is_in_group(s.reg, TS_NUM) && dom.state.values.entail(reg.uvalue == 0)) {
        return;
    }
    require_value(dom.state, 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	#include <variant>
10
11	#include "arith/dsl_syntax.hpp"
12	#include "config.hpp"
13	#include "crab/array_domain.hpp"
14	#include "crab/ebpf_domain.hpp"
15	#include "crab/var_registry.hpp"
16	#include "ir/program.hpp"
17	#include "ir/syntax.hpp"
18	#include "ir/unmarshal.hpp"
19	#include "platform.hpp"
20
21	namespace prevail {
22
23	class EbpfChecker final {	415✔
24	public:
25	explicit EbpfChecker(const EbpfDomain& dom, Assertion assertion) : assertion{std::move(assertion)}, dom(dom) {}	657,126✔
26
27	void visit() { std::visit(*this, assertion); }	438,084✔
28
29	void operator()(const Addable&) const;
30	void operator()(const BoundedLoopCount&) const;
31	void operator()(const Comparable&) const;
32	void operator()(const FuncConstraint&) const;
33	void operator()(const ValidDivisor&) const;
34	void operator()(const TypeConstraint&) const;
35	void operator()(const ValidAccess&) const;
36	void operator()(const ValidCallbackTarget&) const;
37	void operator()(const ValidMapKeyValue&) const;
38	void operator()(const ValidSize&) const;
39	void operator()(const ValidStore&) const;
40	void operator()(const ZeroCtxOffset&) const;
41
42	private:
43	void require_value(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	259,742✔
44	if (!inv.values.entail(cst)) {	389,613✔
45	throw_fail(msg);	566✔
46	}
47	}	259,176✔
48
49	[[noreturn]]
50	void throw_fail(const std::string& msg) const {	810✔
51	throw VerificationError(msg + " (" + to_string(assertion) + ")");	1,215✔
52	}
53
54	// memory check / load / store
55	void check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const;
56	void check_access_context(const LinearExpression& lb, const LinearExpression& ub) const;
57	void check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
58	std::optional<Variable> packet_size) const;
59	void check_access_shared(const LinearExpression& lb, const LinearExpression& ub, Variable shared_region_size) const;
60
61	private:
62	const Assertion assertion;
63
64	const EbpfDomain& dom;
65	};
66
67	std::optional<VerificationError> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion,	572,874✔
68	const Label& where) {
69	if (dom.is_bottom()) {	572,874✔
70	return {};	134,986✔
71	}
72	try {	218,944✔
73	EbpfChecker{dom, assertion}.visit();	658,452✔
74	} catch (VerificationError& error) {	810✔
75	error.where = where;	810✔
76	return {error};	810✔
77	}	810✔
78	return {};	437,078✔
79	}
80
81	void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {	9,408✔
82	using namespace dsl_syntax;	4,704✔
83	require_value(dom.state, reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,	23,526✔
84	"Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
85	require_value(dom.state, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");	14,117✔
86	}	9,402✔
87
88	void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {	8,655✔
89	using namespace dsl_syntax;	2,885✔
90	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	8,655✔
91	require_value(dom.state, ub <= thread_local_program_info->type.context_descriptor->size,	11,543✔
92	std::string("Upper bound must be at most ") +	11,543✔
93	std::to_string(thread_local_program_info->type.context_descriptor->size));	8,656✔
94	}	5,768✔
95
96	void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,	8,532✔
97	const std::optional<Variable> packet_size) const {
98	using namespace dsl_syntax;	4,266✔
99	require_value(dom.state, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");	17,068✔
100	if (packet_size) {	8,530✔
101	require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");	9,125✔
102	} else {
103	require_value(dom.state, ub <= MAX_PACKET_SIZE,	6,246✔
104	std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));	12,492✔
105	}
106	}	8,268✔
107
108	void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,	65,908✔
109	const Variable shared_region_size) const {
110	using namespace dsl_syntax;	32,954✔
111	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	98,890✔
112	require_value(dom.state, ub <= shared_region_size,	131,851✔
113	std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));	197,745✔
114	}	65,852✔
115
116	void EbpfChecker::operator()(const Comparable& s) const {	5,580✔
117	using namespace dsl_syntax;	2,790✔
118	if (dom.state.same_type(s.r1, s.r2)) {	5,580✔
119	// Same type. If both are numbers, that's okay. Otherwise:
120	TypeDomain non_number_types = dom.state.types;	5,570✔
121	non_number_types.remove_type(reg_type(s.r2), T_NUM);	5,570✔
122	// We must check that they belong to a singleton region:
123	if (!non_number_types.is_in_group(s.r1, TS_SINGLETON_PTR) && !non_number_types.is_in_group(s.r1, TS_MAP)) {	5,570✔
124	throw_fail("Cannot subtract pointers to non-singleton regions");	4✔
125	}
126	// And, to avoid wraparound errors, they must be within bounds.
127	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});	5,568✔
128	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});	5,566✔
129	} else {	5,570✔
130	// _Maybe_ different types, so r2 must be a number.
131	// We checked in a previous assertion that r1 is a pointer or a number.
132	if (!dom.state.entail_type(reg_type(s.r2), T_NUM)) {	10✔
133	throw_fail("Cannot subtract pointers to different regions");	9✔
134	}
135	}
136	}	5,570✔
137
138	void EbpfChecker::operator()(const Addable& s) const {	14,614✔
139	if (!dom.state.implies_superset(s.ptr, TS_POINTER, s.num, TS_NUM)) {	14,614✔
140	throw_fail("Only numbers can be added to pointers");	3✔
141	}
142	}	14,612✔
143
144	void EbpfChecker::operator()(const ValidDivisor& s) const {	286✔
145	using namespace dsl_syntax;	143✔
146	if (!dom.state.implies_superset(s.reg, TS_POINTER, s.reg, TS_NUM)) {	286✔
147	throw_fail("Only numbers can be used as divisors");	24✔
148	}
149	if (!thread_local_options.allow_division_by_zero) {	274✔
150	const auto reg = reg_pack(s.reg);	64✔
151	const auto v = s.is_signed ? reg.svalue : reg.uvalue;	64✔
152	require_value(dom.state, v != 0, "Possible division by zero");	256✔
153	}
154	}	210✔
155
156	void EbpfChecker::operator()(const ValidStore& s) const {	910✔
157	if (!dom.state.implies_not_type(s.mem, T_STACK, s.val, TS_NUM)) {	910✔
158	throw_fail("Only numbers can be stored to externally-visible regions");	3✔
159	}
160	}	908✔
161
162	void EbpfChecker::operator()(const TypeConstraint& s) const {	294,764✔
163	if (!dom.state.is_in_group(s.reg, to_typeset(s.types))) {	294,764✔
164	throw_fail("Invalid type");	315✔
165	}
166	}	294,554✔
167
168	void EbpfChecker::operator()(const BoundedLoopCount& s) const {	40✔
169	// Enforces an upper bound on loop iterations by checking that the loop counter
170	// does not exceed the specified limit
171	using namespace dsl_syntax;	20✔
172	const auto counter = variable_registry->loop_counter(to_string(s.name));	40✔
173	require_value(dom.state, counter <= BoundedLoopCount::limit, "Loop counter is too large");	115✔
174	}	18✔
175
176	void EbpfChecker::operator()(const FuncConstraint& s) const {	48✔
177	// Look up the helper function id.
178	if (dom.state.is_bottom()) {	48✔
179	return;
180	}
181	const auto src_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);	48✔
182	if (const auto sn = src_interval.singleton()) {	48✔
183	if (sn->fits<int32_t>()) {	46✔
184	// We can now process it as if the id was immediate.
185	const int32_t imm = sn->cast_to<int32_t>();	46✔
186	if (!thread_local_program_info->platform->is_helper_usable(imm)) {	46✔
187	throw_fail("invalid helper function id " + std::to_string(imm));	12✔
188	}
189	const Call call = make_call(imm, *thread_local_program_info->platform);	42✔
190	for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {	218✔
191	// TODO: create explicit sub assertions elsewhere
192	EbpfChecker{dom, sub_assertion}.visit();	334✔
193	}	42✔
194	return;	22✔
195	}	42✔
196	}
197	throw_fail("callx helper function id is not a valid singleton");	3✔
198	}
199
200	void EbpfChecker::operator()(const ValidSize& s) const {	10,026✔
201	using namespace dsl_syntax;	5,013✔
202	const auto r = reg_pack(s.reg);	10,026✔
203	require_value(dom.state, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");	25,555✔
204	}	9,928✔
205
206	void EbpfChecker::operator()(const ValidCallbackTarget& s) const {	8✔
207	const auto callback_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);	8✔
208	const auto callback_target = callback_interval.singleton();	8✔
209	if (!callback_target.has_value() \|\| !callback_target->fits<int32_t>()) {	8✔
UNCOV 210	throw_fail("callback function pointer must be a singleton code address");	×
211	}
212
213	const int32_t callback_label = callback_target->cast_to<int32_t>();	8✔
214	if (!thread_local_program_info->callback_target_labels.contains(callback_label)) {	8✔
215	throw_fail("callback function pointer does not reference a valid callback entry");	4✔
216	}
217	if (!thread_local_program_info->callback_targets_with_exit.contains(callback_label)) {	6✔
218	throw_fail("callback function does not have a reachable exit");	3✔
219	}
220	}	4✔
221
222	void EbpfChecker::operator()(const ValidMapKeyValue& s) const {	5,328✔
223	using namespace dsl_syntax;	2,664✔
224
225	const auto fd_type = dom.get_map_type(s.map_fd_reg);	5,328✔
226
227	const auto access_reg = reg_pack(s.access_reg);	5,328✔
228	int width;	2,664✔
229	if (s.key) {	5,328✔
230	const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();	4,614✔
231	if (!key_size.has_value()) {	4,614✔
UNCOV 232	throw_fail("Map key size is not singleton");	×
233	}
234	width = key_size->narrow<int>();	4,614✔
235	} else {
236	const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();	714✔
237	if (!value_size.has_value()) {	714✔
UNCOV 238	throw_fail("Map value size is not singleton");	×
239	}
240	width = value_size->narrow<int>();	714✔
241	}
242
243	for (const auto access_reg_type : dom.state.enumerate_types(s.access_reg)) {	10,614✔
244	if (access_reg_type == T_STACK) {	5,328✔
245	Interval offset = dom.state.values.eval_interval(access_reg.stack_offset);	5,254✔
246	if (!dom.stack.all_num_width(offset, Interval{width})) {	5,254✔
247	auto lb_is = offset.lb().number();	22✔
248	std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";	24✔
249	Interval ub = offset + Interval{width};	22✔
250	auto ub_is = ub.ub().number();	22✔
251	std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";	35✔
252	require_value(dom.state, LinearConstraint::false_const(),	44✔
253	"Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");	143✔
254	} else if (thread_local_options.strict && fd_type.has_value()) {	5,276✔
255	EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);	4✔
256	if (map_type.is_array) {	4✔
257	// Get offset value.
258	Variable key_ptr = access_reg.stack_offset;	4✔
259	std::optional<Number> offset_num = dom.state.values.eval_interval(key_ptr).singleton();	4✔
260	if (!offset_num.has_value()) {	4✔
UNCOV 261	throw_fail("Pointer must be a singleton");	×
262	} else if (s.key) {	4✔
263	// Look up the value pointed to by the key pointer.
264	Variable key_value =	2✔
265	variable_registry->cell_var(DataKind::svalues, offset_num.value(), sizeof(uint32_t));	4✔
266
267	if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {	6✔
268	require_value(dom.state, key_value < *max_entries, "Array index overflow");	16✔
269	} else {
UNCOV 270	throw_fail("Max entries is not finite");	×
271	}
272	require_value(dom.state, key_value >= 0, "Array index underflow");	2✔
273	}
274	}
275	}	4✔
276	} else if (access_reg_type == T_PACKET) {	74✔
277	Variable lb = access_reg.packet_offset;	44✔
278	LinearExpression ub = lb + width;	66✔
279	check_access_packet(lb, ub, {});	66✔
280	// Packet memory is both readable and writable.
281	} else if (access_reg_type == T_SHARED) {	74✔
282	Variable lb = access_reg.shared_offset;	30✔
283	LinearExpression ub = lb + width;	45✔
284	check_access_shared(lb, ub, access_reg.shared_region_size);	38✔
285	require_value(dom.state, access_reg.svalue > 0, "Possible null access");	68✔
286	// Shared memory is zero-initialized when created so is safe to read and write.
287	} else {	30✔
288	throw_fail("Only stack, packet, or shared can be used as a parameter");	21✔
289	}
290	}	5,328✔
291	}	5,286✔
292
293	static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,	89,544✔
294	const Variable offset_var) {
295	using namespace dsl_syntax;	44,772✔
296	LinearExpression lb = offset_var + s.offset;	134,316✔
297	LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v	129,473✔
298	: lb + reg_pack(std::get<Reg>(s.width)).svalue;	169,402✔
299	return {lb, ub};	134,316✔
300	}	89,544✔
301
302	void EbpfChecker::operator()(const ValidAccess& s) const {	111,446✔
303	using namespace dsl_syntax;	55,723✔
304
305	const bool is_comparison_check = s.width == Value{Imm{0}};	111,446✔
306
307	const auto reg = reg_pack(s.reg);	111,446✔
308	for (const auto type : dom.state.enumerate_types(s.reg)) {	222,752✔
309	switch (type) {	111,644✔
310	case T_PACKET: {	8,488✔
311	auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);	8,488✔
312	const std::optional<Variable> packet_size =	4,244✔
313	is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();	8,620✔
314	check_access_packet(lb, ub, packet_size);	8,488✔
315	// if within bounds, it can never be null
316	// Context memory is both readable and writable.
317	break;	8,224✔
318	}	8,488✔
319	case T_STACK: {	9,408✔
320	auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);	9,408✔
321	check_access_stack(lb, ub);	9,408✔
322	// if within bounds, it can never be null
323	if (s.access_type == AccessType::read &&	13,108✔
324	!dom.stack.all_num_lb_ub(dom.state.values.eval_interval(lb), dom.state.values.eval_interval(ub))) {	13,019✔
325
326	if (s.offset < 0) {	178✔
UNCOV 327	throw_fail("Stack content is not numeric");	×
328	} else {
329	using namespace dsl_syntax;	89✔
330	LinearExpression w = std::holds_alternative<Imm>(s.width)	178✔
331	? LinearExpression{std::get<Imm>(s.width).v}	178✔
332	: reg_pack(std::get<Reg>(s.width)).svalue;	186✔
333
334	require_value(dom.state, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");	391✔
335	}	178✔
336	}
337	break;	9,392✔
338	}	9,408✔
339	case T_CTX: {	5,770✔
340	auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);	5,770✔
341	check_access_context(lb, ub);	5,770✔
342	// if within bounds, it can never be null
343	// The context is both readable and writable.
344	break;	5,768✔
345	}	5,770✔
346	case T_SHARED: {	65,878✔
347	auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);	65,878✔
348	check_access_shared(lb, ub, reg.shared_region_size);	65,878✔
349	if (!is_comparison_check && !s.or_null) {	65,830✔
350	require_value(dom.state, reg.svalue > 0, "Possible null access");	159,516✔
351	}
352	// Shared memory is zero-initialized when created so is safe to read and write.
353	break;	65,824✔
354	}	65,878✔
355	case T_NUM:	22,040✔
356	if (!is_comparison_check) {	22,040✔
357	if (s.or_null) {	232✔
358	require_value(dom.state, reg.svalue == 0, "Non-null number");	468✔
359	} else {
360	throw_fail("Only pointers can be dereferenced");	×
361	}
362	}
363	break;	11,019✔
364	case T_MAP:	60✔
365	case T_MAP_PROGRAMS:	30✔
366	if (!is_comparison_check) {	60✔
UNCOV 367	throw_fail("FDs cannot be dereferenced directly");	×
368	}
369	break;	30✔
UNCOV 370	case T_SOCKET:	×
371	case T_BTF_ID:
372	// TODO: implement proper access checks for these pointer types.
UNCOV 373	if (!is_comparison_check) {	×
UNCOV 374	throw_fail("Unsupported pointer type for memory access");	×
375	}
376	break;
UNCOV 377	case T_ALLOC_MEM: {	×
378	// Treat like shared: offset-bounded access with null check.
UNCOV 379	auto [lb, ub] = lb_ub_access_pair(s, reg.alloc_mem_offset);	×
UNCOV 380	check_access_shared(lb, ub, reg.alloc_mem_size);	×
UNCOV 381	if (!is_comparison_check && !s.or_null) {	×
UNCOV 382	require_value(dom.state, reg.svalue > 0, "Possible null access");	×
383	}
UNCOV 384	break;	×
UNCOV 385	}	×
UNCOV 386	case T_FUNC:	×
UNCOV 387	if (!is_comparison_check) {	×
UNCOV 388	throw_fail("Function pointers cannot be dereferenced");	×
389	}
390	break;
391	default: throw_fail("Invalid type");	169✔
392	}
393	}	111,446✔
394	}	111,108✔
395
396	void EbpfChecker::operator()(const ZeroCtxOffset& s) const {	6,168✔
397	using namespace dsl_syntax;	3,084✔
398	const auto reg = reg_pack(s.reg);	6,168✔
399	// The domain is not expressive enough to handle join of null and non-null ctx,
400	// Since non-null ctx pointers are nonzero numbers.
401	if (s.or_null && dom.state.is_in_group(s.reg, TS_NUM) && dom.state.values.entail(reg.uvalue == 0)) {	9,300✔
402	return;	24✔
403	}
404	require_value(dom.state, reg.ctx_offset == 0, "Nonzero context offset");	12,292✔
405	}
406
407	} // namespace prevail

Alan-Jowett / ebpf-verifier / 22235569093

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