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

95.45

/src/io/elf_extern_resolve.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <cstdint>
#include <optional>
#include <string_view>
#include <vector>

#include "crab_utils/num_safety.hpp"
#include "io/elf_reader.hpp"

namespace prevail {

namespace {

constexpr uint32_t linux_kernel_version(const uint32_t major, const uint32_t minor, const uint32_t patch) {
    return (major << 16U) | (minor << 8U) | patch;
}

} // namespace

std::optional<uint64_t> resolve_known_linux_extern_symbol(const std::string_view symbol_name) {
    if (symbol_name == "LINUX_KERNEL_VERSION") {
        return linux_kernel_version(6, 6, 0);
    }
    if (symbol_name == "LINUX_HAS_SYSCALL_WRAPPER") {
        return 1;
    }
    if (symbol_name == "LINUX_HAS_BPF_COOKIE") {
        return 1;
    }
    if (symbol_name == "CONFIG_HZ") {
        return 250;
    }
    if (symbol_name == "CONFIG_BPF_SYSCALL") {
        return 1;
    }
    if (symbol_name == "CONFIG_DEFAULT_HOSTNAME") {
        // Store first character ('l' from "localhost"), matching common kconfig usage
        // where the program probes CONFIG_DEFAULT_HOSTNAME[0] for non-empty checks.
        return static_cast<uint64_t>('l');
    }
    return std::nullopt;
}

EbpfInst make_mov_reg_nop(const uint8_t reg) {
    return EbpfInst{
        .opcode = static_cast<uint8_t>(INST_CLS_ALU64 | INST_ALU_OP_MOV | INST_SRC_REG),
        .dst = reg,
        .src = reg,
        .offset = 0,
        .imm = 0,
    };
}

bool rewrite_extern_constant_load(std::vector<EbpfInst>& instructions, const size_t location, const uint64_t value) {
    if (instructions.size() <= location + 2) {
        return false;
    }

    auto [lo_inst, hi_inst] = validate_and_get_lddw_pair(instructions, location, "external symbol");
    EbpfInst& load_inst = instructions[location + 2];
    if ((load_inst.opcode & INST_CLS_MASK) != INST_CLS_LDX) {
        return false;
    }
    const uint8_t mode = load_inst.opcode & INST_MODE_MASK;
    if (mode != INST_MODE_MEM && mode != INST_MODE_MEMSX) {
        return false;
    }
    if (load_inst.src != lo_inst.get().dst || load_inst.offset != 0) {
        return false;
    }

    const auto width = opcode_to_width(load_inst.opcode);
    uint64_t narrowed_value = value;
    switch (width) {
    case 1: narrowed_value &= 0xffULL; break;
    case 2: narrowed_value &= 0xffffULL; break;
    case 4: narrowed_value &= 0xffffffffULL; break;
    case 8: break;
    default: return false;
    }
    if (mode == INST_MODE_MEMSX && width < 8) {
        const auto shift = gsl::narrow<int>(64U - static_cast<uint32_t>(width * 8));
        narrowed_value = static_cast<uint64_t>((static_cast<int64_t>(narrowed_value << shift)) >> shift);
    }

    // BPF MOV imm has a 32-bit immediate field that is sign-extended to 64 bits
    // by the runtime. Bail out if the value cannot survive the int32 → int64
    // sign-extension round-trip; the caller will fall back to the original
    // LDDW+LDX instruction sequence.
    if (!fits_narrow<int32_t>(narrowed_value)) {
        return false;
    }
    const auto truncated = static_cast<int32_t>(narrowed_value);

    // Use mov-imm to materialize the resolved constant in the destination register of
    // the load, and neutralize the preceding LDDW pair.
    const uint8_t mov_opcode = width == 8 || mode == INST_MODE_MEMSX
                                   ? static_cast<uint8_t>(INST_CLS_ALU64 | INST_ALU_OP_MOV | INST_SRC_IMM)
                                   : static_cast<uint8_t>(INST_CLS_ALU | INST_ALU_OP_MOV | INST_SRC_IMM);
    load_inst.opcode = mov_opcode;
    load_inst.src = 0;
    load_inst.offset = 0;
    load_inst.imm = truncated;

    lo_inst.get() = make_mov_reg_nop(lo_inst.get().dst);
    hi_inst.get() = make_mov_reg_nop(hi_inst.get().dst);
    return true;
}

bool rewrite_extern_address_load_to_zero(std::vector<EbpfInst>& instructions, const size_t location) {
    if (location + 1 >= instructions.size()) {
        return false;
    }
    if (instructions[location].opcode != INST_OP_LDDW_IMM) {
        return false;
    }

    auto [lo_inst, hi_inst] = validate_and_get_lddw_pair(instructions, location, "external symbol");
    lo_inst.get().imm = 0;
    hi_inst.get().imm = 0;
    return true;
}

bool rewrite_extern_kfunc_call(EbpfInst& instruction, const KsymBtfId& resolved_target) {
    if (instruction.opcode != INST_OP_CALL || instruction.src != INST_CALL_LOCAL || instruction.dst != 0) {
        return false;
    }
    if (instruction.offset != 0) {
        return false;
    }
    if (resolved_target.btf_id <= 0 || resolved_target.module < 0) {
        return false;
    }

    instruction.src = INST_CALL_BTF_HELPER;
    instruction.offset = resolved_target.module;
    instruction.imm = resolved_target.btf_id;
    return true;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <cstdint>
4	#include <optional>
5	#include <string_view>
6	#include <vector>
7
8	#include "crab_utils/num_safety.hpp"
9	#include "io/elf_reader.hpp"
10
11	namespace prevail {
12
13	namespace {
14
15	constexpr uint32_t linux_kernel_version(const uint32_t major, const uint32_t minor, const uint32_t patch) {	3✔
16	return (major << 16U) \| (minor << 8U) \| patch;	3✔
17	}
18
19	} // namespace
20
21	std::optional<uint64_t> resolve_known_linux_extern_symbol(const std::string_view symbol_name) {	232,890✔
22	if (symbol_name == "LINUX_KERNEL_VERSION") {	232,890✔
23	return linux_kernel_version(6, 6, 0);	6✔
24	}
25	if (symbol_name == "LINUX_HAS_SYSCALL_WRAPPER") {	232,884✔
26	return 1;	10✔
27	}
28	if (symbol_name == "LINUX_HAS_BPF_COOKIE") {	232,874✔
29	return 1;	18✔
30	}
31	if (symbol_name == "CONFIG_HZ") {	232,856✔
32	return 250;	14✔
33	}
34	if (symbol_name == "CONFIG_BPF_SYSCALL") {	232,842✔
35	return 1;	2✔
36	}
37	if (symbol_name == "CONFIG_DEFAULT_HOSTNAME") {	232,840✔
38	// Store first character ('l' from "localhost"), matching common kconfig usage
39	// where the program probes CONFIG_DEFAULT_HOSTNAME[0] for non-empty checks.
40	return static_cast<uint64_t>('l');	2✔
41	}
42	return std::nullopt;	232,838✔
43	}
44
45	EbpfInst make_mov_reg_nop(const uint8_t reg) {	58✔
46	return EbpfInst{
47	.opcode = static_cast<uint8_t>(INST_CLS_ALU64 \| INST_ALU_OP_MOV \| INST_SRC_REG),
48	.dst = reg,	58✔
49	.src = reg,	58✔
50	.offset = 0,
51	.imm = 0,
52	};	58✔
53	}
54
55	bool rewrite_extern_constant_load(std::vector<EbpfInst>& instructions, const size_t location, const uint64_t value) {	66✔
56	if (instructions.size() <= location + 2) {	66✔
57	return false;
58	}
59
60	auto [lo_inst, hi_inst] = validate_and_get_lddw_pair(instructions, location, "external symbol");	99✔
61	EbpfInst& load_inst = instructions[location + 2];	66✔
62	if ((load_inst.opcode & INST_CLS_MASK) != INST_CLS_LDX) {	66✔
63	return false;
64	}
65	const uint8_t mode = load_inst.opcode & INST_MODE_MASK;	66✔
66	if (mode != INST_MODE_MEM && mode != INST_MODE_MEMSX) {	66✔
67	return false;
68	}
69	if (load_inst.src != lo_inst.get().dst \|\| load_inst.offset != 0) {	66✔
70	return false;
71	}
72
73	const auto width = opcode_to_width(load_inst.opcode);	66✔
74	uint64_t narrowed_value = value;	66✔
75	switch (width) {	66✔
76	case 1: narrowed_value &= 0xffULL; break;	30✔
77	case 2: narrowed_value &= 0xffffULL; break;	×
78	case 4: narrowed_value &= 0xffffffffULL; break;	10✔
79	case 8: break;	13✔
80	default: return false;
81	}
82	if (mode == INST_MODE_MEMSX && width < 8) {	66✔
83	const auto shift = gsl::narrow<int>(64U - static_cast<uint32_t>(width * 8));	×
84	narrowed_value = static_cast<uint64_t>((static_cast<int64_t>(narrowed_value << shift)) >> shift);	×
85	}
86
87	// BPF MOV imm has a 32-bit immediate field that is sign-extended to 64 bits
88	// by the runtime. Bail out if the value cannot survive the int32 → int64
89	// sign-extension round-trip; the caller will fall back to the original
90	// LDDW+LDX instruction sequence.
91	if (!fits_narrow<int32_t>(narrowed_value)) {	66✔
92	return false;	4✔
93	}
94	const auto truncated = static_cast<int32_t>(narrowed_value);	58✔
95
96	// Use mov-imm to materialize the resolved constant in the destination register of
97	// the load, and neutralize the preceding LDDW pair.
98	const uint8_t mov_opcode = width == 8 \|\| mode == INST_MODE_MEMSX	78✔
99	? static_cast<uint8_t>(INST_CLS_ALU64 \| INST_ALU_OP_MOV \| INST_SRC_IMM)	78✔
100	: static_cast<uint8_t>(INST_CLS_ALU \| INST_ALU_OP_MOV \| INST_SRC_IMM);
101	load_inst.opcode = mov_opcode;	58✔
102	load_inst.src = 0;	58✔
103	load_inst.offset = 0;	58✔
104	load_inst.imm = truncated;	58✔
105
106	lo_inst.get() = make_mov_reg_nop(lo_inst.get().dst);	58✔
107	hi_inst.get() = make_mov_reg_nop(hi_inst.get().dst);	58✔
108	return true;	58✔
109	}
110
111	bool rewrite_extern_address_load_to_zero(std::vector<EbpfInst>& instructions, const size_t location) {	232,838✔
112	if (location + 1 >= instructions.size()) {	232,838✔
113	return false;
114	}
115	if (instructions[location].opcode != INST_OP_LDDW_IMM) {	232,838✔
116	return false;	116,349✔
117	}
118
119	auto [lo_inst, hi_inst] = validate_and_get_lddw_pair(instructions, location, "external symbol");	280✔
120	lo_inst.get().imm = 0;	140✔
121	hi_inst.get().imm = 0;	140✔
122	return true;	140✔
123	}
124
125	bool rewrite_extern_kfunc_call(EbpfInst& instruction, const KsymBtfId& resolved_target) {	98✔
126	if (instruction.opcode != INST_OP_CALL \|\| instruction.src != INST_CALL_LOCAL \|\| instruction.dst != 0) {	98✔
127	return false;
128	}
129	if (instruction.offset != 0) {	98✔
130	return false;
131	}
132	if (resolved_target.btf_id <= 0 \|\| resolved_target.module < 0) {	98✔
133	return false;
134	}
135
136	instruction.src = INST_CALL_BTF_HELPER;	98✔
137	instruction.offset = resolved_target.module;	98✔
138	instruction.imm = resolved_target.btf_id;	98✔
139	return true;	98✔
140	}
141
142	} // 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