Memory models

[fortunac]

We should have a notion of memory in WP represented as a BV64 -> bool stating that an address returns either true or false if it is in a certain region of memory. For example, the address 0x00007FFFFFFFD588 is true in the stack, and false in the heap.

We should add these types to Env.t such that:

type t = {
  stack : BV64 -> bool;
  heap : BV64 -> bool;
   ...
}

We can then define our own stacks and heaps with: Stack(x) := stack_min <= x <= stack_max and Heap(x) := heap_min <= x <= heap_max where stack_min, stack_max, heap_min, and heap_max are concrete values. There should be some buffer between stack_min and heap_max.

With this, we should have a way to compare the memory between the new binaries. We could start off by comparing the heap with ∀x. Heap(x) -> mem_orig[x] == mem_mod[x + d] and the stack with ∀x. Stack(x) -> mem_orig[x] == mem_mod[x]. These should be added to the precondition.

Lastly, we should add the constraint of Stack(SP) to the precondition to assert that the stack pointer is pointing to a valid location on the stack.

[fortunac]

A related SO post: https://unix.stackexchange.com/questions/466389/where-are-the-kernel-stack-frames-for-c-run-time-startup-functions-and-fr

[fortunac]

We tested out adding ∀x. Heap(x) -> mem_orig[x] == mem_mod[x + d] and ∀x. Stack(x) -> mem_orig[x] == mem_mod[x] as a hypothesis to our precondition, but this results in a major slowdown with Z3 due to the quantifiers. A very simple example with one basic block (diff_data_location) now takes 9 seconds to run.

We will revisit this with a new approach that adds hooks to memory reads/writes.