27778108035

Committed 07 Jun 2026 06:51PM UTC coverage: 86.386% (-2.5%) from 88.93%

Build # 27778108035

Build Type

push

github

Committed by

elazarg

Commit Message

Release v0.2.5

Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installed_package example version requirement.

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

Coverage Stats

9125 of 10563 relevant lines covered (86.39%)

6334294.72 hits per line

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

78.79

/src/linux/kfunc.cpp

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

#include "linux/kfunc.hpp"

#include <algorithm>
#include <array>
#include <string_view>

#include "ir/arg_kind.hpp"
#include "spec/function_prototypes.hpp"

namespace prevail {

namespace {

struct KfuncPrototypeEntry {
    int32_t btf_id{};
    int16_t module{};
    EbpfHelperPrototype proto{};
    KfuncFlags flags = KfuncFlags::none;
    std::string_view required_program_type;
    bool requires_privileged = false;
};

constexpr std::array<KfuncPrototypeEntry, 13> kfunc_prototypes{{
    {.btf_id = 12, .proto = {.name = "kfunc_test_id_overlap_tail_call", .return_type = EBPF_RETURN_TYPE_INTEGER}},
    {.btf_id = 1000, .proto = {.name = "kfunc_test_ret_int", .return_type = EBPF_RETURN_TYPE_INTEGER}},
    // Same BTF id as the prior entry, but provided by a different kernel module.
    // Used to verify that (btf_id, module) is the disambiguating key for kfunc
    // resolution — without this, two kfuncs sharing a BTF id across modules
    // would alias to the same prototype. See issue #1098.
    {.btf_id = 1000,
     .module = 1,
     .proto = {.name = "kfunc_test_ret_int_other_module", .return_type = EBPF_RETURN_TYPE_INTEGER}},
    {.btf_id = 1001,
     .proto = {.name = "kfunc_test_ctx_arg",
               .return_type = EBPF_RETURN_TYPE_INTEGER,
               .argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_CTX}}},
    {.btf_id = 1002,
     .proto = {.name = "kfunc_test_acquire_flag", .return_type = EBPF_RETURN_TYPE_INTEGER},
     .flags = KfuncFlags::acquire},
    {.btf_id = 1003,
     .proto = {.name = "kfunc_test_xdp_only", .return_type = EBPF_RETURN_TYPE_INTEGER},
     .required_program_type = "xdp"},
    {.btf_id = 1004,
     .proto = {.name = "kfunc_test_privileged_only", .return_type = EBPF_RETURN_TYPE_INTEGER},
     .requires_privileged = true},
    {.btf_id = 1005,
     .proto = {.name = "kfunc_test_ret_map_value_or_null", .return_type = EBPF_RETURN_TYPE_PTR_TO_MAP_VALUE_OR_NULL}},
    {.btf_id = 1006,
     .proto = {.name = "kfunc_test_readable_mem_or_null_size",
               .return_type = EBPF_RETURN_TYPE_INTEGER,
               .argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_READABLE_MEM_OR_NULL,
                                 EBPF_ARGUMENT_TYPE_CONST_SIZE_OR_ZERO}}},
    {.btf_id = 1007,
     .proto = {.name = "kfunc_test_writable_mem_size",
               .return_type = EBPF_RETURN_TYPE_INTEGER,
               .argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_WRITABLE_MEM, EBPF_ARGUMENT_TYPE_CONST_SIZE}}},
    {.btf_id = 1008,
     .proto = {.name = "kfunc_test_release_flag", .return_type = EBPF_RETURN_TYPE_INTEGER},
     .flags = KfuncFlags::release},
    // bpf_cpumask_create/bpf_cpumask_release form an acquire/release pair.
    // Acquire without enforced release — verifier does not yet track release obligations (see ID 1010).
    {.btf_id = 1009,
     .proto = {.name = "bpf_cpumask_create", .return_type = EBPF_RETURN_TYPE_INTEGER},
     .flags = KfuncFlags::acquire},
    {.btf_id = 1010, .proto = {.name = "bpf_cpumask_release", .return_type = EBPF_RETURN_TYPE_INTEGER}},
}};

