Allow map_fd intervals

This case comes up in real eBPF programs, such as in Cilium's DSR code, where two maps differ only by max_entries. This change allows them to be used as long as the map type (and inner_map_fd, if a map of maps) are the same. Also move mock fd cache to program_info to avoid reusing the cache across different verification calls Signed-off-by: Dave Thaler <[email protected]>
dthaler · Oct 18, 2021 · 5e6968e · 5e6968e
1 parent 6b8c1c8
commit 5e6968e
Show file tree

Hide file tree

Showing 7 changed files with 149 additions and 26 deletions.
diff --git a/ebpf-samples b/ebpf-samples
diff --git a/src/asm_files.cpp b/src/asm_files.cpp
@@ -26,14 +26,12 @@ static vector<T> vector_of(const ELFIO::section& sec) {
 }
 
 int create_map_crab(const EbpfMapType& map_type, uint32_t key_size, uint32_t value_size, uint32_t max_entries, ebpf_verifier_options_t options) {
-    using EquivalenceKey = std::tuple<EbpfMapValueType, uint32_t, uint32_t, uint32_t>;
-    thread_local static std::map<EquivalenceKey, int> cache;
     EquivalenceKey equiv{map_type.value_type, key_size, value_size, map_type.is_array ? max_entries : 0};
-    if (!cache.count(equiv)) {
+    if (!global_program_info.cache.count(equiv)) {
         // +1 so 0 is the null FD
-        cache[equiv] = (int)cache.size() + 1;
+        global_program_info.cache[equiv] = (int)global_program_info.cache.size() + 1;
     }
-    return cache.at(equiv);
+    return global_program_info.cache.at(equiv);
 }
 
 EbpfMapDescriptor* find_map_descriptor(int map_fd) {

diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -19,6 +19,7 @@
 
 #include "asm_ostream.hpp"
 #include "config.hpp"
+#include "crab_verifier.hpp"
 #include "dsl_syntax.hpp"
 #include "platform.hpp"
 #include "string_constraints.hpp"
@@ -255,8 +256,8 @@ void ebpf_domain_t::forget_packet_pointers() {
 
     for (variable_t v : variable_t::get_type_variables()) {
         // TODO: this is sufficient, but for clarity it may be useful to forget the offset and value too.
-       if (m_inv.intersect(v == T_PACKET))
-           m_inv -= v;
+        if (m_inv.intersect(v == T_PACKET))
+            m_inv -= v;
     }
 }
 
@@ -489,30 +490,131 @@ void ebpf_domain_t::operator()(const ValidSize& s) {
     require(m_inv, s.can_be_zero ? r.value >= 0 : r.value > 0, to_string(s));
 }
 
-std::optional<EbpfMapDescriptor> ebpf_domain_t::get_map_descriptor(const Reg& map_fd_reg) {
-    // Get the actual map_fd value to look up the key size and value size.
-    if (auto fd_opt = m_inv[reg_pack(map_fd_reg).offset].singleton()) {
-        return global_program_info.platform->get_map_descriptor((int)*fd_opt);
-    } else {
+// Get the start and end of the range of possible map fd values.
+// In the future, it would be cleaner to use a set rather than an interval
+// for map fds.
+bool ebpf_domain_t::get_map_fd_range(const Reg& map_fd_reg, int* start_fd, int* end_fd) const {
+    const crab::interval_t& map_fd_interval = m_inv[reg_pack(map_fd_reg).offset];
+    auto lb = map_fd_interval.lb().number();
+    auto ub = map_fd_interval.ub().number();
+    if (!lb || !lb->fits_sint() || !ub || !ub->fits_sint())
+        return false;
+    *start_fd = (int)lb.value();
+    *end_fd = (int)ub.value();
+
+    // Cap the maximum range we'll check.
+    const int max_range = 32;
+    return (*map_fd_interval.finite_size() < max_range);
+}
+
+// All maps in the range must have the same type for us to use it.
+std::optional<uint32_t> ebpf_domain_t::get_map_type(const Reg& map_fd_reg) const {
+    int start_fd, end_fd;
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+        return std::optional<uint32_t>();
+
+    std::optional<uint32_t> type;
+    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
+        EbpfMapDescriptor* map = find_map_descriptor(map_fd);
+        if (map == nullptr)
+            return std::optional<uint32_t>();
+        if (!type.has_value())
+            type = map->type;
+        else if (map->type != *type)
+            return std::optional<uint32_t>();
+    }
+    return type;
+}
+
+// All maps in the range must have the same inner map fd for us to use it.
+std::optional<uint32_t> ebpf_domain_t::get_map_inner_map_fd(const Reg& map_fd_reg) const {
+    int start_fd, end_fd;
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
         return {};
+
+    std::optional<uint32_t> inner_map_fd;
+    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
+        EbpfMapDescriptor* map = find_map_descriptor(map_fd);
+        if (map == nullptr)
+            return {};
+        if (!inner_map_fd.has_value())
+            inner_map_fd = map->inner_map_fd;
+        else if (map->type != *inner_map_fd)
+            return {};
+    }
+    return inner_map_fd;
+}
+
+// We can deal with a range of key sizes.
+crab::interval_t ebpf_domain_t::get_map_key_size(const Reg& map_fd_reg) const {
+    int start_fd, end_fd;
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+        return crab::interval_t::top();
+
+    crab::interval_t result = crab::interval_t::bottom();
+    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
+        if (EbpfMapDescriptor* map = find_map_descriptor(map_fd))
+            result = result | crab::interval_t(number_t(map->key_size));
+        else
+            return crab::interval_t::top();
     }
+    return result;
+}
+
+// We can deal with a range of value sizes.
+crab::interval_t ebpf_domain_t::get_map_value_size(const Reg& map_fd_reg) const {
+    int start_fd, end_fd;
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+        return crab::interval_t::top();
+
+    crab::interval_t result = crab::interval_t::bottom();
+    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
+        if (EbpfMapDescriptor* map = find_map_descriptor(map_fd))
+            result = result | crab::interval_t(number_t(map->value_size));
+        else
+            return crab::interval_t::top();
+    }
+    return result;
+}
+
+// We can deal with a range of max_entries values.
+crab::interval_t ebpf_domain_t::get_map_max_entries(const Reg& map_fd_reg) const {
+    int start_fd, end_fd;
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+        return crab::interval_t::top();
+
+    crab::interval_t result = crab::interval_t::bottom();
+    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
+        if (EbpfMapDescriptor* map = find_map_descriptor(map_fd))
+            result = result | crab::interval_t(number_t(map->max_entries));
+        else
+            return crab::interval_t::top();
+    }
+    return result;
 }
 
 void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
     using namespace crab::dsl_syntax;
 
