From ae600ccb02ab8de6422cfd08a85863f1c28a835e Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Thu, 17 Oct 2024 16:38:11 -0700 Subject: [PATCH] Havoc register if truncating non-number Signed-off-by: Alan Jowett --- src/crab/ebpf_domain.cpp | 6 + src/test/test_yaml.cpp | 1 + test-data/pointer.yaml | 357 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 364 insertions(+) create mode 100644 test-data/pointer.yaml diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index baf8c398b..7d34ba9df 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2497,6 +2497,12 @@ void ebpf_domain_t::operator()(const Bin& bin) { // Use only the low 32 bits of the value. imm = gsl::narrow_cast(pimm->v); bitwise_and(dst.svalue, dst.uvalue, std::numeric_limits::max()); + // If this is a 32-bit operation and the destination is not a number, forget everything about the register. + if (!type_inv.has_type(m_inv, bin.dst, T_NUM)) { + havoc_register(m_inv, bin.dst); + havoc_offsets(bin.dst); + havoc(dst.type); + } } switch (bin.op) { case Bin::Op::MOV: diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index ac8a0b9f5..b7fb6b4d6 100644 --- a/src/test/test_yaml.cpp +++ b/src/test/test_yaml.cpp @@ -35,6 +35,7 @@ YAML_CASE("test-data/movsx.yaml") YAML_CASE("test-data/muldiv.yaml") YAML_CASE("test-data/packet.yaml") YAML_CASE("test-data/parse.yaml") +YAML_CASE("test-data/pointer.yaml") YAML_CASE("test-data/sext.yaml") YAML_CASE("test-data/shift.yaml") YAML_CASE("test-data/stack.yaml") diff --git a/test-data/pointer.yaml b/test-data/pointer.yaml new file mode 100644 index 000000000..7d3dc969c --- /dev/null +++ b/test-data/pointer.yaml @@ -0,0 +1,357 @@ +# Copyright (c) Prevail Verifier contributors. +# SPDX-License-Identifier: MIT +--- +test-case: 32-bit pointer truncation - addition + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 += 0 + r2 = *(u32 *)(r1 + 0) + +post: [] + +messages: + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - subtraction + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 -= 0 + r2 = *(u32 *)(r1 + 0) + +post: [] + +messages: + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - multiplication + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 *= 1 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - division + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 /= 1 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - modulo + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 %= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - signed division + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 s/= 1 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - signed modulo + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 s%= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - AND + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 &= -1 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - OR + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 |= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - XOR + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 ^= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - LSH + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 <<= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - RSH + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 >>= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - ARSH + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 s>>= 0 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.uvalue=[0, 4294967295]" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type in {ctx, stack, packet, shared})" + - "1: Invalid type (valid_access(r1.offset, width=4) for read)" + +--- +test-case: 32-bit pointer truncation - NOT + +pre: + - "r1.ctx_offset=0" + - "r1.svalue=[0, 4294967295]" + - "r1.svalue=r1.uvalue" + - "r1.type=ctx" + - "r1.uvalue=[0, 4294967295]" + +# Trigger 32-bit ALU operation without changing the value +code: + : | + w1 = - w1 + w1 = - w1 + r2 = *(u32 *)(r1 + 0) + +post: + - "r1.type=ctx" + +messages: + - "0: Invalid type (r1.type == number)" + - "1: Invalid type (r1.type == number)" + - "2: Lower bound must be at least 0 (valid_access(r1.offset, width=4) for read)" + - "2: Upper bound must be at most 64 (valid_access(r1.offset, width=4) for read)"