Skip to content

Commit

Permalink
Only set type to pointer if the width is correct (vbpf#581)
Browse files Browse the repository at this point in the history
* Only set type to packet if the width is correct
* Fix and test move operations
* Correct variable name to be offset_width

Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
dthaler authored Feb 11, 2024
1 parent 342996d commit b62f8f1
Show file tree
Hide file tree
Showing 4 changed files with 255 additions and 23 deletions.
2 changes: 1 addition & 1 deletion src/asm_parse.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ using crab::linear_expression_t;
#define ARRAY_RANGE R"_(\s*\[([-+]?\d+)\.\.\.\s*([-+]?\d+)\]?\s*)_"

#define DOT "[.]"
#define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_program)\s*)_"
#define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_programs)\s*)_"

static const std::map<std::string, Bin::Op> str_to_binop = {
{"", Bin::Op::MOV}, {"+", Bin::Op::ADD}, {"-", Bin::Op::SUB}, {"*", Bin::Op::MUL},
Expand Down
81 changes: 60 additions & 21 deletions src/crab/ebpf_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,13 @@ static linear_constraint_t neq(variable_t a, variable_t b) {
}

constexpr int MAX_PACKET_SIZE = 0xffff;

// Pointers in the BPF VM are defined to be 64 bits. Some contexts, like
// data, data_end, and meta in Linux's struct xdp_md are only 32 bit offsets
// from a base address not exposed to the program, but when a program is loaded,
// the offsets get replaced with 64-bit address pointers. However, we currently
// need to do pointer arithmetic on 64-bit numbers so for now we cap the interval
// to 32 bits.
constexpr int64_t PTR_MAX = std::numeric_limits<int32_t>::max() - MAX_PACKET_SIZE;

/** Linear constraint for a pointer comparison.
Expand Down Expand Up @@ -1906,22 +1913,32 @@ void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const

number_t addr = *maybe_addr;

// We use offsets for packet data, data_end, and meta during verification,
// but at runtime they will be 64-bit pointers. We can use the offset values
// for verification like we use map_fd's as a proxy for maps which
// at runtime are actually 64-bit memory pointers.
int offset_width = desc->end - desc->data;
if (addr == desc->data) {
inv.assign(target.packet_offset, 0);
if (width == offset_width)
inv.assign(target.packet_offset, 0);
} else if (addr == desc->end) {
inv.assign(target.packet_offset, variable_t::packet_size());
if (width == offset_width)
inv.assign(target.packet_offset, variable_t::packet_size());
} else if (addr == desc->meta) {
inv.assign(target.packet_offset, variable_t::meta_offset());
if (width == offset_width)
inv.assign(target.packet_offset, variable_t::meta_offset());
} else {
if (may_touch_ptr)
type_inv.havoc_type(inv, target_reg);
else
type_inv.assign_type(inv, target_reg, T_NUM);
return;
}
type_inv.assign_type(inv, target_reg, T_PACKET);
inv += 4098 <= target.svalue;
inv += target.svalue <= PTR_MAX;
if (width == offset_width) {
type_inv.assign_type(inv, target_reg, T_PACKET);
inv += 4098 <= target.svalue;
inv += target.svalue <= PTR_MAX;
}
}

void ebpf_domain_t::do_load_packet_or_shared(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr,
Expand Down Expand Up @@ -2733,30 +2750,52 @@ void ebpf_domain_t::operator()(const Bin& bin) {
assign(dst.uvalue, src.uvalue);
havoc_offsets(bin.dst);
m_inv = type_inv.join_over_types(m_inv, src_reg, [&](NumAbsDomain& inv, type_encoding_t type) {
inv.assign(dst.type, type);

switch (type) {
case T_CTX: inv.assign(dst.ctx_offset, src.ctx_offset); break;
case T_CTX:
if (bin.is64) {
inv.assign(dst.type, type);
inv.assign(dst.ctx_offset, src.ctx_offset);
}
break;
case T_MAP:
case T_MAP_PROGRAMS: inv.assign(dst.map_fd, src.map_fd); break;
case T_PACKET: inv.assign(dst.packet_offset, src.packet_offset); break;
case T_MAP_PROGRAMS:
if (bin.is64) {
inv.assign(dst.type, type);
inv.assign(dst.map_fd, src.map_fd);
}
break;
case T_PACKET:
if (bin.is64) {
inv.assign(dst.type, type);
inv.assign(dst.packet_offset, src.packet_offset);
}
break;
case T_SHARED:
inv.assign(dst.shared_region_size, src.shared_region_size);
inv.assign(dst.shared_offset, src.shared_offset);
if (bin.is64) {
inv.assign(dst.type, type);
inv.assign(dst.shared_region_size, src.shared_region_size);
inv.assign(dst.shared_offset, src.shared_offset);
}
break;
case T_STACK:
inv.assign(dst.stack_offset, src.stack_offset);
inv.assign(dst.stack_numeric_size, src.stack_numeric_size);
if (bin.is64) {
inv.assign(dst.type, type);
inv.assign(dst.stack_offset, src.stack_offset);
inv.assign(dst.stack_numeric_size, src.stack_numeric_size);
}
break;
default: break;
default: inv.assign(dst.type, type); break;
}
});
if ((bin.dst.v != std::get<Reg>(bin.v).v) || (type_inv.get_type(m_inv, dst.type) == T_UNINIT)) {
// Only forget the destination type if we're copying from a different register,
// or from the same uninitialized register.
havoc(dst.type);
if (bin.is64) {
// Add dst.type=src.type invariant.
if ((bin.dst.v != std::get<Reg>(bin.v).v) || (type_inv.get_type(m_inv, dst.type) == T_UNINIT)) {
// Only forget the destination type if we're copying from a different register,
// or from the same uninitialized register.
havoc(dst.type);
}
type_inv.assign_type(m_inv, bin.dst, std::get<Reg>(bin.v));
}
type_inv.assign_type(m_inv, bin.dst, std::get<Reg>(bin.v));
break;
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/crab/split_dbm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1052,7 +1052,7 @@ static std::string to_string(variable_t vd, variable_t vs, const SplitDBM::Param
}

static const std::vector<std::string> type_string = {
"shared", "stack", "packet", "ctx", "number", "map_fd", "map_fd_program", "uninitialized"
"shared", "stack", "packet", "ctx", "number", "map_fd", "map_fd_programs", "uninitialized"
};

string_invariant SplitDBM::to_set() const {
Expand Down
193 changes: 193 additions & 0 deletions test-data/assign.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,21 @@ post:
- r1.uvalue=r2.uvalue
- r1.stack_numeric_size=r2.stack_numeric_size
---
test-case: 32-bit assign register stack value

pre: ["r10.type=stack", "r10.stack_offset=512"]

code:
<start>: |
w2 = r10
post:
- r2.svalue=[0, 4294967295]
- r2.svalue=r2.uvalue
- r2.uvalue=[0, 4294967295]
- r10.type=stack
- r10.stack_offset=512
---
test-case: assign register shared value

pre: ["r1.type=shared", "r1.shared_offset=0", "r1.shared_region_size=16"]
Expand All @@ -190,6 +205,22 @@ post:
- r1.svalue=r2.svalue
- r1.uvalue=r2.uvalue
---
test-case: 32-bit assign register shared value

pre: ["r1.type=shared", "r1.shared_offset=0", "r1.shared_region_size=16"]

code:
<start>: |
w2 = r1
post:
- r1.type=shared
- r1.shared_offset=0
- r1.shared_region_size=16
- r2.svalue=[0, 4294967295]
- r2.uvalue=[0, 4294967295]
- r2.svalue=r2.uvalue
---
test-case: assign register combination value

pre: ["r1.type=[-1,0]", "r1.shared_offset=0", "r1.shared_region_size=16", "r1.stack_offset=500", "r1.stack_numeric_size=16"]
Expand Down Expand Up @@ -229,3 +260,165 @@ post:
- r1.uvalue=[1, 2147418112]
- r2.type=packet
- r2.svalue=[4098, 2147418112]
---
test-case: 16-bit indirect assignment from context

pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]

code:
<start>: |
r2 = *(u16 *)(r1 + 4)
post:
- r1.ctx_offset=0
- r1.type=ctx
- r1.svalue=[1, 2147418112]
- r1.uvalue=[1, 2147418112]
---
test-case: 64-bit indirect assignment from context

pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]

code:
<start>: |
r2 = *(u64 *)(r1 + 4)
post:
- r1.ctx_offset=0
- r1.type=ctx
- r1.svalue=[1, 2147418112]
- r1.uvalue=[1, 2147418112]
---
test-case: assign register packet value

pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]

code:
<start>: |
r1 = r2
post:
- packet_size=r1.packet_offset
- r1.type=packet
- r1.svalue=[4098, 2147418112]
- packet_size=r2.packet_offset
- r2.type=packet
- r2.svalue=[4098, 2147418112]
- r1.packet_offset=r2.packet_offset
- r1.svalue=r2.svalue
- r1.uvalue=r2.uvalue
---
test-case: 32-bit assign register packet value

pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]

code:
<start>: |
w1 = r2
post:
- r1.svalue=[0, 4294967295]
- r1.uvalue=[0, 4294967295]
- r1.svalue=r1.uvalue
- packet_size=r2.packet_offset
- r2.type=packet
- r2.svalue=[4098, 2147418112]
---
test-case: assign register context value

pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]

code:
<start>: |
r2 = r1
post:
- r1.ctx_offset=0
- r1.type=ctx
- r1.svalue=[1, 2147418112]
- r1.uvalue=[1, 2147418112]
- r2.ctx_offset=0
- r2.type=ctx
- r2.svalue=[1, 2147418112]
- r2.uvalue=[1, 2147418112]
- r1.svalue=r2.svalue
- r1.uvalue=r2.uvalue
---
test-case: 32-bit assign register context value

pre: ["r1.ctx_offset=0", "r1.type=ctx", "r1.svalue=[1, 2147418112]", "r1.uvalue=[1, 2147418112]"]

code:
<start>: |
w2 = r1
post:
- r1.ctx_offset=0
- r1.type=ctx
- r1.svalue=[1, 2147418112]
- r1.uvalue=[1, 2147418112]
- r2.svalue=[1, 2147418112]
- r2.uvalue=[1, 2147418112]
- r2.svalue=r2.uvalue
---
test-case: assign register map value

pre: ["r1.type=map_fd", "r1.map_fd=1"]

code:
<start>: |
r2 = r1
post:
- r1.map_fd=1
- r1.type=map_fd
- r2.map_fd=1
- r2.type=map_fd
- r1.svalue=r2.svalue
- r1.uvalue=r2.uvalue
---
test-case: 32-bit assign register map value

pre: ["r1.type=map_fd", "r1.map_fd=1"]

code:
<start>: |
w2 = r1
post:
- r1.map_fd=1
- r1.type=map_fd
- r2.svalue=[0, 4294967295]
- r2.uvalue=[0, 4294967295]
- r2.svalue=r2.uvalue
---
test-case: assign register map programs value

pre: ["r1.type=map_fd_programs", "r1.map_fd=1"]

code:
<start>: |
r2 = r1
post:
- r1.map_fd=1
- r1.type=map_fd_programs
- r2.map_fd=1
- r2.type=map_fd_programs
- r1.svalue=r2.svalue
- r1.uvalue=r2.uvalue
---
test-case: 32-bit assign register map programs value

pre: ["r1.type=map_fd_programs", "r1.map_fd=1"]

code:
<start>: |
w2 = r1
post:
- r1.map_fd=1
- r1.type=map_fd_programs
- r2.svalue=[0, 4294967295]
- r2.uvalue=[0, 4294967295]
- r2.svalue=r2.uvalue

0 comments on commit b62f8f1

Please sign in to comment.