Havoc register if truncating non-number

Signed-off-by: Alan Jowett <[email protected]>
vbpf · Oct 21, 2024 · c66c372 · c66c372
1 parent 4832643
commit c66c372
Show file tree

Hide file tree

Showing 3 changed files with 363 additions and 0 deletions.
diff --git 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<int32_t>(pimm->v);
             bitwise_and(dst.svalue, dst.uvalue, std::numeric_limits<uint32_t>::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
@@ -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
@@ -0,0 +1,356 @@
+# 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:
+  <start>: |
+    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.svalue=[0, 4294967295]"
+  - "r1.svalue=r1.uvalue"
+  - "r1.type=ctx"
+  - "r1.uvalue=[0, 4294967295]"
+
+# Trigger 32-bit ALU operation without changing the value
+code:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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:
+  <start>: |
+    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)"