Fix load aliasing across stores.

analyzer/scanner/memory.py

@@ -90,6 +90,9 @@ def get_involved_vars(self):
     def __repr__(self) -> str:
         return f"{self.val1} == {self.val2}"
 
+    def is_symbolic(self):
+        return is_sym_expr(self.val1.sym) or is_sym_expr(self.val2.sym)
+
     def to_BV(self):
         return self.val1.to_BV() == self.val2.to_BV()
 
@@ -150,12 +153,19 @@ def get_aliases(state: angr.SimState) -> MemoryAlias:
     return filter(lambda x: isinstance(x, MemoryAlias), state.globals.values())
 
 
-def get_aliasing_loads(this: MemOp, state: angr.SimState) -> list[MemoryAlias]:
+def get_aliasing_loads(this: MemOp, state: angr.SimState, alias_store) -> list[MemoryAlias]:
     """
     Check if a load aliases with any other previous load.
     """
     aliasing_loads = []
-    for prev in get_previous_loads(state):
+    prev_loads = get_previous_loads(state)
+
+    if alias_store:
+        for p in prev_loads:
+            if p.id < alias_store.id:
+                del p
+
+    for prev in prev_loads:
         if overlaps_with(this, prev, state):
             memop1, memop2, off = get_overlap(this, prev, state)
 