constexpr bool kfunc_prototypes_are_sorted_by_key() {
    // Strict ordering on the (btf_id, module) pair: same btf_id is allowed
    // across distinct modules, but no exact duplicates and no out-of-order
    // pairs. This is what lets lookup_kfunc_prototype binary-search by btf_id
    // and then linear-scan the (small) module run to disambiguate.
    for (size_t i = 1; i < kfunc_prototypes.size(); ++i) {
        const auto& a = kfunc_prototypes[i - 1];
        const auto& b = kfunc_prototypes[i];
        if (a.btf_id > b.btf_id) {
            return false;
        }
        if (a.btf_id == b.btf_id && a.module >= b.module) {
            return false;
        }
    }
    return true;
}

constexpr bool kfunc_prototypes_have_names() {
    for (const auto& entry : kfunc_prototypes) {
        if (entry.proto.name == nullptr) {
            return false;
        }
    }
    return true;
}

static_assert(kfunc_prototypes_are_sorted_by_key(), "kfunc_prototypes must be strictly sorted by (btf_id, module)");
static_assert(kfunc_prototypes_have_names(), "kfunc_prototypes entries must define proto.name");

std::optional<KfuncPrototypeEntry> lookup_kfunc_prototype(const int32_t btf_id, const int16_t module) {
    auto it = std::lower_bound(kfunc_prototypes.begin(), kfunc_prototypes.end(), btf_id,
                               [](const KfuncPrototypeEntry& entry, const int32_t id) { return entry.btf_id < id; });
    for (; it != kfunc_prototypes.end() && it->btf_id == btf_id; ++it) {
        if (it->module == module) {
            return *it;
        }
    }
    return std::nullopt;
}

void set_unsupported(std::string* why_not, const std::string& reason) {
    if (why_not) {
        *why_not = reason;
    }
}

} // namespace

