Merge pull request #23 from vusec/fix-stride-multiplication

[range-analysis] Bug fix: stride detection for multiplication
vusec · Apr 25, 2024 · 0cfd532 · 0cfd532
2 parents 5239b6f + e5f51c8
commit 0cfd532
Show file tree

Hide file tree

Showing 11 changed files with 104 additions and 63 deletions.
diff --git a/analyzer/analysis/range_strategies/infer_isolated.py b/analyzer/analysis/range_strategies/infer_isolated.py
@@ -14,6 +14,8 @@
 
 l = get_logger("InferIsolated")
 
+debug = False
+
 class RangeStrategyInferIsolated(RangeStrategy):
 
     def find_range(self, constraints, ast : claripy.ast.bv.BVS,
@@ -162,13 +164,18 @@ def concrete_add(self, value, int_length):
 
     def concrete_mul(self, value, int_length):
 
+        # Check if we are in mask mode & multiplication is power of 2
+        if (not self.stride_mode) and (value != 0) and (value & (value-1) == 0):
+            # Power of two
+            return self.shift_left(value.bit_length() - 1, int_length)
+
+
         if (self.and_mask * value) >= (2 ** int_length):
             # mul has a overflow, we are not gonna try it
             return unknown_range()
 
-        # two based shift
+        # Multiply stride by multiplication
         new_map = self.switch_to_stride_mode()
-
         if not new_map.unknown:
             new_map.stride = new_map.stride * value
 
@@ -437,26 +444,24 @@ def op_sub(ast, range_maps):
 
 def op_mul(ast, range_maps):
 
-    non_full_ranges = []
+    base_map = None
     concrete_ast = None
 
     for idx, map in enumerate(range_maps):
+        # concrete value
         if not map:
             if concrete_ast != None:
                 concrete_ast = concrete_ast * ast.args[idx]
             else:
                 concrete_ast = ast.args[idx]
 
-        elif map.is_full_range(ast.length):
-            return map
-
+        # symbolic value
+        elif base_map == None:
+            base_map = range_maps[idx]
         else:
-            non_full_ranges.append(map)
-
-    if len(non_full_ranges) == 1:
-        base_map = non_full_ranges[0]
-
-        return base_map.concrete_mul(concrete_ast.args[0], ast.length)
+            # Mask by symbolic variable, we can't know the range
+            return unknown_range()
+    return base_map.concrete_mul(concrete_ast.args[0], ast.length)
 
 def op_if(ast, range_maps):
     # if arg0 then arg1 else arg2
@@ -522,8 +527,13 @@ def get_range_map_from_ast(ast : claripy.ast.bv.BVS):
             return unknown_range()
 
         if ast.op in operators:
+            if debug:
+                print(f"OP: {ast.op} AST: {ast} MAPS: {args_range_maps}")
+
             new_map = operators[ast.op](ast, args_range_maps)
 
+            if debug:
+                print(f"OUT: {new_map}")
 
             return new_map
 

diff --git a/..._8b880656-118d-4047-83e9-162d87f8dfdd.asm → ..._2a65705b-77ee-4a68-89a4-1cb606719908.asm b/..._8b880656-118d-4047-83e9-162d87f8dfdd.asm → ..._2a65705b-77ee-4a68-89a4-1cb606719908.asm
@@ -19,7 +19,7 @@
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 8b880656-118d-4047-83e9-162d87f8dfdd
+uuid: 2a65705b-77ee-4a68-89a4-1cb606719908
 transmitter: TransmitterType.LOAD
 
 Secret Address:
@@ -39,7 +39,7 @@ Transmission:
   - Expr: <BV64 ((0#6 .. LOAD_64[<BV64 rsi>]_21[57:0]) << 0x6) + ((0#6 .. LOAD_64[<BV64 rdi>]_20[57:0]) << 0x6)>
   - Range: (0x0,0xffffffffffffffc0, 0x40) Exact: False
 
-Register Requirements: {<BV64 rsi>, <BV64 rdi>}
+Register Requirements: {<BV64 rdi>, <BV64 rsi>}
 Constraints: []
 Branches: []
 ------------------------------------------------
diff --git a/..._5e4bb1f5-c302-469f-94c2-b931a9a6b29d.asm → ..._d666c1c2-a045-4e38-a2fa-44d5cf0ad0bb.asm b/..._5e4bb1f5-c302-469f-94c2-b931a9a6b29d.asm → ..._d666c1c2-a045-4e38-a2fa-44d5cf0ad0bb.asm
@@ -4,7 +4,7 @@
 4000003  mov     r9, qword ptr [rsi] ; {Attacker@rsi} -> {Secret@0x4000003}
 4000006  add     r9, r8
 4000009  shl     r9, 0x6
-400000d  mov     r10, qword ptr [r9] ; {Attacker@0x4000000, Secret@0x4000003} -> TRANSMISSION
+400000d  mov     r10, qword ptr [r9] ; {Secret@0x4000003, Attacker@0x4000000} -> TRANSMISSION
 4000010  mov     r8, qword ptr [rdi]
 4000013  mov     r9, qword ptr [rsi]
 4000016  mov     rax, 0x8
@@ -19,7 +19,7 @@
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 5e4bb1f5-c302-469f-94c2-b931a9a6b29d
+uuid: d666c1c2-a045-4e38-a2fa-44d5cf0ad0bb
 transmitter: TransmitterType.LOAD
 
 Secret Address:
@@ -39,7 +39,7 @@ Transmission:
   - Expr: <BV64 ((0#6 .. LOAD_64[<BV64 rsi>]_21[57:0]) << 0x6) + ((0#6 .. LOAD_64[<BV64 rdi>]_20[57:0]) << 0x6)>
   - Range: (0x0,0xffffffffffffffc0, 0x40) Exact: False
 
-Register Requirements: {<BV64 rsi>, <BV64 rdi>}
+Register Requirements: {<BV64 rdi>, <BV64 rsi>}
 Constraints: []
 Branches: []
 ------------------------------------------------
diff --git a/..._269dd679-b3e3-4a86-a67c-8cff10cd6602.asm → ..._19d1a0de-64f2-4cbd-916b-9b5a40e8d942.asm b/..._269dd679-b3e3-4a86-a67c-8cff10cd6602.asm → ..._19d1a0de-64f2-4cbd-916b-9b5a40e8d942.asm
@@ -19,15 +19,15 @@
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 269dd679-b3e3-4a86-a67c-8cff10cd6602
+uuid: 19d1a0de-64f2-4cbd-916b-9b5a40e8d942
 transmitter: TransmitterType.LOAD
 
 Secret Address:
   - Expr: <BV64 rdi>
   - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
 Transmitted Secret:
   - Expr: <BV64 0x8 * LOAD_64[<BV64 rdi>]_23>
-  - Range: (0x0,0xfffffffffffffff8, 0x1) Exact: True
+  - Range: (0x0,0xfffffffffffffff8, 0x8) Exact: True
   - Spread: 3 - 63
   - Number of Bits Inferable: 61
 Base:
@@ -37,7 +37,7 @@ Base:
   - Independent Range: None
 Transmission:
   - Expr: <BV64 0x8 * LOAD_64[<BV64 rdi>]_23>
-  - Range: (0x0,0xfffffffffffffff8, 0x1) Exact: True
+  - Range: (0x0,0xfffffffffffffff8, 0x8) Exact: True
 
 Register Requirements: {<BV64 rdi>}
 Constraints: []

diff --git a/..._45c04779-5b26-43f6-922c-e1bcebf15e52.asm → ..._0abb73b8-972a-4bca-9574-b0d2e3bae122.asm b/..._45c04779-5b26-43f6-922c-e1bcebf15e52.asm → ..._0abb73b8-972a-4bca-9574-b0d2e3bae122.asm
@@ -12,22 +12,22 @@
 4000020  mov     r11, qword ptr [rax]
 4000023  mov     rax, r8
 4000026  mul     r9
-4000029  mov     r12, qword ptr [rax] ; {Secret@0x4000010, Attacker@0x4000013} -> TRANSMISSION
+4000029  mov     r12, qword ptr [rax] ; {Attacker@0x4000013, Secret@0x4000010} -> TRANSMISSION
 400002c  mov     rax, r8
 400002f  mul     rdi
 4000032  mov     r13, qword ptr [rax]
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 45c04779-5b26-43f6-922c-e1bcebf15e52
+uuid: 0abb73b8-972a-4bca-9574-b0d2e3bae122
 transmitter: TransmitterType.LOAD
 
 Secret Address:
   - Expr: <BV64 rdi>
   - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
 Transmitted Secret:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * LOAD_64[<BV64 rsi>]_24>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
   - Spread: 0 - 63
   - Number of Bits Inferable: 64
 Base:
@@ -37,9 +37,9 @@ Base:
   - Independent Range: None
 Transmission:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * LOAD_64[<BV64 rsi>]_24>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
 
-Register Requirements: {<BV64 rsi>, <BV64 rdi>}
+Register Requirements: {<BV64 rdi>, <BV64 rsi>}
 Constraints: []
 Branches: []
 ------------------------------------------------
diff --git a/..._32632e73-cd9e-4600-93ec-f0b7e44db874.asm → ..._f37b0bbb-184a-4ecf-a514-926bbc5b61f9.asm b/..._32632e73-cd9e-4600-93ec-f0b7e44db874.asm → ..._f37b0bbb-184a-4ecf-a514-926bbc5b61f9.asm
@@ -19,15 +19,15 @@
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 32632e73-cd9e-4600-93ec-f0b7e44db874
+uuid: f37b0bbb-184a-4ecf-a514-926bbc5b61f9
 transmitter: TransmitterType.LOAD
 
 Secret Address:
   - Expr: <BV64 rsi>
   - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
 Transmitted Secret:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * LOAD_64[<BV64 rsi>]_24>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
   - Spread: 0 - 63
   - Number of Bits Inferable: 64
 Base:
@@ -37,9 +37,9 @@ Base:
   - Independent Range: None
 Transmission:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * LOAD_64[<BV64 rsi>]_24>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
 
-Register Requirements: {<BV64 rsi>, <BV64 rdi>}
+Register Requirements: {<BV64 rdi>, <BV64 rsi>}
 Constraints: []
 Branches: []
 ------------------------------------------------
diff --git a/..._15d5aa98-c42f-49c4-9c8c-ce4cb0b6cedc.asm → ..._aeb9ca0a-beb3-4ca3-b42e-acc5dc408d55.asm b/..._15d5aa98-c42f-49c4-9c8c-ce4cb0b6cedc.asm → ..._aeb9ca0a-beb3-4ca3-b42e-acc5dc408d55.asm
@@ -19,15 +19,15 @@
 4000035  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 15d5aa98-c42f-49c4-9c8c-ce4cb0b6cedc
+uuid: aeb9ca0a-beb3-4ca3-b42e-acc5dc408d55
 transmitter: TransmitterType.LOAD
 
 Secret Address:
   - Expr: <BV64 rdi>
   - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
 Transmitted Secret:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * rdi>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
   - Spread: 0 - 63
   - Number of Bits Inferable: 64
 Base:
@@ -37,7 +37,7 @@ Base:
   - Independent Range: None
 Transmission:
   - Expr: <BV64 LOAD_64[<BV64 rdi>]_23 * rdi>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
 
 Register Requirements: {<BV64 rdi>}
 Constraints: []

diff --git a/tests/test-cases/complex_transmission/ref-output/out.txt b/tests/test-cases/complex_transmission/ref-output/out.txt
@@ -57,6 +57,6 @@ Found 2 exploitable gadgets!
 [-] Performing exploitability analysis including branch constraints...
 Found 2 exploitable gadgets!
 [-] Performing exploitability analysis assuming the SLAM covert channel...
-Found 4 exploitable gadgets!
+Found 0 exploitable gadgets!
 [-] Saving to gadgets-reasoned.csv
 [-] Done!