-    auto maybe_map_descriptor = get_map_descriptor(s.map_fd_reg);
-    if (!maybe_map_descriptor) {
-        require(m_inv, linear_constraint_t::FALSE(), "Map fd is not singleton");
+    auto key_size = get_map_key_size(s.map_fd_reg).singleton();
+    if (!key_size.has_value()) {
+        require(m_inv, linear_constraint_t::FALSE(), "Map key size is not singleton");
         return;
     }
+    auto value_size = get_map_value_size(s.map_fd_reg).singleton();
+    if (!value_size.has_value()) {
+        require(m_inv, linear_constraint_t::FALSE(), "Map value size is not singleton");
+        return;
+    }
+    auto type = get_map_type(s.map_fd_reg);
+
     auto access_reg = reg_pack(s.access_reg);
     std::string m = std::string(" (") + to_string(s) + ")";
     require(m_inv, access_reg.type >= T_STACK, "Only stack or packet can be used as a parameter" + m);
     require(m_inv, access_reg.type <= T_PACKET, "Only stack or packet can be used as a parameter" + m);
 
     variable_t lb = access_reg.offset;
-    int width = s.key ? (int)maybe_map_descriptor->key_size : (int)maybe_map_descriptor->value_size;
+    int width = s.key ? (int)key_size.value() : (int)value_size.value();
     linear_expression_t ub = lb + width;
 
     auto when_stack = when(access_reg.type == T_STACK);
@@ -523,8 +625,8 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
             auto ub_is = when_stack.eval_interval(ub).ub().number();
             std::string ub_s = ub_is && ub_is->fits_sint() ? std::to_string((int)*ub_is) : "oo";
             require(when_stack, access_reg.type != T_STACK, "Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");
-        } else if (thread_local_options.strict && maybe_map_descriptor.has_value()) {
-            EbpfMapType map_type = global_program_info.platform->get_map_type(maybe_map_descriptor->type);
+        } else if (thread_local_options.strict && type.has_value()) {
+            EbpfMapType map_type = global_program_info.platform->get_map_type(*type);
             if (map_type.is_array) {
                 // Get offset value.
                 variable_t key_ptr = access_reg.offset;
@@ -536,7 +638,10 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
                     variable_t key_value =
                         variable_t::cell_var(data_kind_t::values, (uint64_t)offset.value(), sizeof(uint32_t));
 
-                    require(m_inv, key_value < maybe_map_descriptor->max_entries, "Array index overflow");
+                    auto max_entries = get_map_max_entries(s.map_fd_reg).lb().number();
+                    if (!max_entries.has_value())
+                        require(m_inv, linear_constraint_t::FALSE(), "Max entries is not finite");
+                    require(m_inv, key_value < *max_entries, "Array index overflow");
                     require(m_inv, key_value >= 0, "Array index underflow");
                 }
             }
