diff --git a/src/assertions.cpp b/src/assertions.cpp index 6904c2a0f..b2258691a 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -137,6 +137,31 @@ class AssertExtractor { // no need to check for valid access, it must be a number res.emplace_back(TypeConstraint{cond.left, TypeGroup::number}); } else { + bool allow_pointers = false; + + switch (cond.op) { + case Condition::Op::EQ: allow_pointers = true; break; + case Condition::Op::NE: allow_pointers = true; break; + case Condition::Op::SET: allow_pointers = true; break; + case Condition::Op::NSET: allow_pointers = true; break; + case Condition::Op::LT: allow_pointers = true; break; + case Condition::Op::LE: allow_pointers = true; break; + case Condition::Op::GT: allow_pointers = true; break; + case Condition::Op::GE: allow_pointers = true; break; + case Condition::Op::SLT: allow_pointers = false; break; + case Condition::Op::SLE: allow_pointers = false; break; + case Condition::Op::SGT: allow_pointers = false; break; + case Condition::Op::SGE: allow_pointers = false; break; + default: assert(!"unexpected condition"); + } + + // Only permit pointer comparisons if the operation is 64-bit. + allow_pointers &= cond.is64; + + if (!allow_pointers) { + res.emplace_back(TypeConstraint{cond.left, TypeGroup::number}); + } + res.emplace_back(ValidAccess{cond.left}); // OK - map_fd is just another pointer // Anything can be compared to 0 @@ -168,8 +193,7 @@ class AssertExtractor { Imm width{static_cast(ins.access.width)}; 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_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}); @@ -242,7 +266,8 @@ class AssertExtractor { } return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; } - // For all other binary operations, the destination register must be a number and the source must either be an immediate or a number. + // For all other binary operations, the destination register must be a number and the source must either be an + // immediate or a number. default: if (const auto src = std::get_if(&ins.v)) { return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, diff --git a/src/test/ebpf_yaml.cpp b/src/test/ebpf_yaml.cpp index 56e619fb1..d6206778f 100644 --- a/src/test/ebpf_yaml.cpp +++ b/src/test/ebpf_yaml.cpp @@ -196,6 +196,9 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set& ra // Default to the machine's native endianness. options.big_endian = (std::endian::native == std::endian::big); + // Default to not assuming assertions. + options.assume_assertions = false; + for (const string& name : raw_options) { if (name == "!allow_division_by_zero") { options.allow_division_by_zero = false; @@ -209,6 +212,8 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set& ra options.big_endian = true; } else if (name == "!big_endian") { options.big_endian = false; + } else if (name == "assume_assertions") { + options.assume_assertions = true; } else { throw std::runtime_error("Unknown option: " + name); } diff --git a/test-data/jump.yaml b/test-data/jump.yaml index edc063911..e9c08805a 100644 --- a/test-data/jump.yaml +++ b/test-data/jump.yaml @@ -715,3 +715,537 @@ post: messages: - "0: Invalid type (r1.type in {number, ctx, stack, packet, shared})" + +# # Test cases for special case of comparison of not a number against a number when immediate is 0 +--- +test-case: JEQ with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 == 0 goto + r0 = 1 + : | + exit + +post: + - r0.svalue=1 + - r0.type=number + - r0.uvalue=1 + - r1.ctx_offset=0 + - r1.svalue=[1, 2147418112] + - r1.type=ctx + +messages: + - "0:2: Code is unreachable after 0:2" +--- +test-case: JNE with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 != 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0:1: Code is unreachable after 0:1" + - "2: Code is unreachable after 2" + - "2: Invalid type (r0.type == number)" + +--- +test-case: JSET with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 &== 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "2: Code is unreachable after 2" + - "2: Invalid type (r0.type == number)" + +--- +test-case: JNSET with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 &!= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "2: Code is unreachable after 2" + - "2: Invalid type (r0.type == number)" + +--- +test-case: JLT with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 < 0 goto + r0 = 1 + : | + exit + +post: + - r0.svalue=1 + - r0.type=number + - r0.uvalue=1 + - r1.ctx_offset=0 + - r1.svalue=[1, 2147418112] + - r1.type=ctx + - r1.uvalue=[0, +oo] + +messages: + - "0:2: Code is unreachable after 0:2" + +--- +test-case: JLE with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 <= 0 goto + r0 = 1 + : | + exit + +post: + - r0.svalue=1 + - r0.type=number + - r0.uvalue=1 + - r1.ctx_offset=0 + - r1.svalue=[1, 2147418112] + - r1.type=ctx + - r1.uvalue=[1, +oo] + +messages: + - "0:2: Code is unreachable after 0:2" + +--- +test-case: JGT with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 <= 0 goto + r0 = 1 + : | + exit + +post: + - r0.svalue=1 + - r0.type=number + - r0.uvalue=1 + - r1.ctx_offset=0 + - r1.svalue=[1, 2147418112] + - r1.type=ctx + - r1.uvalue=[1, +oo] + +messages: + - "0:2: Code is unreachable after 0:2" + +--- +test-case: JGE with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 <= 0 goto + r0 = 1 + : | + exit + +post: + - r0.svalue=1 + - r0.type=number + - r0.uvalue=1 + - r1.ctx_offset=0 + - r1.svalue=[1, 2147418112] + - r1.type=ctx + - r1.uvalue=[1, +oo] + +messages: + - "0:2: Code is unreachable after 0:2" + +--- +test-case: JSLT with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 s< 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSLE with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSGT with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSGE with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if r1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JEQ32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 == 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JNE32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 != 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSET32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 &== 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JNSET32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 &!= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JLT32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 < 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JLE32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 <= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JGT32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 <= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JGE32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 <= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSLT32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 s< 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSLE32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSGT32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" + +--- +test-case: JSGE32 with imm 0 and pointer +options: ["assume_assertions"] +pre: + - "r1.type=ctx" + - "r1.svalue=[1, 2147418112]" + - "r1.ctx_offset=0" + +code: + : | + if w1 s<= 0 goto + r0 = 1 + : | + exit + +post: [] + +messages: + - "0: Code is unreachable after 0" + - "0: Invalid type (r1.type == number)" diff --git a/test-data/uninit.yaml b/test-data/uninit.yaml index 397883f5d..9dcb18a44 100644 --- a/test-data/uninit.yaml +++ b/test-data/uninit.yaml @@ -495,3 +495,85 @@ post: messages: - "0: Invalid type (r5.type == number)" + +# Issue: https://github.com/vbpf/ebpf-verifier/issues/754 +# Should these tests fail? +--- +test-case: Read uninitialized stack range - aligned + +pre: + - r10.type=stack + - r10.stack_offset=512 + +code: + : | + r0 = *(u64 *)(r10 - 16) + +post: + - "r0.ctx_offset=s[496...503].ctx_offset" + - "r0.map_fd=s[496...503].map_fd" + - "r0.packet_offset=s[496...503].packet_offset" + - "r0.shared_offset=s[496...503].shared_offset" + - "r0.shared_region_size=s[496...503].shared_region_size" + - "r0.stack_numeric_size=s[496...503].stack_numeric_size" + - "r0.stack_offset=s[496...503].stack_offset" + - "r0.svalue=s[496...503].svalue" + - "r0.type=s[496...503].type" + - "r0.uvalue=s[496...503].uvalue" + - "r10.stack_offset=512" + - "r10.type=stack" + +messages: [] + +--- +test-case: Read uninitialized stack range - aligned + +pre: + - r10.type=stack + - r10.stack_offset=512 + +code: + : | + r0 = *(u64 *)(r10 - 8) + +post: + - "r0.ctx_offset=s[504...511].ctx_offset" + - "r0.map_fd=s[504...511].map_fd" + - "r0.packet_offset=s[504...511].packet_offset" + - "r0.shared_offset=s[504...511].shared_offset" + - "r0.shared_region_size=s[504...511].shared_region_size" + - "r0.stack_numeric_size=s[504...511].stack_numeric_size" + - "r0.stack_offset=s[504...511].stack_offset" + - "r0.svalue=s[504...511].svalue" + - "r0.type=s[504...511].type" + - "r0.uvalue=s[504...511].uvalue" + - "r10.stack_offset=512" + - "r10.type=stack" + +messages: [] +--- +test-case: Read uninitialized stack range - unaligned + +pre: + - r10.type=stack + - r10.stack_offset=512 + +code: + : | + r0 = *(u64 *)(r10 - 10) + +post: + - "r0.ctx_offset=s[502...509].ctx_offset" + - "r0.map_fd=s[502...509].map_fd" + - "r0.packet_offset=s[502...509].packet_offset" + - "r0.shared_offset=s[502...509].shared_offset" + - "r0.shared_region_size=s[502...509].shared_region_size" + - "r0.stack_numeric_size=s[502...509].stack_numeric_size" + - "r0.stack_offset=s[502...509].stack_offset" + - "r0.svalue=s[502...509].svalue" + - "r0.type=s[502...509].type" + - "r0.uvalue=s[502...509].uvalue" + - "r10.stack_offset=512" + - "r10.type=stack" + +messages: []