@@ -205,7 +215,7 @@ def get_aliasing_store(load_addr: claripy.BV, load_size: int, state: angr.SimSta
     """
     store = None
 
-    # Get oldest store that aliases with this address.
+    # Get newest store that aliases with this address.
     for s in get_previous_stores(state):
         if not state.solver.satisfiable(extra_constraints=[load_addr != s.addr]):
             if not store or store.id < s.id:

analyzer/scanner/scanner.py

@@ -406,12 +406,15 @@ def load_hook_after(self, state: angr.SimState):
                                 op_type=memory.MemOpType.LOAD)
         self.cur_id += 1
 
-        aliases = memory.get_aliasing_loads(cur_load, state)
+        aliases = memory.get_aliasing_loads(cur_load, state, alias_store)
         for alias in aliases:
             state.globals[f"alias_{self.n_alias}"] = alias
             self.n_alias += 1
             # Add a symbolic constraint to the angr state.
             state.solver.add(alias.to_BV())
+            l.warning(f"Adding alias {alias.to_BV()}")
+            if not state.solver.satisfiable():
+                report_error(Exception(), hex(self.cur_state.addr), hex(0), error_type="ALIAS UNSAT")
 
 
         # Save this load in the angr state.

tests/test-cases/nested_calls/Makefile

@@ -0,0 +1,8 @@
+all: gadget
+.PHONY: clean
+
+gadget: gadget.s
+	cc -g -O0 -c gadget.s -o gadget
+
+clean:
+	rm -f -r gadget output asm gadgets.csv gadgets-reasoned.csv

tests/test-cases/nested_calls/gadget.s

@@ -0,0 +1,18 @@
+.intel_syntax noprefix
+
+nested_calls:
+        call    target_1 # store at rsp - 0x8
+        call    target_2 # store at rsp - 0x8
+
+        mov    r8, QWORD PTR [rdi]
+        movzx  r9, WORD PTR [rdi]
+        mov    r10, QWORD PTR [r9 + 0xffffffff81000000] # <<< TRANSMISSION
+
+        jmp    0xdead
+
+target_1:
+        ret  # load at rsp - 0x8
+
+target_2:
+        ret # load at rsp - 0x8
+            # Should not alias with the first ret

tests/test-cases/nested_calls/ref-asm/gadget_nested_calls_0x4000011_41558b82-e604-4142-8b02-05dde89d04e0.asm

@@ -0,0 +1,38 @@
+----------------- TRANSMISSION -----------------
+         nested_calls:
+4000000  call    target_1 ; Taken   <Bool True>
+         target_1:
+400001d  ret      ; Taken   <Bool True>
+4000005  call    target_2 ; Taken   <Bool True>
+         target_2:
+400001e  ret      ; Taken   <Bool True>
+400000a  mov     r8, qword ptr [rdi]
+400000d  movzx   r9, word ptr [rdi] ; {Attacker@rdi} -> {Secret@0x400000d}
+4000011  mov     r10, qword ptr [r9-0x7f000000] ; {Secret@0x400000d} -> TRANSMISSION
+4000018  jmp     0x400dead
+
+------------------------------------------------
+uuid: 41558b82-e604-4142-8b02-05dde89d04e0
+transmitter: TransmitterType.LOAD
+
+Secret Address:
+  - Expr: <BV64 rdi>
+  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
+Transmitted Secret:
+  - Expr: <BV64 0#48 .. LOAD_16[<BV64 rdi>]_27>
+  - Range: (0x0,0xffff, 0x1) Exact: True
+  - Spread: 0 - 15
+  - Number of Bits Inferable: 16
+Base:
+  - Expr: <BV64 0xffffffff81000000>
+  - Range: 0xffffffff81000000
+  - Independent Expr: <BV64 0xffffffff81000000>
+  - Independent Range: 0xffffffff81000000
+Transmission:
+  - Expr: <BV64 0xffffffff81000000 + (0#48 .. LOAD_16[<BV64 rdi>]_27)>
+  - Range: (0xffffffff81000000,0xffffffff8100ffff, 0x1) Exact: True
+
+Register Requirements: {<BV64 rdi>}
+Constraints: []
+Branches: [('0x4000000', <Bool True>, 'Taken'), ('0x400001d', <Bool True>, 'Taken'), ('0x4000005', <Bool True>, 'Taken'), ('0x400001e', <Bool True>, 'Taken')]
+------------------------------------------------

tests/test-cases/nested_calls/ref-output/out.txt

@@ -0,0 +1,42 @@
+
+gadget:     file format elf64-x86-64
+
+
+Disassembly of section .text:
+
+0000000004000000 <nested_calls>:
+ 4000000:	e8 18 00 00 00       	call   400001d <target_1>
+ 4000005:	e8 14 00 00 00       	call   400001e <target_2>
+ 400000a:	4c 8b 07             	mov    r8,QWORD PTR [rdi]
+ 400000d:	4c 0f b7 0f          	movzx  r9,WORD PTR [rdi]
+ 4000011:	4d 8b 91 00 00 00 81 	mov    r10,QWORD PTR [r9-0x7f000000]
+ 4000018:	e9 00 00 00 00       	jmp    400001d <target_1>
+
+000000000400001d <target_1>:
+ 400001d:	c3                   	ret
+
+000000000400001e <target_2>:
+ 400001e:	c3                   	ret
+
+== SCANNER ==
+[MAIN]  Loading angr project...
+[MAIN]  Analyzing gadget at address 0x4000000...
+[MAIN]  Found 1 potential transmissions.
+[MAIN]  Found 0 tainted function pointers.
+[MAIN]  Extracted 1 transmissions.
+[MAIN]  --------------- ANALYZING TRANSMISSIONS ------------------
+[MAIN]  Analyzing <BV64 0xffffffff81000000 + (0#48 .. LOAD_16[<BV64 rdi>]_27)>...
+[MAIN]  Dumped annotated ASM to asm
+[MAIN]  Dumped properties to gadgets.csv
+[MAIN]  --------------- ANALYZING TFPs ------------------
+
+== REASONER ==
+[-] Imported 1 gadgets
+[-] Performing exploitability analysis...
+Found 1 exploitable gadgets!
+[-] Performing exploitability analysis including branch constraints...
+Found 1 exploitable gadgets!
+[-] Performing exploitability analysis assuming the SLAM covert channel...
+Found 0 exploitable gadgets!
+[-] Saving to gadgets-reasoned.csv
+[-] Done!