@@ -934,15 +1039,19 @@ void ebpf_domain_t::operator()(const Call& call) {
     if (call.is_map_lookup) {
         // This is the only way to get a null pointer
         if (maybe_fd_reg) {
-            if (auto maybe_map_descriptor = get_map_descriptor(*maybe_fd_reg)) {
-                if (global_program_info.platform->get_map_type(maybe_map_descriptor->type).value_type == EbpfMapValueType::MAP) {
-                    do_load_mapfd(r0, (int)maybe_map_descriptor->inner_map_fd, true);
+            if (auto map_type = get_map_type(*maybe_fd_reg)) {
+                if (global_program_info.platform->get_map_type(*map_type).value_type == EbpfMapValueType::MAP) {
+                    auto inner_map_fd = get_map_inner_map_fd(*maybe_fd_reg);
+                    if (inner_map_fd.has_value()) {
+                        do_load_mapfd(r0, (int)*inner_map_fd, true);
+                        goto out;
+                    }
                 } else {
                     assign_valid_ptr(r0, true);
                     assign(r0.offset, 0);
-                    assign(r0.type, maybe_map_descriptor->value_size);
+                    m_inv.set(r0.type, get_map_value_size(*maybe_fd_reg));
+                    goto out;
                 }
-                goto out;
             }
         }
         assign_valid_ptr(r0, true);

diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
@@ -134,7 +134,11 @@ class ebpf_domain_t final {
     NumAbsDomain when(const linear_constraint_t& condition);
 
     void scratch_caller_saved_registers();
-    std::optional<EbpfMapDescriptor> get_map_descriptor(const Reg& map_fd_reg);
+    std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
+    std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
+    crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
+    crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
+    crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
     void forget_packet_pointers();
     void do_load_mapfd(const reg_pack_t& dst, int mapfd, bool maybe_null);
 
@@ -183,5 +187,6 @@ class ebpf_domain_t final {
     crab::domains::array_domain_t stack;
 
     std::function<check_require_func_t> check_require{};
+    bool get_map_fd_range(const Reg& map_fd_reg, int* start_fd, int* end_fd) const;
 
 }; // end ebpf_domain_t
diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp
@@ -216,6 +216,8 @@ class interval_t final {
 
     static interval_t bottom() { return interval_t(); }
 
+    [[nodiscard]] std::optional<number_t> finite_size() const { return (_ub - _lb).number(); }
+
   private:
     interval_t() : _lb(0), _ub(-1) {}
 

diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
+#include <map>
 #include <string>
 #include <vector>
 #include "ebpf_base.h"
@@ -38,10 +39,17 @@ struct EbpfProgramType {
 };
 void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, std::ostream& o);
 
+using EquivalenceKey = std::tuple<
+    EbpfMapValueType /* value_type */,
+    uint32_t /* key_size */,
+    uint32_t /* value_size */,
+    uint32_t /* max_entries */>;
+
 struct program_info {
     const struct ebpf_platform_t* platform;
     std::vector<EbpfMapDescriptor> map_descriptors;
     EbpfProgramType type;
+    std::map<EquivalenceKey, int> cache;
 };
 
 struct raw_program {

diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp
@@ -449,6 +449,7 @@ TEST_SECTION("build", "stackok.o", ".text")
 TEST_SECTION("build", "packet_start_ok.o", "xdp")
 TEST_SECTION("build", "tail_call.o", "xdp_prog")
 TEST_SECTION("build", "map_in_map.o", ".text")
+TEST_SECTION("build", "twomaps.o", ".text");
 
 // Test some programs that ought to fail verification.
 TEST_SECTION_REJECT("build", "badhelpercall.o", ".text")
+5 −0		CMakeLists.txt
+ −		build/twomaps.o
+48 −0		src/twomaps.c