Symbolic memory addressing

[r4dr3fr4d]

Hello,

I'm trying to experiment with how Maat handles symbolic memory addressing. I have the following C program, which contains an input-indexed load and a potential crash:

#include <stdio.h>
#include <stdlib.h>

int main(int argc, char ** argv) {
    char buffer[10] = "abcdefghij";
    printf("%c\n", buffer[atoi(argv[1])]);
    return 0;
}

Which emits the following assembly:

0000000000001149 <main>:
    1149:       55                      push   rbp
    114a:       48 89 e5                mov    rbp,rsp
    114d:       48 83 ec 20             sub    rsp,0x20
    1151:       89 7d ec                mov    DWORD PTR [rbp-0x14],edi
    1154:       48 89 75 e0             mov    QWORD PTR [rbp-0x20],rsi
    1158:       48 b8 61 62 63 64 65    movabs rax,0x6867666564636261
    115f:       66 67 68
    1162:       48 89 45 f6             mov    QWORD PTR [rbp-0xa],rax
    1166:       66 c7 45 fe 69 6a       mov    WORD PTR [rbp-0x2],0x6a69
    116c:       48 8b 45 e0             mov    rax,QWORD PTR [rbp-0x20]
    1170:       48 83 c0 08             add    rax,0x8
    1174:       48 8b 00                mov    rax,QWORD PTR [rax]
    1177:       48 89 c7                mov    rdi,rax
    117a:       e8 c1 fe ff ff          call   1040 <atoi@plt>
    117f:       48 98                   cdqe
    1181:       0f b6 44 05 f6          movzx  eax,BYTE PTR [rbp+rax*1-0xa]
    1186:       0f be c0                movsx  eax,al
    1189:       89 c6                   mov    esi,eax
    118b:       48 8d 05 72 0e 00 00    lea    rax,[rip+0xe72]        # 2004 <_IO_stdin_used+0x4>
    1192:       48 89 c7                mov    rdi,rax
    1195:       b8 00 00 00 00          mov    eax,0x0
    119a:       e8 91 fe ff ff          call   1030 <printf@plt>
    119f:       b8 00 00 00 00          mov    eax,0x0
    11a4:       c9                      leave
    11a5:       c3                      ret

If I create an engine, set cpu.rax to a symbolic value, then execute run_from(0x1181, 1), the resulting rax is a large expression of ITEs - I'm trying to then evaluate the range of possible indices and thereby loaded values, using the solver, but I cannot seem to figure out the minimum and maximum possibilities. Would you happen to have any advise and/or any guidance on handling symbolic memory addressing in general?

[Boyan-MILANOV]

We are planning to write a tutorial that focuses on symbolic memory specifically, but until then I can try to provide some insights :)

First of all, I will point out that if rax is symbolic and can have any value, then the expression rbp+rax*1-0xa can also take pretty much any value from 0x0 to 0xffffffffffffffff.

I'm trying to then evaluate the range of possible indices and thereby loaded values

The ITE expression returned technically does this for you. Maat returns a conditional expression containing all possible loaded values depending on the memory index.

Now, I assume that what you want to do is extract and isolate the list of possible indexes, perhaps to check if they can be out of bounds? It is not possible to extract them from the ITE expression directly. However, when handling symbolic pointers, Maat internally computes the range of possible values that the pointer can take as a value set which consists in a minimum value, a maximum value, and a stride. For instance a value set of [min: 0x1000, max: 0x2000, stride: 8] means that the pointer can take all the values: 0x1000, 0x1004, 0x1008, ..... 0x2000. Although the value set is not currently exposed to users, we can expose it in the MemAccess class accessible in callbacks for memory access events in engine.info.mem_access. So we could access the info like:

range = engine.info.mem_access.range
range.min # minimum value for the symbolic pointer
range.max # maximum value for the symbolic pointer
range.stride # stride for the symbolic pointer interval

There's actually already a dedicated issue for this: #18

Important note: the value set for symbolic pointers will vary depending on whether the symptr_refine_range option is enabled or not. If symptr_refine_range is disabled, the value set is computed using fast over-approximations. If it is enabled, Maat uses a solver to compute a more accurate value set. The symptr_refine_timeout setting can be used to tell how much time we want to spend refining the range of possible values for symbolic pointers.

Important note 2: there are other options that tweak symbolic memory behaviour, such as restraining the range of possible values for pointers to a hardcoded maximal size, etc. Take a look at the Settings class for more.

[r4dr3fr4d]

Thank you for the answer - I was imagining that there was some sort of cap that limited the range and thereby the number of possible values.

[r4dr3fr4d]

Have you considered the MemSight model? https://raw.githubusercontent.com/season-lab/memsight/master/publications/memsight-ase17.pdf

[Boyan-MILANOV]

Actually Maat already uses a memory model very close to MemSight, with only two differences:

• no support for state merging
• with concolic data, instead of introducing new symbols for potential accesses to uninitialised memory, Maat uses the concrete value of the symbolic expression as the default address

