13036894912

Committed 29 Jan 2025 05:24PM UTC coverage: 88.096% (-0.04%) from 88.133%

Build # 13036894912

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #127 from Alan-Jowett/verifier_fuzzing_support

Verifier fuzzing support

Run Details

0 of 5 new or added lines in 1 file covered. (0.0%)

2 existing lines in 1 file now uncovered.

8533 of 9686 relevant lines covered (88.1%)

7379587.78 hits per line

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

63.49

/src/crab_verifier.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
/**
 *  This module is about selecting the numerical and memory domains, initiating
 *  the verification process and returning the results.
 **/

#include <map>
#include <ranges>
#include <string>

#include "asm_files.hpp"
#include "asm_syntax.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/fwd_analyzer.hpp"
#include "crab_utils/lazy_allocator.hpp"
#include "crab_verifier.hpp"
#include "string_constraints.hpp"

using crab::ebpf_domain_t;
using std::string;

thread_local crab::lazy_allocator<program_info> thread_local_program_info;
thread_local ebpf_verifier_options_t thread_local_options;
void ebpf_verifier_clear_before_analysis();

// Note:
// The check is intended to find abstract state values that violate the constraints of the
// pre or post invariant. The check is done by the crab library.
// There are 4 possible outcomes:
// 1. The abstract state contains an invariant that is not present in the pre or post invariant.
// 2. The pre or post invariant contains an invariant that is not present in the abstract state.
// 3. The abstract state contains an invariant that is present in the pre or post invariant and
// the value of the invariant is within the constraints of the pre or post invariant.
// 4. The abstract state contains an invariant that is present in the pre or post invariant, but the
// value of the invariant is not within the constraints of the pre or post invariant.
// The check should return false only for the 4th case where there is a violation of the constraints.
// Usage of <= doesn't work as there are cases where the externally provided state contains constraints
// that the pre and post invariant doesn't have. Examples are the registers where the pre and post invariant
// have 'havoc'ed the constraints, but the externally provided state has constraints on the registers.

bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const {
    const ebpf_domain_t abstract_state =
        ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
    return !(abstract_state & invariants.at(label).post).is_bottom();
}

bool Invariants::is_valid_before(const label_t& label, const string_invariant& state) const {
    const ebpf_domain_t abstract_state =
        ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
    return !(abstract_state & invariants.at(label).pre).is_bottom();
}

string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }

crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }

int Invariants::max_loop_count() const {
    crab::extended_number max_loop_count{0};
    // Gather the upper bound of loop counts from post-invariants.
    for (const auto& inv_pair : std::views::values(invariants)) {
        max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound());
    }
    const auto m = max_loop_count.number();
    if (m && m->fits<int32_t>()) {
        return m->cast_to<int32_t>();
    }
    return std::numeric_limits<int>::max();
}

Invariants analyze(const Program& prog, ebpf_domain_t&& entry_invariant) {
    return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};
}

Invariants analyze(const Program& prog) {
    ebpf_verifier_clear_before_analysis();
    return analyze(prog, ebpf_domain_t::setup_entry(thread_local_options.setup_constraints));
}

Invariants analyze(const Program& prog, const string_invariant& entry_invariant) {
    ebpf_verifier_clear_before_analysis();
    return analyze(prog,
                   ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));
}

bool Invariants::verified(const Program& prog) const {
    for (const auto& [label, inv_pair] : invariants) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        for (const Assertion& assertion : prog.assertions_at(label)) {
            if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {
                return false;
            }
        }
    }
    return true;
}

Report Invariants::check_assertions(const Program& prog) const {
    Report report;
    for (const auto& [label, inv_pair] : invariants) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        for (const Assertion& assertion : prog.assertions_at(label)) {
            const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);
            for (const auto& msg : warnings) {
                report.warnings[label].emplace_back(msg);
            }
        }
        if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {
            if (inv_pair.post.is_bottom()) {
                const auto s = to_string(*passume);
                report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");
            }
        }
    }
    return report;
}

void ebpf_verifier_clear_before_analysis() {
    crab::domains::clear_thread_local_state();
    crab::variable_t::clear_thread_local_state();
}

