diff --git a/src/assertions.cpp b/src/assertions.cpp index 6904c2a0f..fcc922184 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -168,8 +168,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}); 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: []