[ranges] Add wrap-around support for infer-isolated, improve disjoint ranges #3

Author: SanWieb

analyzer/analysis/rangeAnalysis.py

@@ -42,7 +42,7 @@ def get_ast_ranges(constraints, ast : claripy.BV):
 
     # We calculate the min and max once
     s = claripy.Solver(timeout=global_config["Z3Timeout"])
-    s.constraints = constraints
+    s.constraints = constraints.copy()
     ast_min = s.min(ast)
     ast_max = s.max(ast)
 

analyzer/analysis/range_strategies/find_constraints_bounds.py

@@ -50,30 +50,45 @@ def find_range(self, constraints, ast : claripy.ast.bv.BVS,
         if ast_min == ast_max:
             return self.infer_isolated_strategy.find_range([], ast, ast_min, ast_max)
 
-        # print(f"min:{ast_min}     max:{ast_max}")
+
         try:
             sat_ranges = _find_sat_distribution(constraints, ast, ast_min, ast_max, stride=1)
         except claripy.ClaripyZ3Error as e:
             # timeout
             return None
 
+        # --------- One non-satisfiable range
+
         if sat_ranges != None and len(sat_ranges) == 1:
-            # It is a full range, we can treat it as isolated
-            return self.infer_isolated_strategy.find_range([], ast, sat_ranges[0][0], sat_ranges[0][1])
+            # We have one non-satisfiable range, so we can try to treat it as
+            # isolated
+
+            r = self.infer_isolated_strategy.find_range([], ast, sat_ranges[0][0], sat_ranges[0][1])
+
+            if sat_ranges[0][0] > sat_ranges[0][1]:
+                # The range wraps around, we have to be sure that the AST range is
+                # a simple strided range, otherwise we get two separate disjoint ranges
+                # which we cannot describe in our range (e.g., [ast != 0xf, ast <= 0xffff])
+                if r.and_mask != None or r.or_mask != None or \
+                    ast_max != ((1 << ast.size()) - 1 - (r.stride - 1)) or ast_min != 0:
+
+                    # We have a complex range thus fail (e.g., masking is performed)
+                    return None
+
+            return r
 
         # --------- Signed range
         if ast_min == 0 and ast_max == (2**ast.size()) - 1:
             s = claripy.Solver(timeout=global_config["Z3Timeout"])
             new_min = (1 << (ast.size() - 1))
-            s.constraints = constraints + [(ast > new_min)]
+            s.constraints = constraints + [(ast >= new_min)]
             upper_ast_min = s.min(ast)
             upper_ast_max = s.max(ast)
             s = claripy.Solver(timeout=global_config["Z3Timeout"])
-            s.constraints = constraints + [ast <= new_min]
+            s.constraints = constraints + [ast < new_min]
             lower_ast_min = s.min(ast)
             lower_ast_max = s.max(ast)
 
-            # print(f" new_min:{hex(new_min)} upper_min: {hex(upper_ast_min)}   upper_max: {hex(upper_ast_max)}    lower_min: {hex(lower_ast_min)}    lower_max: {hex(lower_ast_max)}")
 
             if lower_ast_min == 0 and upper_ast_max == (2**ast.size()) - 1:
                 # treat this as a single range that wraps around ( min > max )
@@ -124,8 +139,7 @@ def _find_sat_distribution(constraints, ast, start, end, stride = 1):
             return [(start, end)]
 
         # Range with a "hole"
-        # print(f"Range: {[(value+1, value-1)]}")
-        return [value+1, value-1]
+        return [(value+1, value-1)]
 
     # TODO: Double check the validity of the code below
     return None

analyzer/analysis/range_strategies/find_masking.py

@@ -24,7 +24,7 @@ def find_range(self, constraints, ast : claripy.ast.bv.BVS,
 
         entropy, and_mask, or_mask = _find_entropy(s, ast, ast_max)
 
-        return range_complex(ast_min, ast_max, False, entropy, and_mask, or_mask)
+        return range_complex(ast_min, ast_max, ast.size(), False, entropy, and_mask, or_mask)
 
 def _find_entropy(s : claripy.Solver, ast : claripy.BV, ast_max : int):
 

analyzer/analysis/range_strategies/infer_isolated.py

@@ -20,7 +20,6 @@ def find_range(self, constraints, ast : claripy.ast.bv.BVS,
                    ast_min : int = None, ast_max : int = None):
 
         # We only support isolated ranges
-
         if constraints:
             return None
 
@@ -34,34 +33,73 @@ def find_range(self, constraints, ast : claripy.ast.bv.BVS,
                 ast_max = s.max(ast)
 
         if ast.depth == 1:
-            return range_simple(ast_min, ast_max, 1, True)
+            return range_simple(ast_min, ast_max, ast.size(), 1, True)
 
         range_map = get_range_map_from_ast(ast)
 
         if range_map.unknown:
-            return None
+
+            # We try an extra optimization: separating the concrete value
+            # from addition. This covers cases like:
+            # 0xffffffff81000000 + <BV32 AST >
+            # get_range_map_from_ast() cannot handle 'overflows', so we
+            # split the AST and add the concrete value manually to the range.
+            if ast.op == '__add__' and any(not arg.symbolic for arg in ast.args):
+
+                concrete_value =  next(arg for arg in ast.args if not arg.symbolic).args[0]
+                sub_ast = sum([arg for arg in ast.args if arg.symbolic])
+
+                range_map = get_range_map_from_ast(sub_ast)
+
+                if range_map.unknown:
+                    return None
+
+                range_map = range_map.switch_to_stride_mode()
+
+                if range_map.unknown:
+                    return None
+
+                s = claripy.Solver(timeout=global_config["Z3Timeout"])
+                sub_ast_min = s.min(sub_ast)
+                sub_ast_max = s.max(sub_ast)
+
+                isolated_ast_min = sub_ast_min + concrete_value
+                isolated_ast_max = sub_ast_max + concrete_value
+
+                # handle overflows
+                isolated_ast_min &= (1 << ast.size()) - 1
+                isolated_ast_max &= (1 << ast.size()) - 1
+
+                if isolated_ast_min - isolated_ast_max == range_map.stride:
+                    isolated_ast_min = s.min(ast)
+                    isolated_ast_max = s.max(ast)
+
+                # incorporate non-isolated min and max, only adjust if they are
+                # tighter
+                # Note: Conditions hold for both normal and disjoint ranges
+                ast_min = ast_min if isolated_ast_min < ast_min else isolated_ast_min
+                ast_max = ast_max if isolated_ast_max > ast_max else isolated_ast_max
+
+            else:
+                return None
 
 
         if range_map.stride_mode:
-            return range_simple(ast_min, ast_max, range_map.stride, isolated=True)
+            return range_simple(ast_min, ast_max, ast.size(), range_map.stride, isolated=True)
 
         else:
-            return range_complex(ast_min, ast_max, True, None, range_map.and_mask, range_map.or_mask, True)
+            return range_complex(ast_min, ast_max, ast.size(), True, None, range_map.and_mask, range_map.or_mask, True)
 
 
 def is_linear_mask(and_mask, or_mask):
 
     mask = and_mask & ~or_mask
 
-    # print(bin(mask))
-
     highest_bit = mask.bit_length()
     lowest_bit = (mask & -mask).bit_length() - 1
 
     stride_mask = (2 ** highest_bit - 1) & ~(2 ** lowest_bit - 1)
 
-    # print(bin(stride_mask))
-
     return mask == stride_mask
 
 @dataclass

analyzer/analysis/range_strategies/small_set.py

@@ -16,7 +16,7 @@ def _list_to_stride_range(numbers : list):
         if numbers[i] + stride != numbers[i+1]:
             return None
 
-    return AstRange(min=numbers[0] , max=numbers[-1],
+    return AstRange(min=numbers[0] , max=numbers[-1], ast_size=0,
                     exact=True, isolated=True,
                     intervals=[Interval(numbers[0], numbers[-1], stride)])
 

analyzer/shared/ranges.py

@@ -49,10 +49,18 @@ def stride(self):
             # TODO: Handle multiple intervals
             None
 
-    def __init__(self, min, max, exact, entropy=None, isolated=False, and_mask=None, or_mask=None, values=[], intervals=[]):
+    def __init__(self, min, max, ast_size, exact, entropy=None, isolated=False, and_mask=None, or_mask=None, values=[], intervals=[]):
         self.min = min
         self.max = max
-        self.window = max - min
+        self.__ast_size = ast_size
+
+        if min <= max:
+            self.window = max - min
+        else:
+            assert(ast_size > 0)
+            # wrap around range
+            # window = 0:max + min:ast_size
+            self.window = ((1 << ast_size) - 1) - (min - 1) + max
 
         self.entropy = entropy
         self.isolated = isolated
@@ -102,10 +110,11 @@ def to_string(self):
             return ",".join([hex(i) for i in self.values]) + f" Exact: {self.exact}"
 
     def copy(self):
-        return AstRange(min=self.min, max=self.max, exact=self.exact,
-                        entropy=self.entropy, isolated=self.isolated,
-                        and_mask=self.and_mask, or_mask=self.or_mask,
-                        values=self.values, intervals=self.intervals)
+        return AstRange(min=self.min, max=self.max, ast_size=self.__ast_size,
+                        exact=self.exact, entropy=self.entropy,
+                        isolated=self.isolated, and_mask=self.and_mask,
+                        or_mask=self.or_mask, values=self.values,
+                        intervals=self.intervals)
 
     def __str__(self):
 
@@ -118,11 +127,11 @@ def __repr__(self):
 def range_static(value, isolated):
     interval = Interval(min=value, max=value+1, stride=1)
 
-    return AstRange(min=value, max=value, exact=True, entropy=0, isolated=isolated, intervals=[interval])
+    return AstRange(min=value, max=value, ast_size=0, exact=True, entropy=0, isolated=isolated, intervals=[interval])
 
 
-def range_simple(min, max, stride, isolated):
-    return AstRange(min=min, max=max, exact=True, isolated=isolated, intervals=[Interval(min, max, stride)])
+def range_simple(min, max, ast_size, stride, isolated):
+    return AstRange(min=min, max=max, ast_size=ast_size, exact=True, isolated=isolated, intervals=[Interval(min, max, stride)])
 
 
 def get_stride_from_mask(and_mask, or_mask):
@@ -136,7 +145,7 @@ def get_stride_from_mask(and_mask, or_mask):
     return 2 ** lowest_bit
 
 
-def range_complex(min, max, exact, entropy, and_mask, or_mask, isolated=False):
+def range_complex(min, max, ast_size, exact, entropy, and_mask, or_mask, isolated=False):
     stride = get_stride_from_mask(and_mask, or_mask)
 
     highest_bit = max.bit_length()
@@ -151,7 +160,7 @@ def range_complex(min, max, exact, entropy, and_mask, or_mask, isolated=False):
         # We dont need the mask, stride is enough
         and_mask = None
 
-    return AstRange(min=min, max=max,exact=exact, entropy=entropy,
-                    isolated=isolated, and_mask=and_mask, or_mask=or_mask,
-                    intervals=[Interval(min, max, stride)])
+    return AstRange(min=min, max=max, ast_size=ast_size, exact=exact,
+                    entropy=entropy, isolated=isolated, and_mask=and_mask,
+                    or_mask=or_mask, intervals=[Interval(min, max, stride)])
 

analyzer/shared/transmission.py

@@ -165,8 +165,8 @@ def to_dict(self):
             ('branches', [str(x) for x in self.branches]),
             ('constraints', [str(x) for x in self.constraints]),
             ('requirements', self.requirements.to_dict()),
-            ('range', ranges.AstRange(0,0,False).to_dict() if self.range == None else self.range.to_dict()),
-            ('range_w_branches', ranges.AstRange(0,0,False).to_dict() if self.range_with_branches == None else self.range_with_branches.to_dict()),
+            ('range', ranges.AstRange(0,0,0,False).to_dict() if self.range == None else self.range.to_dict()),
+            ('range_w_branches', ranges.AstRange(0,0,0,False).to_dict() if self.range_with_branches == None else self.range_with_branches.to_dict()),
             ('control', str(self.control)),
             ('n_dependent_loads', str(self.max_load_depth))
         ]

tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000004_c881501a-57ea-45fb-8d28-450f6aa76dd6.asm renamed to tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000004_7ffd1082-0000-4995-b313-dbcc2c9ced70.asm

@@ -9,7 +9,7 @@
 4000019  jmp     0x400dead
 
 ------------------------------------------------
-uuid: c881501a-57ea-45fb-8d28-450f6aa76dd6
+uuid: 7ffd1082-0000-4995-b313-dbcc2c9ced70
 
 Secret Address:
   - Expr: <BV64 rdi>
@@ -26,7 +26,7 @@ Base:
   - Independent Range: 0xffffffffffffffe0
 Transmission:
   - Expr: <BV64 0xffffffffffffffe0 + (0#48 .. LOAD_16[<BV64 rdi>]_20)>
-  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: False
+  - Range: (0xffffffffffffffe0,0xffdf, 0x1) Exact: True
 
 Register Requirements: {<BV64 rdi>}
 Constraints: []

tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000008_ccb61920-0524-4704-a156-d5872324e38d.asm renamed to tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000008_8fb91631-205c-4606-8a75-cf830f7f8b6d.asm

@@ -2,14 +2,14 @@
          alias_type_1:
 4000000  movzx   r8d, word ptr [rdi] ; {Attacker@rdi} > {Secret@0x4000000}
 4000004  mov     rcx, qword ptr [r8-0x20]
-4000008  mov     r10, qword ptr [rdi+r8+0x50] ; {Attacker@rdi, Secret@0x4000000} > TRANSMISSION
+4000008  mov     r10, qword ptr [rdi+r8+0x50] ; {Secret@0x4000000, Attacker@rdi} > TRANSMISSION
 400000d  mov     r11, qword ptr [rsi]
 4000010  movzx   r9d, word ptr [r11]
 4000014  mov     rax, qword ptr [r11+r9+0x20]
 4000019  jmp     0x400dead
 
 ------------------------------------------------
-uuid: ccb61920-0524-4704-a156-d5872324e38d
+uuid: 8fb91631-205c-4606-8a75-cf830f7f8b6d
 
 Secret Address:
   - Expr: <BV64 rdi>

tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000010_853ce41f-58d0-4a94-85f5-930a5bfa6123.asm renamed to tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000010_d6dc9608-50db-4823-baa6-c48a912b8a15.asm

@@ -9,7 +9,7 @@
 4000019  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 853ce41f-58d0-4a94-85f5-930a5bfa6123
+uuid: d6dc9608-50db-4823-baa6-c48a912b8a15
 
 Secret Address:
   - Expr: <BV64 rsi>

tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000014_3924305c-37d3-48b0-ae6a-fd42e6a02b39.asm renamed to tests/test-cases/alias_type_1/ref-asm/gadget_alias_type_1_0x4000014_830a85c4-0c4f-4245-b16d-719531b0e796.asm

@@ -5,11 +5,11 @@
 4000008  mov     r10, qword ptr [rdi+r8+0x50]
 400000d  mov     r11, qword ptr [rsi] ; {Attacker@rsi} > {Secret@0x400000d}
 4000010  movzx   r9d, word ptr [r11] ; {Attacker@0x400000d} > {Attacker@0x4000010}
-4000014  mov     rax, qword ptr [r11+r9+0x20] ; {Secret@0x400000d, Attacker@0x4000010} > TRANSMISSION
+4000014  mov     rax, qword ptr [r11+r9+0x20] ; {Attacker@0x4000010, Secret@0x400000d} > TRANSMISSION
 4000019  jmp     0x400dead
 
 ------------------------------------------------
-uuid: 3924305c-37d3-48b0-ae6a-fd42e6a02b39
+uuid: 830a85c4-0c4f-4245-b16d-719531b0e796
 
 Secret Address:
   - Expr: <BV64 rsi>

tests/test-cases/alias_type_1/ref-output/reasoner_data.txt

@@ -208,7 +208,7 @@
 +-----------+------------------------+------------------------+---------------------------+---------------------------+-----------------------------+----------------------------+--------------------------+-----------------------------------+-----------------------------------+--------------------------------------+--------------------------------------+----------------------------------------+---------------------------------------+-------------------------------------+
 |    pc     | transmission_range_min | transmission_range_max | transmission_range_window | transmission_range_stride | transmission_range_and_mask | transmission_range_or_mask | transmission_range_exact | transmission_range_w_branches_min | transmission_range_w_branches_max | transmission_range_w_branches_window | transmission_range_w_branches_stride | transmission_range_w_branches_and_mask | transmission_range_w_branches_or_mask | transmission_range_w_branches_exact |
 +-----------+------------------------+------------------------+---------------------------+---------------------------+-----------------------------+----------------------------+--------------------------+-----------------------------------+-----------------------------------+--------------------------------------+--------------------------------------+----------------------------------------+---------------------------------------+-------------------------------------+
-| 0x4000004 | 0                      | 18446744073709551615   | 18446744073709551615      | 1                         |                             |                            | False                    | 0                                 | 18446744073709551615              | 18446744073709551615                 | 1                                    |                                        |                                       | False                               |
+| 0x4000004 | 18446744073709551584   | 65503                  | 65535                     | 1                         |                             |                            | True                     | 18446744073709551584              | 65503                             | 65535                                | 1                                    |                                        |                                       | True                                |
 | 0x4000008 | 0                      | 18446744073709551615   | 18446744073709551615      | 1                         |                             |                            | True                     | 0                                 | 18446744073709551615              | 18446744073709551615                 | 1                                    |                                        |                                       | True                                |
 | 0x4000010 | 0                      | 18446744073709551615   | 18446744073709551615      | 1                         |                             |                            | True                     | 0                                 | 18446744073709551615              | 18446744073709551615                 | 1                                    |                                        |                                       | True                                |
 | 0x4000014 | 0                      | 18446744073709551615   | 18446744073709551615      | 1                         |                             |                            | True                     | 0                                 | 18446744073709551615              | 18446744073709551615                 | 1                                    |                                        |                                       | True                                |