void ebpf_verifier_clear_thread_local_state() {
    crab::CrabStats::clear_thread_local_state();
    thread_local_program_info.clear();
    crab::domains::clear_thread_local_state();
    crab::domains::SplitDBM::clear_thread_local_state();
}

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	/**
4	* This module is about selecting the numerical and memory domains, initiating
5	* the verification process and returning the results.
6	**/
7
8	#include <map>
9	#include <ranges>
10	#include <string>
11
12	#include "asm_files.hpp"
13	#include "asm_syntax.hpp"
14	#include "crab/ebpf_domain.hpp"
15	#include "crab/fwd_analyzer.hpp"
16	#include "crab_utils/lazy_allocator.hpp"
17	#include "crab_verifier.hpp"
18	#include "string_constraints.hpp"
19
20	using crab::ebpf_domain_t;
21	using std::string;
22
23	thread_local crab::lazy_allocator<program_info> thread_local_program_info;
24	thread_local ebpf_verifier_options_t thread_local_options;
25	void ebpf_verifier_clear_before_analysis();
26
27	// Note:
28	// The check is intended to find abstract state values that violate the constraints of the
29	// pre or post invariant. The check is done by the crab library.
30	// There are 4 possible outcomes:
31	// 1. The abstract state contains an invariant that is not present in the pre or post invariant.
32	// 2. The pre or post invariant contains an invariant that is not present in the abstract state.
33	// 3. The abstract state contains an invariant that is present in the pre or post invariant and
34	// the value of the invariant is within the constraints of the pre or post invariant.
35	// 4. The abstract state contains an invariant that is present in the pre or post invariant, but the
36	// value of the invariant is not within the constraints of the pre or post invariant.
37	// The check should return false only for the 4th case where there is a violation of the constraints.
38	// Usage of <= doesn't work as there are cases where the externally provided state contains constraints
39	// that the pre and post invariant doesn't have. Examples are the registers where the pre and post invariant
40	// have 'havoc'ed the constraints, but the externally provided state has constraints on the registers.
41
UNCOV 42	bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const {	×
43	const ebpf_domain_t abstract_state =
44	ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);	×
NEW 45	return !(abstract_state & invariants.at(label).post).is_bottom();	×
NEW 46	}	×
47
NEW 48	bool Invariants::is_valid_before(const label_t& label, const string_invariant& state) const {	×
49	const ebpf_domain_t abstract_state =
NEW 50	ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);	×
NEW 51	return !(abstract_state & invariants.at(label).pre).is_bottom();	×
UNCOV 52	}	×
53
54	string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }	1,380✔
55
56	crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }	438✔
57
58	int Invariants::max_loop_count() const {	×
59	crab::extended_number max_loop_count{0};	×
60	// Gather the upper bound of loop counts from post-invariants.
61	for (const auto& inv_pair : std::views::values(invariants)) {	×
62	max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound());	×
63	}
64	const auto m = max_loop_count.number();	×
65	if (m && m->fits<int32_t>()) {	×
66	return m->cast_to<int32_t>();	×
67	}
68	return std::numeric_limits<int>::max();
69	}	×
70
71	Invariants analyze(const Program& prog, ebpf_domain_t&& entry_invariant) {	2,486✔
72	return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};	3,729✔
73	}
74
75	Invariants analyze(const Program& prog) {	668✔
76	ebpf_verifier_clear_before_analysis();	668✔
77	return analyze(prog, ebpf_domain_t::setup_entry(thread_local_options.setup_constraints));	983✔
78	}
79
80	Invariants analyze(const Program& prog, const string_invariant& entry_invariant) {	1,818✔
81	ebpf_verifier_clear_before_analysis();	1,818✔
82	return analyze(prog,	909✔
83	ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));	2,727✔
84	}
85
86	bool Invariants::verified(const Program& prog) const {	1,068✔
87	for (const auto& [label, inv_pair] : invariants) {	138,350✔
88	if (inv_pair.pre.is_bottom()) {	137,326✔
89	continue;	836✔
90	}
91	for (const Assertion& assertion : prog.assertions_at(label)) {	253,436✔
92	if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {	116,990✔
93	return false;	44✔
94	}
95	}	136,490✔
96	}
97	return true;	512✔
98	}
99
100	Report Invariants::check_assertions(const Program& prog) const {	1,380✔
101	Report report;	1,380✔
102	for (const auto& [label, inv_pair] : invariants) {	6,712✔
103	if (inv_pair.pre.is_bottom()) {	5,332✔
104	continue;	540✔
105	}
106	for (const Assertion& assertion : prog.assertions_at(label)) {	7,674✔
107	const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);	2,882✔
108	for (const auto& msg : warnings) {	3,256✔
109	report.warnings[label].emplace_back(msg);	374✔
110	}
111	}	7,674✔
112	if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {	7,458✔
113	if (inv_pair.post.is_bottom()) {	558✔
114	const auto s = to_string(*passume);	192✔
115	report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");	384✔
116	}	192✔
117	}
118	}
119	return report;	1,380✔
120	}	×
121
122	void ebpf_verifier_clear_before_analysis() {	2,486✔
123	crab::domains::clear_thread_local_state();	2,486✔
124	crab::variable_t::clear_thread_local_state();	2,486✔
125	}	1,243✔
126
127	void ebpf_verifier_clear_thread_local_state() {	×
128	crab::CrabStats::clear_thread_local_state();	×
129	thread_local_program_info.clear();	×
130	crab::domains::clear_thread_local_state();	×
131	crab::domains::SplitDBM::clear_thread_local_state();	×
132	}	×

Alan-Jowett / ebpf-verifier / 13036894912

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