std::optional<ResolvedCall> make_kfunc_call(const int32_t btf_id, const int16_t module,
                                            const EbpfProgramType& program_type, std::string* why_not) {
    const auto entry = lookup_kfunc_prototype(btf_id, module);
    if (!entry) {
        std::string reason = "kfunc prototype lookup failed for BTF id " + std::to_string(btf_id);
        if (module != 0) {
            reason += " in module " + std::to_string(module);
        }
        set_unsupported(why_not, reason);
        return std::nullopt;
    }
    const auto& proto = entry->proto;

    ResolvedCall res;
    res.call = Call{.func = btf_id, .kind = CallKind::kfunc, .module = module};
    res.name = proto.name;
    res.contract.reallocate_packet = proto.reallocate_packet;
    res.contract.is_map_lookup = proto.return_type == EBPF_RETURN_TYPE_PTR_TO_MAP_VALUE_OR_NULL;

    // Per-flag handling: accept flags whose safety properties are covered by existing type checking,
    // reject flags that require unimplemented reference lifecycle tracking.
    constexpr auto accepted_flags =
        KfuncFlags::acquire | KfuncFlags::destructive | KfuncFlags::trusted_args | KfuncFlags::sleepable;
    // KF_ACQUIRE: type propagation works; release obligation not enforced (same gap as ringbuf).
    // KF_DESTRUCTIVE: privilege-level gate; no verification machinery needed.
    // KF_TRUSTED_ARGS: arguments already type-checked via the normal assertion path.
    // KF_SLEEPABLE: context constraint; not a memory-safety property.
    // KF_RELEASE: rejected — requires acquire/release state machine (see docs/parity/lifetime.md).
    if ((entry->flags & ~accepted_flags) != KfuncFlags::none) {
        set_unsupported(why_not, std::string("kfunc has unsupported flags (release requires lifecycle tracking): ") +
                                     proto.name);
        return std::nullopt;
    }
    if (!entry->required_program_type.empty() && program_type.name != entry->required_program_type) {
        set_unsupported(why_not,
                        std::string("kfunc is unavailable for program type ") + program_type.name + ": " + proto.name);
        return std::nullopt;
    }
    if (entry->requires_privileged && !program_type.is_privileged) {
        set_unsupported(why_not, std::string("kfunc requires privileged program type: ") + proto.name);
        return std::nullopt;
    }

    if (proto.unsupported || proto.return_type == EBPF_RETURN_TYPE_UNSUPPORTED) {
        set_unsupported(why_not, std::string("kfunc prototype is unavailable on this platform: ") + proto.name);
        return std::nullopt;
    }
    const auto return_info = classify_call_return_type(proto.return_type);
    if (!return_info.has_value()) {
        set_unsupported(why_not, std::string("kfunc return type is unsupported on this platform: ") + proto.name);
        return std::nullopt;
    }
    res.contract.return_ptr_type = return_info->pointer_type;
    res.contract.return_nullable = return_info->pointer_nullable;

    const std::array<ebpf_argument_type_t, 7> args = {
        {EBPF_ARGUMENT_TYPE_DONTCARE, proto.argument_type[0], proto.argument_type[1], proto.argument_type[2],
         proto.argument_type[3], proto.argument_type[4], EBPF_ARGUMENT_TYPE_DONTCARE}};
    for (size_t i = 1; i < args.size() - 1;) {
        switch (process_arg(res.contract, args, i)) {
        case ArgOutcome::Single: i += 1; break;
        case ArgOutcome::Pair: i += 2; break;
        case ArgOutcome::Stop: return res;
        case ArgOutcome::Unavailable:
            set_unsupported(why_not, std::string("kfunc argument type is unsupported on this platform: ") + proto.name);
            return std::nullopt;
        case ArgOutcome::MismatchedSize:
            set_unsupported(why_not,
                            std::string("kfunc pointer argument not followed by EBPF_ARGUMENT_TYPE_CONST_SIZE or "
                                        "EBPF_ARGUMENT_TYPE_CONST_SIZE_OR_ZERO: ") +
                                proto.name);
            return std::nullopt;
        }
    }
    return res;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	#include "linux/kfunc.hpp"
5
6	#include <algorithm>
7	#include <array>
8	#include <string_view>
9
10	#include "ir/arg_kind.hpp"
11	#include "spec/function_prototypes.hpp"
12
13	namespace prevail {
14
15	namespace {
16
17	struct KfuncPrototypeEntry {
18	int32_t btf_id{};
19	int16_t module{};
20	EbpfHelperPrototype proto{};
21	KfuncFlags flags = KfuncFlags::none;
22	std::string_view required_program_type;
23	bool requires_privileged = false;
24	};
25
26	constexpr std::array<KfuncPrototypeEntry, 13> kfunc_prototypes{{
27	{.btf_id = 12, .proto = {.name = "kfunc_test_id_overlap_tail_call", .return_type = EBPF_RETURN_TYPE_INTEGER}},
28	{.btf_id = 1000, .proto = {.name = "kfunc_test_ret_int", .return_type = EBPF_RETURN_TYPE_INTEGER}},
29	// Same BTF id as the prior entry, but provided by a different kernel module.
30	// Used to verify that (btf_id, module) is the disambiguating key for kfunc
31	// resolution — without this, two kfuncs sharing a BTF id across modules
32	// would alias to the same prototype. See issue #1098.
33	{.btf_id = 1000,
34	.module = 1,
35	.proto = {.name = "kfunc_test_ret_int_other_module", .return_type = EBPF_RETURN_TYPE_INTEGER}},
36	{.btf_id = 1001,
37	.proto = {.name = "kfunc_test_ctx_arg",
38	.return_type = EBPF_RETURN_TYPE_INTEGER,
39	.argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_CTX}}},
40	{.btf_id = 1002,
41	.proto = {.name = "kfunc_test_acquire_flag", .return_type = EBPF_RETURN_TYPE_INTEGER},
42	.flags = KfuncFlags::acquire},
43	{.btf_id = 1003,
44	.proto = {.name = "kfunc_test_xdp_only", .return_type = EBPF_RETURN_TYPE_INTEGER},
45	.required_program_type = "xdp"},
46	{.btf_id = 1004,
47	.proto = {.name = "kfunc_test_privileged_only", .return_type = EBPF_RETURN_TYPE_INTEGER},
48	.requires_privileged = true},
49	{.btf_id = 1005,
50	.proto = {.name = "kfunc_test_ret_map_value_or_null", .return_type = EBPF_RETURN_TYPE_PTR_TO_MAP_VALUE_OR_NULL}},
51	{.btf_id = 1006,
52	.proto = {.name = "kfunc_test_readable_mem_or_null_size",
53	.return_type = EBPF_RETURN_TYPE_INTEGER,
54	.argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_READABLE_MEM_OR_NULL,
55	EBPF_ARGUMENT_TYPE_CONST_SIZE_OR_ZERO}}},
56	{.btf_id = 1007,
57	.proto = {.name = "kfunc_test_writable_mem_size",
58	.return_type = EBPF_RETURN_TYPE_INTEGER,
59	.argument_type = {EBPF_ARGUMENT_TYPE_PTR_TO_WRITABLE_MEM, EBPF_ARGUMENT_TYPE_CONST_SIZE}}},
60	{.btf_id = 1008,
61	.proto = {.name = "kfunc_test_release_flag", .return_type = EBPF_RETURN_TYPE_INTEGER},
62	.flags = KfuncFlags::release},
63	// bpf_cpumask_create/bpf_cpumask_release form an acquire/release pair.
64	// Acquire without enforced release — verifier does not yet track release obligations (see ID 1010).
65	{.btf_id = 1009,
66	.proto = {.name = "bpf_cpumask_create", .return_type = EBPF_RETURN_TYPE_INTEGER},
67	.flags = KfuncFlags::acquire},
68	{.btf_id = 1010, .proto = {.name = "bpf_cpumask_release", .return_type = EBPF_RETURN_TYPE_INTEGER}},
69	}};
70
71	constexpr bool kfunc_prototypes_are_sorted_by_key() {
72	// Strict ordering on the (btf_id, module) pair: same btf_id is allowed
73	// across distinct modules, but no exact duplicates and no out-of-order
74	// pairs. This is what lets lookup_kfunc_prototype binary-search by btf_id
75	// and then linear-scan the (small) module run to disambiguate.
76	for (size_t i = 1; i < kfunc_prototypes.size(); ++i) {
77	const auto& a = kfunc_prototypes[i - 1];
78	const auto& b = kfunc_prototypes[i];
79	if (a.btf_id > b.btf_id) {
80	return false;
81	}
82	if (a.btf_id == b.btf_id && a.module >= b.module) {
83	return false;
84	}
85	}
86	return true;
87	}
88
89	constexpr bool kfunc_prototypes_have_names() {
90	for (const auto& entry : kfunc_prototypes) {
91	if (entry.proto.name == nullptr) {
92	return false;
93	}
94	}
95	return true;
96	}
97
98	static_assert(kfunc_prototypes_are_sorted_by_key(), "kfunc_prototypes must be strictly sorted by (btf_id, module)");
99	static_assert(kfunc_prototypes_have_names(), "kfunc_prototypes entries must define proto.name");
100
101	std::optional<KfuncPrototypeEntry> lookup_kfunc_prototype(const int32_t btf_id, const int16_t module) {	132✔
102	auto it = std::lower_bound(kfunc_prototypes.begin(), kfunc_prototypes.end(), btf_id,	132✔
103	[](const KfuncPrototypeEntry& entry, const int32_t id) { return entry.btf_id < id; });	504✔
104	for (; it != kfunc_prototypes.end() && it->btf_id == btf_id; ++it) {	208✔
105	if (it->module == module) {	122✔
106	return *it;	112✔
107	}
108	}
109	return std::nullopt;	20✔
110	}
111
112	void set_unsupported(std::string* why_not, const std::string& reason) {	26✔
113	if (why_not) {	26✔
114	*why_not = reason;	26✔
115	}
116	}	13✔
117
118	} // namespace
119
120	std::optional<ResolvedCall> make_kfunc_call(const int32_t btf_id, const int16_t module,	132✔
121	const EbpfProgramType& program_type, std::string* why_not) {
122	const auto entry = lookup_kfunc_prototype(btf_id, module);	132✔
123	if (!entry) {	132✔
124	std::string reason = "kfunc prototype lookup failed for BTF id " + std::to_string(btf_id);	20✔
125	if (module != 0) {	20✔
126	reason += " in module " + std::to_string(module);	6✔
127	}
128	set_unsupported(why_not, reason);	20✔
129	return std::nullopt;	20✔
130	}	20✔
131	const auto& proto = entry->proto;	112✔
132
133	ResolvedCall res;	112✔
134	res.call = Call{.func = btf_id, .kind = CallKind::kfunc, .module = module};	112✔
135	res.name = proto.name;	112✔
136	res.contract.reallocate_packet = proto.reallocate_packet;	112✔
137	res.contract.is_map_lookup = proto.return_type == EBPF_RETURN_TYPE_PTR_TO_MAP_VALUE_OR_NULL;	112✔
138
139	// Per-flag handling: accept flags whose safety properties are covered by existing type checking,
140	// reject flags that require unimplemented reference lifecycle tracking.
141	constexpr auto accepted_flags =	112✔
142	KfuncFlags::acquire \| KfuncFlags::destructive \| KfuncFlags::trusted_args \| KfuncFlags::sleepable;
143	// KF_ACQUIRE: type propagation works; release obligation not enforced (same gap as ringbuf).
144	// KF_DESTRUCTIVE: privilege-level gate; no verification machinery needed.
145	// KF_TRUSTED_ARGS: arguments already type-checked via the normal assertion path.
146	// KF_SLEEPABLE: context constraint; not a memory-safety property.
147	// KF_RELEASE: rejected — requires acquire/release state machine (see docs/parity/lifetime.md).
148	if ((entry->flags & ~accepted_flags) != KfuncFlags::none) {	112✔
149	set_unsupported(why_not, std::string("kfunc has unsupported flags (release requires lifecycle tracking): ") +	3✔
150	proto.name);	2✔
151	return std::nullopt;	2✔
152	}
153	if (!entry->required_program_type.empty() && program_type.name != entry->required_program_type) {	110✔
154	set_unsupported(why_not,	2✔
155	std::string("kfunc is unavailable for program type ") + program_type.name + ": " + proto.name);	7✔
156	return std::nullopt;	2✔
157	}
158	if (entry->requires_privileged && !program_type.is_privileged) {	108✔
159	set_unsupported(why_not, std::string("kfunc requires privileged program type: ") + proto.name);	5✔
160	return std::nullopt;	2✔
161	}
162
163	if (proto.unsupported \|\| proto.return_type == EBPF_RETURN_TYPE_UNSUPPORTED) {	106✔
164	set_unsupported(why_not, std::string("kfunc prototype is unavailable on this platform: ") + proto.name);	×
165	return std::nullopt;	×
166	}
167	const auto return_info = classify_call_return_type(proto.return_type);	106✔
168	if (!return_info.has_value()) {	106✔
169	set_unsupported(why_not, std::string("kfunc return type is unsupported on this platform: ") + proto.name);	×
170	return std::nullopt;	×
171	}
172	res.contract.return_ptr_type = return_info->pointer_type;	106✔
173	res.contract.return_nullable = return_info->pointer_nullable;	106✔
174
175	const std::array<ebpf_argument_type_t, 7> args = {	106✔
176	{EBPF_ARGUMENT_TYPE_DONTCARE, proto.argument_type[0], proto.argument_type[1], proto.argument_type[2],	106✔
177	proto.argument_type[3], proto.argument_type[4], EBPF_ARGUMENT_TYPE_DONTCARE}};	106✔
178	for (size_t i = 1; i < args.size() - 1;) {	197✔
179	switch (process_arg(res.contract, args, i)) {	144✔
180	case ArgOutcome::Single: i += 1; break;	10✔
181	case ArgOutcome::Pair: i += 2; break;	28✔
182	case ArgOutcome::Stop: return res;	106✔
183	case ArgOutcome::Unavailable:	×
184	set_unsupported(why_not, std::string("kfunc argument type is unsupported on this platform: ") + proto.name);	×
185	return std::nullopt;	×
186	case ArgOutcome::MismatchedSize:	×
187	set_unsupported(why_not,	×
188	std::string("kfunc pointer argument not followed by EBPF_ARGUMENT_TYPE_CONST_SIZE or "	×
189	"EBPF_ARGUMENT_TYPE_CONST_SIZE_OR_ZERO: ") +	×
190	proto.name);	×
191	return std::nullopt;	×
192	}
193	}
194	return res;	×
195	}	112✔
196
197	} // namespace prevail

Alan-Jowett / ebpf-verifier / 27778108035

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