From 514162ad06c381a8cd43312f0a4824a8e29d8565 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Thu, 10 Oct 2024 14:07:14 -0700 Subject: [PATCH 01/10] Add test case Signed-off-by: Dave Thaler --- test-data/calllocal.yaml | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml index fa2c811c..7338b7c2 100644 --- a/test-data/calllocal.yaml +++ b/test-data/calllocal.yaml @@ -1,6 +1,30 @@ # Copyright (c) Prevail Verifier contributors. # SPDX-License-Identifier: MIT --- +test-case: call local with stack + +pre: ["r10.type=stack", "r10.stack_offset=512", + "s[511...511].type=number", "s[511...511].svalue=2", "s[511...511].uvalue=2"] + +code: + : | + call + exit + : | + *(u8 *)(r10 - 1) = 1 ; this should not change s[511...511] + r0 = *(u8 *)(r10 - 1) + exit + +post: + - r0.type=number + - r0.svalue=1 + - r0.uvalue=1 + - r10.type=stack + - r10.stack_offset=512 + - s[511].type=number + - s[511].svalue=2 + - s[511].uvalue=2 +--- test-case: call local pre: [] From 2c20c44863d76a64615db89774bf846806aa66f6 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Thu, 10 Oct 2024 14:58:21 -0700 Subject: [PATCH 02/10] Update r10 for call local and exit Signed-off-by: Dave Thaler --- src/crab/ebpf_domain.cpp | 13 ++++++++++--- src/spec_type_descriptors.hpp | 3 +++ 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index baf8c398..ba92f3ec 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -912,8 +912,8 @@ void ebpf_domain_t::scratch_caller_saved_registers() { void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) { // Create variables specific to the new call stack frame that store - // copies of the states of r6 through r9. - for (int r = R6; r <= R9; r++) { + // copies of the states of r6 through r10. + for (int r = R6; r <= R10_STACK_POINTER; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::reg(kind, r); if (!m_inv[src_var].is_top()) { @@ -924,7 +924,7 @@ void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) { } void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { - for (int r = R6; r <= R9; r++) { + for (int r = R6; r <= R10_STACK_POINTER; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix); if (!m_inv[src_var].is_top()) { @@ -2213,6 +2213,13 @@ void ebpf_domain_t::operator()(const CallLocal& call) { return; } save_callee_saved_registers(call.stack_frame_prefix); + + // Lower r10.stack_offset to be the minimum stack area + // already initialized. + const auto r10 = reg_pack(R10_STACK_POINTER); + sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE); + + std::cout << "DEBUG: " << m_inv << "\n"; } void ebpf_domain_t::operator()(const Callx& callx) { diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index 8ed4d84d..b98ba00e 100644 --- a/src/spec_type_descriptors.hpp +++ b/src/spec_type_descriptors.hpp @@ -12,6 +12,9 @@ constexpr int EBPF_STACK_SIZE = 512; +// Stack space when subprograms are used. +constexpr int EBPF_SUBPROGRAM_STACK_SIZE = 256; + enum class EbpfMapValueType { ANY, MAP, PROGRAM }; struct EbpfMapType { From 3e2019d005955ae2e25a7b46bb5d40b21fccbd16 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Thu, 10 Oct 2024 22:04:51 -0700 Subject: [PATCH 03/10] Havoc stack on return from a subprogram Signed-off-by: Dave Thaler --- src/crab/ebpf_domain.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index ba92f3ec..42cf2c7c 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -924,6 +924,18 @@ void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) { } void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { + // First havoc the subprogram's stack. + variable_t r10_stack_offset = variable_t::reg(data_kind_t::stack_offsets, R10_STACK_POINTER); + auto r10_interval = m_inv.eval_interval(r10_stack_offset); + if (r10_interval.is_singleton()) { + int32_t stack_offset = r10_interval.singleton()->cast_to(); + int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE; + + for (const data_kind_t kind : iterate_kinds()) { + stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE); + } + } + for (int r = R6; r <= R10_STACK_POINTER; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix); @@ -2029,7 +2041,10 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, int width = b.access.width; const number_t offset{b.access.offset}; if (b.access.basereg.v == R10_STACK_POINTER) { - const number_t base_addr{EBPF_STACK_SIZE}; + auto r10_stack_offset = reg_pack(b.access.basereg).stack_offset; + const auto r10_interval = m_inv.eval_interval(r10_stack_offset); + const int32_t stack_offset = r10_interval.singleton()->cast_to(); + const number_t base_addr{stack_offset}; do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg); return; } @@ -2218,8 +2233,6 @@ void ebpf_domain_t::operator()(const CallLocal& call) { // already initialized. const auto r10 = reg_pack(R10_STACK_POINTER); sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE); - - std::cout << "DEBUG: " << m_inv << "\n"; } void ebpf_domain_t::operator()(const Callx& callx) { From dbacc841274675f9b9f0cce8c5cd00e55713e2d3 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 09:24:56 -0700 Subject: [PATCH 04/10] Increase subprogram stack size to 512 So we don't have to test whether subprograms exist or not for now Signed-off-by: Dave Thaler --- src/asm_cfg.cpp | 1 - src/asm_unmarshal.cpp | 2 +- src/assertions.cpp | 2 +- src/crab/array_domain.cpp | 2 +- src/crab/bitset_domain.cpp | 20 ++++++++++---------- src/crab/bitset_domain.hpp | 14 +++++++------- src/crab/ebpf_domain.cpp | 8 ++++---- src/ebpf_base.h | 8 ++++++++ src/ebpf_yaml.cpp | 18 +++++++++--------- src/spec_type_descriptors.hpp | 5 ----- test-data/calllocal.yaml | 14 +++++++------- 11 files changed, 48 insertions(+), 46 deletions(-) diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index 5d6439bf..e74606fd 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -119,7 +119,6 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t // Finally, recurse to replace any nested function macros. string caller_label_str = to_string(caller_label); long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2; - constexpr int MAX_CALL_STACK_FRAMES = 8; for (auto& macro_label : seen_labels) { for (const label_t label(macro_label.from, macro_label.to, caller_label_str); const auto& inst : cfg.get_node(label)) { diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 24086438..09491723 100644 --- a/src/asm_unmarshal.cpp +++ b/src/asm_unmarshal.cpp @@ -338,7 +338,7 @@ struct Unmarshaller { const uint8_t basereg = isLoad ? inst.src : inst.dst; if (basereg == R10_STACK_POINTER && - (inst.offset + opcode_to_width(inst.opcode) > 0 || inst.offset < -EBPF_STACK_SIZE)) { + (inst.offset + opcode_to_width(inst.opcode) > 0 || inst.offset < -EBPF_TOTAL_STACK_SIZE)) { note("Stack access out of bounds"); } auto res = Mem{ diff --git a/src/assertions.cpp b/src/assertions.cpp index 34a3d221..9ecf61c8 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -169,7 +169,7 @@ class AssertExtractor { const int offset = ins.access.offset; if (basereg.v == R10_STACK_POINTER) { // We know we are accessing the stack. - if (offset < -EBPF_STACK_SIZE || offset + static_cast(width.v) >= 0) { + if (offset < -EBPF_TOTAL_STACK_SIZE || offset + static_cast(width.v) >= 0) { // This assertion will fail res.emplace_back( ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write}); diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp index 9b4825a8..8fb23e47 100644 --- a/src/crab/array_domain.cpp +++ b/src/crab/array_domain.cpp @@ -816,7 +816,7 @@ void array_domain_t::havoc(NumAbsDomain& inv, const data_kind_t kind, const line void array_domain_t::store_numbers(const NumAbsDomain& inv, const variable_t _idx, const variable_t _width) { // TODO: this should be an user parameter. - const number_t max_num_elems = EBPF_STACK_SIZE; + const number_t max_num_elems = EBPF_TOTAL_STACK_SIZE; if (is_bottom()) { return; diff --git a/src/crab/bitset_domain.cpp b/src/crab/bitset_domain.cpp index e530c40f..af721cf7 100644 --- a/src/crab/bitset_domain.cpp +++ b/src/crab/bitset_domain.cpp @@ -6,23 +6,23 @@ std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) { o << "Numbers -> {"; bool first = true; - for (int i = -EBPF_STACK_SIZE; i < 0; i++) { - if (b.non_numerical_bytes[EBPF_STACK_SIZE + i]) { + for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) { + if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) { continue; } if (!first) { o << ", "; } first = false; - o << "[" << EBPF_STACK_SIZE + i; + o << "[" << EBPF_TOTAL_STACK_SIZE + i; int j = i + 1; for (; j < 0; j++) { - if (b.non_numerical_bytes[EBPF_STACK_SIZE + j]) { + if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) { break; } } if (j > i + 1) { - o << "..." << EBPF_STACK_SIZE + j - 1; + o << "..." << EBPF_TOTAL_STACK_SIZE + j - 1; } o << "]"; i = j; @@ -40,19 +40,19 @@ string_invariant bitset_domain_t::to_set() const { } std::set result; - for (int i = -EBPF_STACK_SIZE; i < 0; i++) { - if (non_numerical_bytes[EBPF_STACK_SIZE + i]) { + for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) { + if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) { continue; } - std::string value = "s[" + std::to_string(EBPF_STACK_SIZE + i); + std::string value = "s[" + std::to_string(EBPF_TOTAL_STACK_SIZE + i); int j = i + 1; for (; j < 0; j++) { - if (non_numerical_bytes[EBPF_STACK_SIZE + j]) { + if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) { break; } } if (j > i + 1) { - value += "..." + std::to_string(EBPF_STACK_SIZE + j - 1); + value += "..." + std::to_string(EBPF_TOTAL_STACK_SIZE + j - 1); } value += "].type=number"; result.insert(value); diff --git a/src/crab/bitset_domain.hpp b/src/crab/bitset_domain.hpp index a9f13654..c242f446 100644 --- a/src/crab/bitset_domain.hpp +++ b/src/crab/bitset_domain.hpp @@ -4,12 +4,12 @@ #include #include -#include "spec_type_descriptors.hpp" // for EBPF_STACK_SIZE +#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE #include "string_constraints.hpp" class bitset_domain_t final { private: - using bits_t = std::bitset; + using bits_t = std::bitset; bits_t non_numerical_bytes; public: @@ -64,7 +64,7 @@ class bitset_domain_t final { [[nodiscard]] std::pair uniformity(size_t lb, int width) const { - width = std::min(width, (int)(EBPF_STACK_SIZE - lb)); + width = std::min(width, (int)(EBPF_TOTAL_STACK_SIZE - lb)); bool only_num = true; bool only_non_num = true; for (int j = 0; j < width; j++) { @@ -82,21 +82,21 @@ class bitset_domain_t final { [[nodiscard]] int all_num_width(size_t lb) const { size_t ub = lb; - while ((ub < EBPF_STACK_SIZE) && !non_numerical_bytes[ub]) { + while ((ub < EBPF_TOTAL_STACK_SIZE) && !non_numerical_bytes[ub]) { ub++; } return (int)(ub - lb); } void reset(size_t lb, int n) { - n = std::min(n, (int)(EBPF_STACK_SIZE - lb)); + n = std::min(n, (int)(EBPF_TOTAL_STACK_SIZE - lb)); for (int i = 0; i < n; i++) { non_numerical_bytes.reset(lb + i); } } void havoc(size_t lb, int width) { - width = std::min(width, (int)(EBPF_STACK_SIZE - lb)); + width = std::min(width, (int)(EBPF_TOTAL_STACK_SIZE - lb)); for (int i = 0; i < width; i++) { non_numerical_bytes.set(lb + i); } @@ -109,7 +109,7 @@ class bitset_domain_t final { bool all_num(int32_t lb, int32_t ub) const { assert(lb < ub); lb = std::max(lb, 0); - ub = std::min(ub, EBPF_STACK_SIZE); + ub = std::min(ub, EBPF_TOTAL_STACK_SIZE); if (lb < 0 || ub > (int)non_numerical_bytes.size()) { return false; } diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 42cf2c7c..c3949c66 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -819,7 +819,7 @@ ebpf_domain_t ebpf_domain_t::calculate_constant_limits() { inv += r.svalue >= std::numeric_limits::min(); inv += r.uvalue <= std::numeric_limits::max(); inv += r.uvalue >= 0; - inv += r.stack_offset <= EBPF_STACK_SIZE; + inv += r.stack_offset <= EBPF_TOTAL_STACK_SIZE; inv += r.stack_offset >= 0; inv += r.shared_offset <= r.shared_region_size; inv += r.shared_offset >= 0; @@ -1199,7 +1199,7 @@ void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expressio const linear_expression_t& ub) const { using namespace crab::dsl_syntax; require(inv, lb >= 0, "Lower bound must be at least 0"); - require(inv, ub <= EBPF_STACK_SIZE, "Upper bound must be at most EBPF_STACK_SIZE"); + require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE"); } void ebpf_domain_t::check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, @@ -2912,9 +2912,9 @@ ebpf_domain_t ebpf_domain_t::setup_entry(const bool init_r1) { ebpf_domain_t inv; const auto r10 = reg_pack(R10_STACK_POINTER); constexpr Reg r10_reg{R10_STACK_POINTER}; - inv += EBPF_STACK_SIZE <= r10.svalue; + inv += EBPF_TOTAL_STACK_SIZE <= r10.svalue; inv += r10.svalue <= PTR_MAX; - inv.assign(r10.stack_offset, EBPF_STACK_SIZE); + inv.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE); // stack_numeric_size would be 0, but TOP has the same result // so no need to assign it. inv.type_inv.assign_type(inv.m_inv, r10_reg, T_STACK); diff --git a/src/ebpf_base.h b/src/ebpf_base.h index e6c96463..0f49a391 100644 --- a/src/ebpf_base.h +++ b/src/ebpf_base.h @@ -37,3 +37,11 @@ typedef struct _ebpf_context_descriptor { int end; // Offset into ctx struct of pointer to end of data. int meta; // Offset into ctx struct of pointer to metadata. } ebpf_context_descriptor_t; + +constexpr int MAX_CALL_STACK_FRAMES = 8; + +// Stack space per subprogram. +constexpr int EBPF_SUBPROGRAM_STACK_SIZE = 512; + +// Total stack space usable with nested subprogram calls. +constexpr int EBPF_TOTAL_STACK_SIZE (MAX_CALL_STACK_FRAMES * EBPF_SUBPROGRAM_STACK_SIZE); diff --git a/src/ebpf_yaml.cpp b/src/ebpf_yaml.cpp index 9b2e5712..c9cc1119 100644 --- a/src/ebpf_yaml.cpp +++ b/src/ebpf_yaml.cpp @@ -278,8 +278,8 @@ void add_stack_variable(std::set& more, int& offset, const std::vec using TU = std::make_unsigned_t; TS svalue; TU uvalue; - memcpy(&svalue, memory_bytes.data() + offset + memory_bytes.size() - EBPF_STACK_SIZE, sizeof(TS)); - memcpy(&uvalue, memory_bytes.data() + offset + memory_bytes.size() - EBPF_STACK_SIZE, sizeof(TU)); + memcpy(&svalue, memory_bytes.data() + offset + memory_bytes.size() - EBPF_TOTAL_STACK_SIZE, sizeof(TS)); + memcpy(&uvalue, memory_bytes.data() + offset + memory_bytes.size() - EBPF_TOTAL_STACK_SIZE, sizeof(TU)); more.insert("s[" + std::to_string(offset) + "..." + std::to_string(offset + sizeof(TS) - 1) + "].svalue" + "=" + std::to_string(svalue)); more.insert("s[" + std::to_string(offset) + "..." + std::to_string(offset + sizeof(TU) - 1) + "].uvalue" + "=" + @@ -289,14 +289,14 @@ void add_stack_variable(std::set& more, int& offset, const std::vec string_invariant stack_contents_invariant(const std::vector& memory_bytes) { std::set more = {"r1.type=stack", - "r1.stack_offset=" + std::to_string(EBPF_STACK_SIZE - memory_bytes.size()), + "r1.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()), "r1.stack_numeric_size=" + std::to_string(memory_bytes.size()), "r10.type=stack", - "r10.stack_offset=" + std::to_string(EBPF_STACK_SIZE), - "s[" + std::to_string(EBPF_STACK_SIZE - memory_bytes.size()) + "..." + - std::to_string(EBPF_STACK_SIZE - 1) + "].type=number"}; + "r10.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE), + "s[" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()) + "..." + + std::to_string(EBPF_TOTAL_STACK_SIZE - 1) + "].type=number"}; - int offset = EBPF_STACK_SIZE - gsl::narrow(memory_bytes.size()); + int offset = EBPF_TOTAL_STACK_SIZE - gsl::narrow(memory_bytes.size()); if (offset % 2 != 0) { add_stack_variable(more, offset, memory_bytes); } @@ -306,7 +306,7 @@ string_invariant stack_contents_invariant(const std::vector& memory_byt if (offset % 8 != 0) { add_stack_variable(more, offset, memory_bytes); } - while (offset < EBPF_STACK_SIZE) { + while (offset < EBPF_TOTAL_STACK_SIZE) { add_stack_variable(more, offset, memory_bytes); } @@ -324,7 +324,7 @@ ConformanceTestResult run_conformance_test_case(const std::vector& memo string_invariant pre_invariant = string_invariant::top(); if (!memory_bytes.empty()) { - if (memory_bytes.size() > EBPF_STACK_SIZE) { + if (memory_bytes.size() > EBPF_TOTAL_STACK_SIZE) { std::cerr << "memory size overflow\n"; return {}; } diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index b98ba00e..c4b33333 100644 --- a/src/spec_type_descriptors.hpp +++ b/src/spec_type_descriptors.hpp @@ -10,11 +10,6 @@ #include "crab_utils/lazy_allocator.hpp" -constexpr int EBPF_STACK_SIZE = 512; - -// Stack space when subprograms are used. -constexpr int EBPF_SUBPROGRAM_STACK_SIZE = 256; - enum class EbpfMapValueType { ANY, MAP, PROGRAM }; struct EbpfMapType { diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml index 7338b7c2..9e86bf41 100644 --- a/test-data/calllocal.yaml +++ b/test-data/calllocal.yaml @@ -3,15 +3,15 @@ --- test-case: call local with stack -pre: ["r10.type=stack", "r10.stack_offset=512", - "s[511...511].type=number", "s[511...511].svalue=2", "s[511...511].uvalue=2"] +pre: ["r10.type=stack", "r10.stack_offset=1024", + "s[1023...1023].type=number", "s[1023...1023].svalue=2", "s[1023...1023].uvalue=2"] code: : | call exit : | - *(u8 *)(r10 - 1) = 1 ; this should not change s[511...511] + *(u8 *)(r10 - 1) = 1 ; this should not change s[1023...1023] r0 = *(u8 *)(r10 - 1) exit @@ -20,10 +20,10 @@ post: - r0.svalue=1 - r0.uvalue=1 - r10.type=stack - - r10.stack_offset=512 - - s[511].type=number - - s[511].svalue=2 - - s[511].uvalue=2 + - r10.stack_offset=1024 + - s[1023].type=number + - s[1023].svalue=2 + - s[1023].uvalue=2 --- test-case: call local From 4c330539decfe3c015007791367df0faf2eaf904 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 09:34:48 -0700 Subject: [PATCH 05/10] Add test case with multiple stack levels Signed-off-by: Dave Thaler --- test-data/calllocal.yaml | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml index 9e86bf41..df62ff3f 100644 --- a/test-data/calllocal.yaml +++ b/test-data/calllocal.yaml @@ -3,27 +3,38 @@ --- test-case: call local with stack -pre: ["r10.type=stack", "r10.stack_offset=1024", - "s[1023...1023].type=number", "s[1023...1023].svalue=2", "s[1023...1023].uvalue=2"] +pre: ["r10.type=stack", "r10.stack_offset=1536", + "s[1535...1535].type=number", "s[1535...1535].svalue=1", "s[1535...1535].uvalue=1"] code: : | - call + call + r1 = *(u8 *)(r10 - 1) + r0 += r1 ; r0 = 1 + 2 + 3 = 6 exit - : | - *(u8 *)(r10 - 1) = 1 ; this should not change s[1023...1023] + : | + *(u8 *)(r10 - 1) = 2 ; this should not change the caller's stack + call + r1 = *(u8 *)(r10 - 1) + r0 += r1 ; r0 = 2 + 3 = 5 + exit + : | + *(u8 *)(r10 - 1) = 3 ; this should not change the caller's stack r0 = *(u8 *)(r10 - 1) exit post: - r0.type=number - - r0.svalue=1 - - r0.uvalue=1 + - r0.svalue=6 + - r0.uvalue=6 + - r1.type=number + - r1.svalue=1 + - r1.uvalue=1 - r10.type=stack - - r10.stack_offset=1024 - - s[1023].type=number - - s[1023].svalue=2 - - s[1023].uvalue=2 + - r10.stack_offset=1536 + - s[1535].type=number + - s[1535].svalue=1 + - s[1535].uvalue=1 --- test-case: call local From de750bb6ce42ba58e054109701a6255c0d4a01cf Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 10:14:00 -0700 Subject: [PATCH 06/10] Add test case for accessing beyond end of subprogram stack Signed-off-by: Dave Thaler --- src/assertions.cpp | 2 +- src/crab/ebpf_domain.cpp | 5 ++- test-data/calllocal.yaml | 70 ++++++++++++++++++++-------------------- test-data/stack.yaml | 23 +++++++++++++ 4 files changed, 63 insertions(+), 37 deletions(-) diff --git a/src/assertions.cpp b/src/assertions.cpp index 9ecf61c8..e9b2e587 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -169,7 +169,7 @@ class AssertExtractor { const int offset = ins.access.offset; if (basereg.v == R10_STACK_POINTER) { // We know we are accessing the stack. - if (offset < -EBPF_TOTAL_STACK_SIZE || offset + static_cast(width.v) >= 0) { + if (offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + static_cast(width.v) >= 0) { // This assertion will fail res.emplace_back( ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write}); diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index c3949c66..38d2ec9b 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -1198,7 +1198,10 @@ void ebpf_domain_t::operator()(const basic_block_t& bb) { void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const { using namespace crab::dsl_syntax; - require(inv, lb >= 0, "Lower bound must be at least 0"); + variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset; + int64_t stack_offset = m_inv.eval_interval(r10_stack_offset).singleton()->cast_to(); + require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE, + "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE"); require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE"); } diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml index df62ff3f..58eda114 100644 --- a/test-data/calllocal.yaml +++ b/test-data/calllocal.yaml @@ -1,41 +1,6 @@ # Copyright (c) Prevail Verifier contributors. # SPDX-License-Identifier: MIT --- -test-case: call local with stack - -pre: ["r10.type=stack", "r10.stack_offset=1536", - "s[1535...1535].type=number", "s[1535...1535].svalue=1", "s[1535...1535].uvalue=1"] - -code: - : | - call - r1 = *(u8 *)(r10 - 1) - r0 += r1 ; r0 = 1 + 2 + 3 = 6 - exit - : | - *(u8 *)(r10 - 1) = 2 ; this should not change the caller's stack - call - r1 = *(u8 *)(r10 - 1) - r0 += r1 ; r0 = 2 + 3 = 5 - exit - : | - *(u8 *)(r10 - 1) = 3 ; this should not change the caller's stack - r0 = *(u8 *)(r10 - 1) - exit - -post: - - r0.type=number - - r0.svalue=6 - - r0.uvalue=6 - - r1.type=number - - r1.svalue=1 - - r1.uvalue=1 - - r10.type=stack - - r10.stack_offset=1536 - - s[1535].type=number - - s[1535].svalue=1 - - s[1535].uvalue=1 ---- test-case: call local pre: [] @@ -369,3 +334,38 @@ post: [] messages: - "0/2: illegal recursion" +--- +test-case: call local with stack + +pre: ["r10.type=stack", "r10.stack_offset=1536", + "s[1535...1535].type=number", "s[1535...1535].svalue=1", "s[1535...1535].uvalue=1"] + +code: + : | + call + r1 = *(u8 *)(r10 - 1) + r0 += r1 ; r0 = 1 + 2 + 3 = 6 + exit + : | + *(u8 *)(r10 - 1) = 2 ; this should not change the caller's stack + call + r1 = *(u8 *)(r10 - 1) + r0 += r1 ; r0 = 2 + 3 = 5 + exit + : | + *(u8 *)(r10 - 1) = 3 ; this should not change the caller's stack + r0 = *(u8 *)(r10 - 1) + exit + +post: + - r0.type=number + - r0.svalue=6 + - r0.uvalue=6 + - r1.type=number + - r1.svalue=1 + - r1.uvalue=1 + - r10.type=stack + - r10.stack_offset=1536 + - s[1535].type=number + - s[1535].svalue=1 + - s[1535].uvalue=1 diff --git a/test-data/stack.yaml b/test-data/stack.yaml index 68fd3e86..8df80ca1 100644 --- a/test-data/stack.yaml +++ b/test-data/stack.yaml @@ -572,3 +572,26 @@ post: - r10.stack_offset=512 - r10.type=stack - s[498...511].type=number +--- +test-case: invalid stack access + +pre: ["r10.type=stack", "r10.stack_offset=1024"] + +code: + : | + *(u8 *)(r10 - 513) = 0 ; write out of range + r0 = 0 + exit + +post: + - r0.type=number + - r0.svalue=0 + - r0.uvalue=0 + - r10.type=stack + - r10.stack_offset=1024 + - s[511].type=number + - s[511].svalue=0 + - s[511].uvalue=0 + +messages: + - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE (valid_access(r10.offset-513, width=1) for write)" From 8aaff6a3130b122399004d43754cd00f226ddc4a Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 10:25:11 -0700 Subject: [PATCH 07/10] Simplify code Signed-off-by: Dave Thaler --- src/crab/ebpf_domain.cpp | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 38d2ec9b..032ffa2b 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -927,15 +927,13 @@ void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { // First havoc the subprogram's stack. variable_t r10_stack_offset = variable_t::reg(data_kind_t::stack_offsets, R10_STACK_POINTER); auto r10_interval = m_inv.eval_interval(r10_stack_offset); - if (r10_interval.is_singleton()) { - int32_t stack_offset = r10_interval.singleton()->cast_to(); - int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE; - - for (const data_kind_t kind : iterate_kinds()) { - stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE); - } + int32_t stack_offset = r10_interval.singleton()->cast_to(); + int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE; + for (const data_kind_t kind : iterate_kinds()) { + stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE); } + // Now restore registers. for (int r = R6; r <= R10_STACK_POINTER; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix); @@ -2232,8 +2230,6 @@ void ebpf_domain_t::operator()(const CallLocal& call) { } save_callee_saved_registers(call.stack_frame_prefix); - // Lower r10.stack_offset to be the minimum stack area - // already initialized. const auto r10 = reg_pack(R10_STACK_POINTER); sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE); } From 8a1c36a9582ac6f3a6bba33c4a402e508de8e162 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 13:27:07 -0700 Subject: [PATCH 08/10] Don't change r10 Signed-off-by: Dave Thaler --- src/asm_syntax.hpp | 11 ++++++++ src/assertions.cpp | 30 ++++++++++++-------- src/crab/bitset_domain.hpp | 4 +-- src/crab/ebpf_domain.cpp | 56 ++++++++++++++++++++++---------------- src/crab/ebpf_domain.hpp | 3 +- src/ebpf_base.h | 7 +++-- test-data/atomic.yaml | 40 +++++++++++++++++++++++++++ test-data/call.yaml | 18 ++++++++++-- test-data/calllocal.yaml | 8 +++--- test-data/callx.yaml | 11 +++++++- test-data/jump.yaml | 3 ++ test-data/stack.yaml | 2 +- test-data/subtract.yaml | 18 ++++++++---- 13 files changed, 156 insertions(+), 55 deletions(-) diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp index 9e7d13ab..a4e31786 100644 --- a/src/asm_syntax.hpp +++ b/src/asm_syntax.hpp @@ -51,6 +51,16 @@ struct label_t { return to != -1; } + [[nodiscard]] + int call_stack_depth() const { + // The call stack depth is the number of "/" separated components in the label, + // which is one more than the number of "/" separated components in the prefix. + if (stack_frame_prefix.empty()) { + return 1; + } + return 2 + std::count(stack_frame_prefix.begin(), stack_frame_prefix.end(), STACK_FRAME_DELIMITER); + } + friend std::ostream& operator<<(std::ostream& os, const label_t& label) { if (label == entry) { return os << "entry"; @@ -337,6 +347,7 @@ enum class AccessType { }; struct ValidAccess { + int call_stack_depth{}; Reg reg; int32_t offset{}; Value width{Imm{0}}; diff --git a/src/assertions.cpp b/src/assertions.cpp index e9b2e587..6d9e3335 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -27,6 +27,12 @@ class AssertExtractor { return res; } + ValidAccess make_valid_access(Reg reg, int32_t offset = {}, Value width = Imm{0}, bool or_null = {}, + AccessType access_type = {}) const { + int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1; + return ValidAccess{ depth, reg, offset, width, or_null, access_type}; + } + public: explicit AssertExtractor(program_info info, std::optional label) : info{std::move(info)}, current_label(label) {} @@ -99,17 +105,17 @@ class AssertExtractor { switch (arg.kind) { case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL: res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem_or_num}); - res.emplace_back(ValidAccess{arg.mem, 0, arg.size, true, AccessType::read}); + res.emplace_back(make_valid_access(arg.mem, 0, arg.size, true, AccessType::read)); break; case ArgPair::Kind::PTR_TO_READABLE_MEM: /* pointer to valid memory (stack, packet, map value) */ res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem}); - res.emplace_back(ValidAccess{arg.mem, 0, arg.size, false, AccessType::read}); + res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::read)); break; case ArgPair::Kind::PTR_TO_WRITABLE_MEM: // memory may be uninitialized, i.e. write only res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem}); - res.emplace_back(ValidAccess{arg.mem, 0, arg.size, false, AccessType::write}); + res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::write)); break; } // TODO: reg is constant (or maybe it's not important) @@ -137,14 +143,14 @@ class AssertExtractor { // no need to check for valid access, it must be a number res.emplace_back(TypeConstraint{cond.left, TypeGroup::number}); } else { - res.emplace_back(ValidAccess{cond.left}); + res.emplace_back(make_valid_access(cond.left)); // OK - map_fd is just another pointer // Anything can be compared to 0 } } else { const auto reg_right = get(cond.right); - res.emplace_back(ValidAccess{cond.left}); - res.emplace_back(ValidAccess{reg_right}); + res.emplace_back(make_valid_access(cond.left)); + res.emplace_back(make_valid_access(reg_right)); if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) { res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num}); } @@ -171,13 +177,13 @@ class AssertExtractor { // We know we are accessing the stack. if (offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + static_cast(width.v) >= 0) { // This assertion will fail - res.emplace_back( - ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write}); + res.emplace_back(make_valid_access(basereg, offset, width, false, + ins.is_load ? AccessType::read : AccessType::write)); } } else { res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer}); - res.emplace_back( - ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write}); + res.emplace_back(make_valid_access(basereg, offset, width, false, + ins.is_load ? AccessType::read : AccessType::write)); if (!info.type.is_privileged && !ins.is_load) { if (const auto preg = std::get_if(&ins.value)) { if (width.v != 8) { @@ -194,8 +200,8 @@ class AssertExtractor { vector operator()(const Atomic& ins) const { vector res; res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::pointer}); - res.emplace_back( - ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast(ins.access.width)}, false}); + res.emplace_back(make_valid_access(ins.access.basereg, ins.access.offset, + Imm{static_cast(ins.access.width)}, false)); if (ins.op == Atomic::Op::CMPXCHG) { // The memory contents pointed to by ins.access will be compared // against the value of the ins.valreg register. Only numbers are diff --git a/src/crab/bitset_domain.hpp b/src/crab/bitset_domain.hpp index c242f446..f047a854 100644 --- a/src/crab/bitset_domain.hpp +++ b/src/crab/bitset_domain.hpp @@ -4,7 +4,7 @@ #include #include -#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE +#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE constant #include "string_constraints.hpp" class bitset_domain_t final { @@ -109,7 +109,7 @@ class bitset_domain_t final { bool all_num(int32_t lb, int32_t ub) const { assert(lb < ub); lb = std::max(lb, 0); - ub = std::min(ub, EBPF_TOTAL_STACK_SIZE); + ub = std::min(ub, (int32_t)EBPF_TOTAL_STACK_SIZE); if (lb < 0 || ub > (int)non_numerical_bytes.size()) { return false; } diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 032ffa2b..f2401bb3 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -912,8 +912,8 @@ void ebpf_domain_t::scratch_caller_saved_registers() { void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) { // Create variables specific to the new call stack frame that store - // copies of the states of r6 through r10. - for (int r = R6; r <= R10_STACK_POINTER; r++) { + // copies of the states of r6 through r9. + for (int r = R6; r <= R9; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::reg(kind, r); if (!m_inv[src_var].is_top()) { @@ -924,17 +924,7 @@ void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) { } void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { - // First havoc the subprogram's stack. - variable_t r10_stack_offset = variable_t::reg(data_kind_t::stack_offsets, R10_STACK_POINTER); - auto r10_interval = m_inv.eval_interval(r10_stack_offset); - int32_t stack_offset = r10_interval.singleton()->cast_to(); - int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE; - for (const data_kind_t kind : iterate_kinds()) { - stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE); - } - - // Now restore registers. - for (int r = R6; r <= R10_STACK_POINTER; r++) { + for (int r = R6; r <= R9; r++) { for (const data_kind_t kind : iterate_kinds()) { const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix); if (!m_inv[src_var].is_top()) { @@ -947,6 +937,24 @@ void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { } } +void ebpf_domain_t::havoc_subprogram_stack(const std::string& prefix) { + // Calculate the call stack depth being returned from. Since we're returning + // *to* the given prefix, the current call stack is 1 + the number of + // '/'-separated labels in the prefix. + int call_stack_depth = 2 + std::count(prefix.begin(), prefix.end(), '/'); + + variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset; + auto intv = m_inv.eval_interval(r10_stack_offset); + if (!intv.is_singleton()) { + return; + } + int64_t stack_offset = intv.singleton()->cast_to(); + int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth; + for (const data_kind_t kind : iterate_kinds()) { + stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE); + } +} + void ebpf_domain_t::forget_packet_pointers() { using namespace crab::dsl_syntax; @@ -1194,12 +1202,15 @@ void ebpf_domain_t::operator()(const basic_block_t& bb) { } void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, - const linear_expression_t& ub) const { + const linear_expression_t& ub, int call_stack_depth) const { using namespace crab::dsl_syntax; variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset; - int64_t stack_offset = m_inv.eval_interval(r10_stack_offset).singleton()->cast_to(); - require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE, - "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE"); + auto interval = inv.eval_interval(r10_stack_offset); + if (interval.is_singleton()) { + int64_t stack_offset = interval.singleton()->cast_to(); + require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth, + "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth"); + } require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE"); } @@ -1367,6 +1378,7 @@ void ebpf_domain_t::operator()(const Exit& a) { if (prefix.empty()) { return; } + havoc_subprogram_stack(prefix); restore_callee_saved_registers(prefix); } @@ -1384,8 +1396,8 @@ void ebpf_domain_t::operator()(const Comparable& s) { return; } // And, to avoid wraparound errors, they must be within bounds. - this->operator()(ValidAccess{s.r1, 0, Imm{0}, false}); - this->operator()(ValidAccess{s.r2, 0, Imm{0}, false}); + 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. @@ -1676,7 +1688,7 @@ void ebpf_domain_t::operator()(const ValidAccess& s) { } case T_STACK: { auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset); - check_access_stack(inv, lb, ub); + check_access_stack(inv, lb, ub, s.call_stack_depth); // if within bounds, it can never be null if (s.access_type == AccessType::read) { // Require that the stack range contains numbers. @@ -2044,6 +2056,7 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, if (b.access.basereg.v == R10_STACK_POINTER) { auto r10_stack_offset = reg_pack(b.access.basereg).stack_offset; const auto r10_interval = m_inv.eval_interval(r10_stack_offset); + assert(r10_interval.is_singleton()); const int32_t stack_offset = r10_interval.singleton()->cast_to(); const number_t base_addr{stack_offset}; do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg); @@ -2229,9 +2242,6 @@ void ebpf_domain_t::operator()(const CallLocal& call) { return; } save_callee_saved_registers(call.stack_frame_prefix); - - const auto r10 = reg_pack(R10_STACK_POINTER); - sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE); } void ebpf_domain_t::operator()(const Callx& callx) { diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 9113df8c..486993b1 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -149,6 +149,7 @@ class ebpf_domain_t final { void scratch_caller_saved_registers(); void save_callee_saved_registers(const std::string& prefix); void restore_callee_saved_registers(const std::string& prefix); + void havoc_subprogram_stack(const std::string& prefix); [[nodiscard]] std::optional get_map_type(const Reg& map_fd_reg) const; [[nodiscard]] @@ -167,7 +168,7 @@ class ebpf_domain_t final { void require(domains::NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s) const; // memory check / load / store - void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const; + void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, int call_stack_depth) const; void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const; void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, std::optional packet_size) const; diff --git a/src/ebpf_base.h b/src/ebpf_base.h index 0f49a391..c44062d6 100644 --- a/src/ebpf_base.h +++ b/src/ebpf_base.h @@ -38,10 +38,13 @@ typedef struct _ebpf_context_descriptor { int meta; // Offset into ctx struct of pointer to metadata. } ebpf_context_descriptor_t; +// Maximum number of nested function calls allowed in eBPF programs. +// This limit helps prevent stack overflow and ensures predictable behavior. constexpr int MAX_CALL_STACK_FRAMES = 8; -// Stack space per subprogram. +// Stack space allocated for each subprogram (in bytes). +// This ensures each function call has its own dedicated stack space. constexpr int EBPF_SUBPROGRAM_STACK_SIZE = 512; // Total stack space usable with nested subprogram calls. -constexpr int EBPF_TOTAL_STACK_SIZE (MAX_CALL_STACK_FRAMES * EBPF_SUBPROGRAM_STACK_SIZE); +constexpr int EBPF_TOTAL_STACK_SIZE = MAX_CALL_STACK_FRAMES * EBPF_SUBPROGRAM_STACK_SIZE; diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml index d0e4e15a..c5f615d6 100644 --- a/test-data/atomic.yaml +++ b/test-data/atomic.yaml @@ -264,6 +264,7 @@ test-case: atomic 32-bit ADD stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] code: @@ -272,12 +273,14 @@ code: post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"] --- test-case: atomic 32-bit ADD and fetch stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] code: @@ -286,12 +289,14 @@ code: post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"] --- test-case: atomic 64-bit ADD stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] code: @@ -300,12 +305,14 @@ code: post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"] --- test-case: atomic 64-bit ADD and fetch stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] code: @@ -314,12 +321,14 @@ code: post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"] --- test-case: atomic 32-bit AND stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -328,12 +337,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] --- test-case: atomic 32-bit AND and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -342,12 +353,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] --- test-case: atomic 64-bit AND stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -356,12 +369,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] --- test-case: atomic 64-bit AND and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -370,12 +385,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] --- test-case: atomic 32-bit OR stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -384,12 +401,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"] --- test-case: atomic 32-bit OR and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -398,12 +417,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"] --- test-case: atomic 64-bit OR stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -412,12 +433,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"] --- test-case: atomic 64-bit OR and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -426,12 +449,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"] --- test-case: atomic 32-bit XOR stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -440,12 +465,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"] --- test-case: atomic 32-bit XOR and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -454,12 +481,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"] --- test-case: atomic 64-bit XOR stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -468,12 +497,14 @@ code: post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"] --- test-case: atomic 64-bit XOR and fetch stack pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -482,12 +513,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"] --- test-case: atomic 32-bit XCHG stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] code: @@ -496,12 +529,14 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=2", "s[4...7].uvalue=2"] --- test-case: atomic 64-bit XCHG stack pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] code: @@ -510,6 +545,7 @@ code: post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=2", "s[4...11].uvalue=2"] --- test-case: atomic 32-bit CMPXCHG stack @@ -517,6 +553,7 @@ test-case: atomic 32-bit CMPXCHG stack pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", "r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] code: @@ -526,6 +563,7 @@ code: post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", "r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...7].type=number"] --- test-case: atomic 64-bit CMPXCHG stack @@ -533,6 +571,7 @@ test-case: atomic 64-bit CMPXCHG stack pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", "r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] code: @@ -542,6 +581,7 @@ code: post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", "r1.type=number", "r1.svalue=2", "r1.uvalue=2", "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "r10.type=stack", "r10.stack_offset=512", "s[4...11].type=number"] --- test-case: atomic 32-bit ADD to non-pointer space diff --git a/test-data/call.yaml b/test-data/call.yaml index 235951b3..f75b4ecb 100644 --- a/test-data/call.yaml +++ b/test-data/call.yaml @@ -294,6 +294,7 @@ pre: ["r1.type=map_fd", "r1.map_fd=1", "r2.type=stack", "r2.stack_offset=504", "r3.type=number", "r3.svalue=8", "r3.uvalue=8", "r4.type=number", + "r10.type=stack", "r10.stack_offset=512", "s[504...511].type=number"] code: @@ -302,6 +303,8 @@ code: post: - r0.type=number + - r10.type=stack + - r10.stack_offset=512 - s[504...511].type=number --- test-case: bpf_ringbuf_output with non-numeric stack value @@ -309,7 +312,8 @@ test-case: bpf_ringbuf_output with non-numeric stack value pre: ["r1.type=map_fd", "r1.map_fd=1", "r2.type=stack", "r2.stack_offset=504", "r3.type=number", "r3.svalue=8", "r3.uvalue=8", - "r4.type=number"] + "r4.type=number", + "r10.type=stack", "r10.stack_offset=512"] code: : | @@ -317,6 +321,8 @@ code: post: - r0.type=number + - r10.type=stack + - r10.stack_offset=512 messages: - "0: Stack content is not numeric (valid_access(r2.offset, width=r3) for read)" @@ -345,7 +351,8 @@ test-case: bpf_get_stack pre: ["r1.type=ctx", "r1.ctx_offset=0", "r2.type=stack", "r2.stack_offset=504", "r3.type=number", "r3.svalue=8", "r3.uvalue=8", - "r4.type=number"] + "r4.type=number", + "r10.type=stack", "r10.stack_offset=512"] code: : | @@ -354,6 +361,8 @@ code: post: - r0.type=number - s[504...511].type=number + - r10.type=stack + - r10.stack_offset=512 --- test-case: bpf_get_stack overwriting ctx @@ -389,7 +398,8 @@ post: test-case: bpf_trace_printk with negative size buffer pre: ["r1.type=stack", "r1.stack_offset=504", - "r2.type=number", "r2.svalue=-13", "r2.uvalue=18446744073709551603"] + "r2.type=number", "r2.svalue=-13", "r2.uvalue=18446744073709551603", + "r10.type=stack", "r10.stack_offset=512"] code: : | @@ -397,6 +407,8 @@ code: post: - r0.type=number + - r10.type=stack + - r10.stack_offset=512 messages: - "0: Invalid size (r2.value > 0)" diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml index 58eda114..5f09446a 100644 --- a/test-data/calllocal.yaml +++ b/test-data/calllocal.yaml @@ -347,14 +347,14 @@ code: r0 += r1 ; r0 = 1 + 2 + 3 = 6 exit : | - *(u8 *)(r10 - 1) = 2 ; this should not change the caller's stack + *(u8 *)(r10 - 513) = 2 call - r1 = *(u8 *)(r10 - 1) + r1 = *(u8 *)(r10 - 513) r0 += r1 ; r0 = 2 + 3 = 5 exit : | - *(u8 *)(r10 - 1) = 3 ; this should not change the caller's stack - r0 = *(u8 *)(r10 - 1) + *(u8 *)(r10 - 1025) = 3 + r0 = *(u8 *)(r10 - 1025) exit post: diff --git a/test-data/callx.yaml b/test-data/callx.yaml index 44096aef..2af9e0a8 100644 --- a/test-data/callx.yaml +++ b/test-data/callx.yaml @@ -220,6 +220,7 @@ pre: ["r1.type=map_fd", "r1.map_fd=1", "r3.type=stack", "r3.stack_offset=496", "r4.type=number", "r8.type=number", "r8.svalue=2", "r8.uvalue=2", + "r10.type=stack", "r10.stack_offset=512", "s[496...511].type=number"] code: @@ -232,6 +233,8 @@ post: - r8.type=number - r8.svalue=2 - r8.uvalue=2 + - r10.type=stack + - r10.stack_offset=512 --- test-case: callx bpf_map_update_elem with shared value @@ -401,6 +404,7 @@ pre: ["r1.type=map_fd", "r1.map_fd=1", "r3.type=number", "r3.svalue=8", "r3.uvalue=8", "r4.type=number", "r8.type=number", "r8.svalue=130", "r8.uvalue=130", + "r10.type=stack", "r10.stack_offset=512", "s[504...511].type=number"] code: @@ -412,6 +416,8 @@ post: - r8.type=number - r8.svalue=130 - r8.uvalue=130 + - r10.type=stack + - r10.stack_offset=512 - s[504...511].type=number --- test-case: callx bpf_ringbuf_output with non-numeric stack value @@ -420,7 +426,8 @@ pre: ["r1.type=map_fd", "r1.map_fd=1", "r2.type=stack", "r2.stack_offset=504", "r3.type=number", "r3.svalue=8", "r3.uvalue=8", "r4.type=number", - "r8.type=number", "r8.svalue=130", "r8.uvalue=130"] + "r8.type=number", "r8.svalue=130", "r8.uvalue=130", + "r10.type=stack", "r10.stack_offset=512"] code: : | @@ -431,6 +438,8 @@ post: - r8.type=number - r8.svalue=130 - r8.uvalue=130 + - r10.type=stack + - r10.stack_offset=512 messages: - "0: Stack content is not numeric (valid_access(r2.offset, width=r3) for read)" diff --git a/test-data/jump.yaml b/test-data/jump.yaml index edc06391..22e11505 100644 --- a/test-data/jump.yaml +++ b/test-data/jump.yaml @@ -493,6 +493,7 @@ pre: ["r0.type=number", "r7.type=stack", "r7.stack_offset=0", "r8.type=packet", "r8.packet_offset=4", "r9.type=packet", "r9.packet_offset=0", + "r10.type=stack", "r10.stack_offset=512", "meta_offset=0"] code: @@ -532,6 +533,8 @@ post: - r8.packet_offset=4 - r9.type=packet - r9.packet_offset=0 + - r10.type=stack + - r10.stack_offset=512 messages: - "7:9: Code is unreachable after 7:9" diff --git a/test-data/stack.yaml b/test-data/stack.yaml index 8df80ca1..456097c4 100644 --- a/test-data/stack.yaml +++ b/test-data/stack.yaml @@ -594,4 +594,4 @@ post: - s[511].uvalue=0 messages: - - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE (valid_access(r10.offset-513, width=1) for write)" + - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth (valid_access(r10.offset-513, width=1) for write)" diff --git a/test-data/subtract.yaml b/test-data/subtract.yaml index 41200f5e..3c7047d9 100644 --- a/test-data/subtract.yaml +++ b/test-data/subtract.yaml @@ -101,7 +101,8 @@ test-case: allow subtraction of equal dual-typed pointers pre: ["r2.type=[-2, -1]", "r2.packet_offset=4", "r2.stack_offset=4", "r3.type=[-2, -1]", "r3.packet_offset=8", "r3.stack_offset=8", - "r2.type=r3.type", "meta_offset=-4", "packet_size=[16,32]"] + "r2.type=r3.type", "meta_offset=-4", "packet_size=[16,32]", + "r10.type=stack", "r10.stack_offset=512"] code: : | @@ -114,6 +115,8 @@ post: - r3.type=number - r3.svalue=4 - r3.uvalue=4 + - r10.type=stack + - r10.stack_offset=512 - meta_offset=-4 - packet_size=[16, 32] @@ -137,8 +140,9 @@ post: --- test-case: disallow subtraction of pointer from invalid pointer to a singleton region -pre: ["r1.type=stack", "r1.stack_offset=[500, 580]", - "r2.type=stack", "r2.stack_offset=[140, 230]"] +pre: ["r1.type=stack", "r1.stack_offset=[4040, 4130]", + "r2.type=stack", "r2.stack_offset=[140, 230]", + "r10.type=stack", "r10.stack_offset=4096"] code: : | @@ -146,10 +150,12 @@ code: post: - r1.type=number - - r1.svalue=[270, 440] - - r1.uvalue=[270, 440] + - r1.svalue=[3810, 3990] + - r1.uvalue=[3810, 3990] - r1.svalue=r1.uvalue - r2.type=stack - r2.stack_offset=[140, 230] + - r10.type=stack + - r10.stack_offset=4096 messages: - - "0: Upper bound must be at most EBPF_STACK_SIZE (r2.type == number or r1.type == r2.type in {ctx, stack, packet})" + - "0: Upper bound must be at most EBPF_TOTAL_STACK_SIZE (r2.type == number or r1.type == r2.type in {ctx, stack, packet})" From 0331ebe2d706f600797bc076aa4a5162b73ed413 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 13:59:17 -0700 Subject: [PATCH 09/10] Address coderabbit suggestions Signed-off-by: Dave Thaler --- src/asm_syntax.hpp | 5 +++-- src/crab/bitset_domain.hpp | 2 +- src/crab/ebpf_domain.cpp | 4 ++-- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp index a4e31786..3dd04c55 100644 --- a/src/asm_syntax.hpp +++ b/src/asm_syntax.hpp @@ -53,8 +53,9 @@ struct label_t { [[nodiscard]] int call_stack_depth() const { - // The call stack depth is the number of "/" separated components in the label, - // which is one more than the number of "/" separated components in the prefix. + // The call stack depth is the number of '/' separated components in the label, + // which is one more than the number of '/' separated components in the prefix, + // hence two more than the number of '/' in the prefix, if any. if (stack_frame_prefix.empty()) { return 1; } diff --git a/src/crab/bitset_domain.hpp b/src/crab/bitset_domain.hpp index f047a854..bb0d1270 100644 --- a/src/crab/bitset_domain.hpp +++ b/src/crab/bitset_domain.hpp @@ -109,7 +109,7 @@ class bitset_domain_t final { bool all_num(int32_t lb, int32_t ub) const { assert(lb < ub); lb = std::max(lb, 0); - ub = std::min(ub, (int32_t)EBPF_TOTAL_STACK_SIZE); + ub = std::min(ub, (int)EBPF_TOTAL_STACK_SIZE); if (lb < 0 || ub > (int)non_numerical_bytes.size()) { return false; } diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index f2401bb3..87d1156b 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -940,8 +940,8 @@ void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) { void ebpf_domain_t::havoc_subprogram_stack(const std::string& prefix) { // Calculate the call stack depth being returned from. Since we're returning // *to* the given prefix, the current call stack is 1 + the number of - // '/'-separated labels in the prefix. - int call_stack_depth = 2 + std::count(prefix.begin(), prefix.end(), '/'); + // '/'-separated labels in the prefix, hence 2 plus the number of separators in the prefix. + int call_stack_depth = 2 + std::count(prefix.begin(), prefix.end(), STACK_FRAME_DELIMITER); variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset; auto intv = m_inv.eval_interval(r10_stack_offset); From c5ba6d735c72e958e95382cbebae34437b1e5972 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 11 Oct 2024 15:13:34 -0700 Subject: [PATCH 10/10] Fix bug hit by a test Signed-off-by: Dave Thaler --- src/crab/ebpf_domain.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 87d1156b..2b38b6f7 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2056,10 +2056,11 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, if (b.access.basereg.v == R10_STACK_POINTER) { auto r10_stack_offset = reg_pack(b.access.basereg).stack_offset; const auto r10_interval = m_inv.eval_interval(r10_stack_offset); - assert(r10_interval.is_singleton()); - const int32_t stack_offset = r10_interval.singleton()->cast_to(); - const number_t base_addr{stack_offset}; - do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg); + if (r10_interval.is_singleton()) { + const int32_t stack_offset = r10_interval.singleton()->cast_to(); + const number_t base_addr{stack_offset}; + do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg); + } return; } m_inv = type_inv.join_over_types(m_inv, b.access.basereg, [&](NumAbsDomain& inv, const type_encoding_t type) {