Did you observe some symbolic memory behaviour that doesn't match what you expected to see?

To be honest I think Mayhem was describing a very similar approach to MemSight in their CGC paper, from which we took some ideas to implement symbolic memory in Maat.

[r4dr3fr4d]

Really? I didn't realize that - does it not do it by default? I would think that would be preferred over doing the range/VSA. I may have to test a little more and see if I could produce a counterexample.

…

On Fri, May 13, 2022 at 1:00 PM Boyan MILANOV ***@***.***> wrote: Actually Maat already uses a memory model very close to MemSight, with only two differences: - no support for state merging - with concolic data, instead of introducing new symbols for potential accesses to uninitialised memory, Maat uses the concrete value of the symbolic expression as the default address Did you observe some symbolic memory behaviour that doesn't match what you expected to see? To be honest I think Mayhem was describing a very similar approach to MemSight in their CGC paper, from which we took some ideas to implement symbolic memory in Maat. — Reply to this email directly, view it on GitHub <#95 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACRPRYR5XCNAEHHRKHSTJWLVJ2DCTANCNFSM5VYTJKOQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[Boyan-MILANOV]

Well unless I'm missing something MemSight does the range/VSA stuff. From their paper, you can see that they do build ITEs for reads to memory that could be affected by symbolic writes, just like Maat does:

And then they state that they use VSA as an optimisation:

B. Refinements
In its initial naive formulation, the proposed scheme suffers from a few generality and performance issues. We discuss a
number of refinements that lead to Algorithm 2.

1. Address range selection: One of the main drawbacks of Algorithm 1 is that load and merge operations need to scan the entire memory, which can be highly time and spaceconsuming. We note that it is common for a symbolic address to be constrained within a certain interval [3]. Hence, a more effective approach is to index each tuple (e, v, t, δ) with the smallest range [a, b] that includes all possible values e can attain (line 6 of store in Algorithm 2). The range can be computed by the SMT solver (lines 2–3). A load(e) operation can therefore scan just the tuples whose ranges intersect with the minimum and maximum values of e (lines 2–3, 8).

[r4dr3fr4d]

Perhaps I didn't read into it enough - I didn't know VSA was in the mix of their idea, and that the gist of it was simply storing a tuple (roughly: (sym_address, value)) somewhere so that the symbolic addresses of stored values can be examined later for symbolic reads. I didn't expect VSA or the ITE stuff at all - but I may need to dig deeper and understand it better. I'll try some more examples I couldn't get working with angr.

[Boyan-MILANOV]

Yeah. I'd be interested in the examples you're trying to solve if you don't mind sharing them. More experimenting with symbolic memory is always welcome, and I would certainly be able to provide some insights on potential tweaks of Maat's symbolic memory settings to make the examples work :)

[r4dr3fr4d]

I'm happy to share more examples as I go after them. I'm starting with the simple one I posted above, and after that I'll probably try something like CGC binaries since they're a bit more complex. I looked more at the white paper and the algorithm - you mention above they "build ITEs" for reads to memory, but looking at the algorithm, I'm not sure it's the same thing - the ITE in that load algorithm seems to be for checking the list of addr/value tuples that are maintained in the state, and then returning a value of one of the addresses match the requested one (again, the addresses in this case being symbolic). Are these tuples maintained in maat's state model? I think this works fundamentally differently from the ITE resulting from the VSA method you mention - which is the same as (or similar to) the way angr does it. Does that make sense? Or am I still missing something?

…

On Fri, May 13, 2022 at 3:36 PM Boyan MILANOV ***@***.***> wrote: Yeah. I'd be interested in the examples you're trying to solve if you don't mind sharing them. More experimenting with symbolic memory is always welcome, and I would certainly be able to provide some insights on potential tweaks of Maat's symbolic memory settings to make the examples work :) — Reply to this email directly, view it on GitHub <#95 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACRPRYWV67ZYAV3TIAMHUO3VJ2VKLANCNFSM5VYTJKOQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[Boyan-MILANOV]

the ITE in that load algorithm seems to be for checking the list of addr/value tuples that are maintained in the state, and then returning a value of one of the addresses match the requested one

I believe you are wrong here. I maintain that the ITE in the MemSight load algorithm does effectively build conditional ITE expressions, and their own implementation shows it: the code for load() with a symbolic address does iterate through all tuples and build a conditional ITE expression for each possible tuple match: https://github.com/season-lab/memsight/blob/4c5c5db7fa4c674b0d5cc7321f7d5fef56bd3ff9/memory/simple_fully_symbolic_memory.py#L232-L234

If you maintain a list of tuple and just try to match addresses, you loose a lot of expressivity. For instance If you write 42 at symbolic address A and then read from symbolic address B , and then want to find an input such that reading from B returns 42, the memory read has to return an ITE expression like ITE(A==B, 42, 0). That way you can find out that in order for B to contain 42, we need A == B. But if you instead try to simply match addresses, A would not match B, and you would just return the default value 0.