30559636792

Committed 27 Jul 2026 07:29AM UTC coverage: 86.764% (+0.1%) from 86.649%

Build # 30559636792

Build Type

push

github

Committed by

elazarg

Commit Message

Fix 32-bit soundness holes that let unsafe programs pass verification

Two independent classes of ALU32/JMP32 unsoundness allowed a crafted program to
be accepted while performing an out-of-bounds stack access.

MOVSX: the no-op fast path returned early for `wX sN= wX`, skipping the
zero-extension applied at the end of the function. The verifier kept a
sign-extended 64-bit value where the CPU produces a zero-extended 32-bit one, so
`r1 = r10; r2 = -1; w2 s8= r2; r1 += r2` was analyzed as r10 - 1 while the CPU
computes r10 + 0xFFFFFFFF, and the resulting out-of-bounds store was proved
in-bounds. The verifier already contradicted itself here: with r1 = -1,
`w2 s8= r1` yielded 0xFFFFFFFF but `w2 s8= r2` yielded -1 for the same operation
and input. Guard the fast path with bin.is64; the 64-bit form remains a no-op.

32-bit compares: the helpers emitted constraints over the 64-bit svalue/uvalue
variables after testing only the truncated 32-bit views. When a register's
64-bit value falls outside the 32-bit range those views say nothing about how the
64-bit variables are ordered, so branches that concrete executions do take were
proved dead, and unsafe code on them was never checked. Test the 64-bit intervals
instead, falling back to the existing no-constraint case. Precision is unchanged
for registers holding genuine 32-bit values, since the comparison itself pins the
operand's sign in the branches that assert one.

assume_unsigned_32bit_lt already guarded every branch this way, which is why only
the >, >=, s<, s<=, s> and s>= paths were affected.

Also drop the interval parameters these helpers no longer read.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Coverage Stats

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

107 existing lines in 5 files now uncovered.

9328 of 10751 relevant lines covered (86.76%)

6280124.66 hits per line

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

94.87

/src/string_constraints.cpp

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

#include <ostream>
#include <set>
#include <string>

#include "result.hpp"
#include "string_constraints.hpp"

namespace prevail {

std::set<std::string> StringInvariant::to_lines() const {
    if (is_bottom()) {
        return {"_|_"};
    }
    return *maybe_inv;
}

StringInvariant StringInvariant::operator+(const StringInvariant& b) const {
    if (this->is_bottom()) {
        return b;
    }
    if (b.is_bottom()) {
        return *this;
    }
    StringInvariant res = *this;
    for (const std::string& cst : b.value()) {
        if (!res.contains(cst)) {
            res.maybe_inv->insert(cst);
        }
    }
    return res;
}

std::ostream& operator<<(std::ostream& o, const StringInvariant& inv) {
    if (inv.is_bottom()) {
        return o << "_|_";
    }

    const RelevantState* filter = get_invariant_filter(o);

    bool first = true;
    o << "[";
    auto& set = inv.maybe_inv.value();
    std::string lastbase;
    for (const auto& item : set) {
        if (filter && !filter->is_relevant_constraint(item)) {
            continue;
        }

        if (first) {
            first = false;
        } else {
            o << ", ";
        }
        const size_t pos = item.find_first_of(".=[");
        std::string base = item.substr(0, pos);
        if (base != lastbase) {
            o << "\n    ";
            lastbase = base;
        }
        o << item;
    }
    o << "]";
    return o;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	#include <ostream>
5	#include <set>
6	#include <string>
7
8	#include "result.hpp"
9	#include "string_constraints.hpp"
10
11	namespace prevail {
12
13	std::set<std::string> StringInvariant::to_lines() const {	14✔
14	if (is_bottom()) {	14✔
15	return {"_\|_"};	6✔
16	}
17	return *maybe_inv;	8✔
18	}
19
20	StringInvariant StringInvariant::operator+(const StringInvariant& b) const {	2,216✔
21	if (this->is_bottom()) {	2,216✔
22	return b;	1,108✔
23	}
24	if (b.is_bottom()) {	2,216✔
UNCOV 25	return *this;	×
26	}
27	StringInvariant res = *this;	2,216✔
28	for (const std::string& cst : b.value()) {	6,928✔
29	if (!res.contains(cst)) {	4,712✔
30	res.maybe_inv->insert(cst);	4,712✔
31	}
32	}
33	return res;	2,216✔
34	}	2,216✔
35
36	std::ostream& operator<<(std::ostream& o, const StringInvariant& inv) {	12✔
37	if (inv.is_bottom()) {	12✔
UNCOV 38	return o << "_\|_";	×
39	}
40
41	const RelevantState* filter = get_invariant_filter(o);	12✔
42
43	bool first = true;	12✔
44	o << "[";	12✔
45	auto& set = inv.maybe_inv.value();	12✔
46	std::string lastbase;	12✔
47	for (const auto& item : set) {	90✔
48	if (filter && !filter->is_relevant_constraint(item)) {	78✔
49	continue;	60✔
50	}
51
52	if (first) {	18✔
53	first = false;	4✔
54	} else {
55	o << ", ";	10✔
56	}
57	const size_t pos = item.find_first_of(".=[");	18✔
58	std::string base = item.substr(0, pos);	18✔
59	if (base != lastbase) {	18✔
60	o << "\n ";	16✔
61	lastbase = base;	16✔
62	}
63	o << item;	18✔
64	}	18✔
65	o << "]";	12✔
66	return o;	12✔
67	}	12✔
68
69	} // namespace prevail

Alan-Jowett / ebpf-verifier / 30559636792

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