Store substitution passes incorrect expression at call

[SanWieb]

In certain cases the getSubstitution() function in store_hook_before returns an incorrect expression if a call is performed, resulting in an incorrect store transmission.

Test-case: 0xffffffff81225b90 get_unmapped_area

TransmitterType.STORE:

----------------- TRANSMISSION -----------------
                  get_unmapped_area:
ffffffff81225b90  endbr64 
ffffffff81225b94  push    rbp
ffffffff81225b95  mov     rax, qword ptr  gs:[pcpu_hot]
ffffffff81225b9e  push    rbx
ffffffff81225b9f  mov     rbx, rdx
ffffffff81225ba2  mov     rdx, qword ptr [rax]
ffffffff81225ba5  test    edx, 0x20000000
ffffffff81225bab  je      0xffffffff81225c8c ; Taken   <Bool (LOAD_64[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_21>]_23[31:0] & 0x20000000) != 0x0>
ffffffff81225bb1  test    byte ptr [rax+0x4d3], 0x8
ffffffff81225bb8  mov     edx, 0xffffe000
ffffffff81225bbd  mov     eax, 0xc0000000
ffffffff81225bc2  cmove   rax, rdx
ffffffff81225bc6  cmp     rax, rbx
ffffffff81225bc9  jb      0xffffffff81225c7e ; Taken   <Bool (if (LOAD_8[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_21 + 0x4d3>]_24 & 8) == 0 then 0xffffe000 else 0xc0000000) >= rdx>
ffffffff81225bcf  mov     rax, qword ptr  gs:[pcpu_hot] ; {Uncontrolled@gs} > {MaybeAttacker@0xffffffff81225bcf}
ffffffff81225bd8  mov     rax, qword ptr [rax+0x4a8] ; {MaybeAttacker@0xffffffff81225bcf} > {Attacker@0xffffffff81225bd8}
ffffffff81225bdf  mov     rax, qword ptr [rax+0x50] ; {Attacker@0xffffffff81225bd8} > {Secret@0xffffffff81225bdf}
ffffffff81225be3  test    rdi, rdi
ffffffff81225be6  je      0xffffffff81225c9b ; Taken   <Bool rdi == 0x0>
ffffffff81225c9b  mov     rdx, r8
ffffffff81225c9e  mov     r9, shmem_get_unmapped_area
ffffffff81225ca5  and     edx, 0x1
ffffffff81225ca8  cmovne  rax, r9
ffffffff81225cac  cmovne  rcx, rdi
ffffffff81225cb0  jmp     0xffffffff81225c01 ; Taken   <Bool True>
ffffffff81225c01  mov     rdx, rbx
ffffffff81225c04  call    __x86_indirect_thunk_array ; {Secret@0xffffffff81225bdf} > TRANSMISSION

------------------------------------------------
uuid: 05b4c0b8-5a35-48b8-a0b5-e0d0159529b8

Secret Address:
  - Expr: <BV64 LOAD_64[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_25 + 0x4a8>]_26 + 0x50>
  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
Transmitted Secret:
  - Expr: <BV64 LOAD_64[<BV64 LOAD_64[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_25 + 0x4a8>]_26 + 0x50>]_27>
  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True
  - Spread: 0 - 63
  - Number of Bits Inferable: 64
Base:
  - Expr: None
  - Range: None
  - Independent Expr: None
  - Independent Range: None
Transmission:
  - Expr: <BV64 LOAD_64[<BV64 LOAD_64[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_25 + 0x4a8>]_26 + 0x50>]_27>
  - Range: (0x0,0xffffffffffffffff, 0x1) Exact: True

Register Requirements: {<BV64 gs>, <BV64 r8>}
Constraints: [('0xffffffff81225c04', <Bool r8[0:0] == 0>)]
Branches: [(18446744071581096875, <Bool (LOAD_64[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_21>]_23[31:0] & 0x20000000) != 0x0>, 'Taken'), (18446744071581096905, <Bool (if (LOAD_8[<BV64 LOAD_64[<BV64 0x2ac80 + gs>]_21 + 0x4d3>]_24 & 8) == 0 then 0xffffe000 else 0xc0000000) >= rdx>, 'Taken'), (18446744071581096934, <Bool rdi == 0x0>, 'Taken'), (18446744071581097136, <Bool True>, 'Taken')]
------------------------------------------------

Store log:

Store@0xffffffff81225b94: [<BV64 rsp - 0x8>] = <BV64 rbp>
After substitution: Store@0xffffffff81225b94: [<BV64 rsp - 0x8>] = <BV64 rbp>
Store@0xffffffff81225b9e: [<BV64 rsp - 0x10>] = <BV64 rbx>
After substitution: Store@0xffffffff81225b9e: [<BV64 rsp - 0x10>] = <BV64 rbx>
Store@0xffffffff81225c04: [<BV64 0xfffffffffffffff0 + rsp - 0x8>] = <BV64 0xffffffff81225c09>
After substitution: Store@0xffffffff81225c04: [<BV64 0xfffffffffffffff0 + rsp - 0x8>] = <BV64 0xffffffff81225c09>
Store@0xffffffff81225c04: [<BV64 0xfffffffffffffff0 + rsp - 0x8>] = <BV64 0xffffffff81225c09>
After substitution: Store@0xffffffff81225c04: [<BV64 LOAD_64[<BV64 LOAD_64[<BV64 rdi + 0xb0>]_28 + 0x98>]_29>] = <BV64 0xffffffff81225c09>

[AlviseDeFaveri]

Can you check if this is still reproducible? For the same test case I now see only 3 CODE_LOADs reported at address 0xffffffff81225c04

[AlviseDeFaveri]

closing, please reopen if this is not solved