`symbolic`: Modeling the stack

langston-barrett commented 3 months ago

In a downstream project, we're using macaw-symbolic to symbolically execute binaries. macaw-symbolic encodes functions in the binary as Crucible CFGs that take and return a struct that represents the values of all the registers. To execute such CFGs, we must set initial values for all registers. Most registers can be set to zeroes or symbolic values and plenty of code will run just fine. However, machine code has a lot of expectations about one particular register: the stack pointer.

Each ABI[^1] specifies a stack layout, and our project attempts to model this layout at a low level of abstraction. In particular, we create a large-ish (1MiB) Crucible-LLVM allocation, and:

On AArch32, the very end is initialized with a number of pointer-sized stack slocks, which are reserved for stack-spilled arguments.[^spill]
On PPC, the very end is initialized with (in order):
- A pointer-sized chunk of bytes representing the return address.
- A pointer-sized zero value, representing the PowerPC back chain for the entrypoint function.
- A number of pointer-sized stack slocks, which are reserved for stack-spilled arguments.
On x86_64, the very end is initialized with (in order):
- A pointer-sized chunk of bytes representing the return address.
- A number of pointer-sized stack slocks, which are reserved for stack-spilled arguments.

The contents of the stack pointer register are then initialized to be a pointer to this allocation, offset to where the above data begin.

I'd wager that since a lot of code uses the stack, most clients of macaw-symbolic want to model the stack somehow. Furthermore, since macaw-symbolic fairly directly translates manipulations of the stack pointer register in binaries into the Crucible CFGs, I'd argue that this is likely the only strategy that works "out of the box". Therefore, I think we should upstream this code (or something like it) into macaw-*-symbolic.

One notable upside of this kind of model of the stack is that we can examine what happens in the case of certain kinds of common stack-based exploits, such as stack buffer overruns that clobber adjacent variables, as in this C program:

#include "stddef.h"
#include "stdio.h"

__attribute__((noinline)) void zero(char *buf, size_t len) {
  for (int i = 0; i < len; i++) {
    buf[i] = 0;
  }
}

__attribute__((noinline)) void print(char val) {
  printf("val = %i\n", val);
}

void caller(void) {
  char val = 1;
  char buf[8] = {1};
  zero(buf, 9);
  print(val);
}

int main() {
  caller();
}

One notable downside is that such exploits are not automatically detected by the Crucible-LLVM memory model, and so care would be required by users of such an API if they intend to perform safety-oriented analysis.

[^1]: at a first approximation, each (OS, architecture) pair [^spill]: One difficulty is that it's hard to tell in advance of executing a function how many stack slots should be reserved for spilled arguments. DWARF information can serve as a source of truth here, when it's available.

sauclovian-g commented 3 months ago

Does Crucible's memory model have the ability to segment a chunk of memory? (As in, distinguish regions that are adjacent to each other and addressable from the same base pointer?) Then you could prepare a stack frame that will be resistant to such attacks... given some assumptions about when you should specialize a pointer to a segmented chunk to a pointer to a segment, which may turn out to be not so easy.

(just speculating, feel free to ignore)

langston-barrett commented 3 months ago

Does Crucible's memory model have the ability to segment a chunk of memory? (As in, distinguish regions that are adjacent to each other and addressable from the same base pointer?)

I don't believe so.

Another idea, not sure how feasible this one is... We could create an ExecutionFeature that, before entering a new Macaw CFG:

Allocates a fresh Crucible-LLVM allocation of type StackAlloc
Writes the return address and/or other ABI-specific information to the end of the allocation
Puts a pointer to (almost the end of) this fresh allocation into the stack pointer register

That would at least prevent inter-frame memory corruption, though it wouldn't do anything to stop code from overwriting adjacent stack variables nor the return address. Perhaps for the return address, the same execution feature could check that it is unmodified at function returns.

RyanGlScott commented 3 months ago

An addendum: I believe that RISC-V also initializes the end of its stack with slots for stack-spilled arguments, just as AArch32 does (although you should make sure that you adjust the offset on the stack pointer s0 depending on whether you are using 32-bit or 64-bit RISC-V).

langston-barrett commented 3 months ago

Prior art:

`Data.Macaw.Symbolic.Testing`

Uses a symbolic, SMT-array-backed stack. As an aside, it's kind of odd to me that this stack setup is spread across so many different lines.

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L501-L506

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L530-L531

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L533-L538

`pate`

Also seems array-backed

https://github.com/GaloisInc/pate/blob/c43542818be7780264d8a2552bfeba1cffba2902/src/Pate/Verification/InlineCallee.hs#L135-L143

`saw-script`

Seems like it's just a fresh, symbolic pointer?

https://github.com/GaloisInc/saw-script/blob/47a7632c973df3fdb2d32268edc92948fc150f2d/src/SAWScript/X86Spec.hs#L446

Potentially with negative consequences?

https://github.com/GaloisInc/saw-script/blob/47a7632c973df3fdb2d32268edc92948fc150f2d/src/SAWScript/X86Spec.hs#L1285-L1288

`ambient-verifier`

Also does an SMT array:

https://github.com/GaloisInc/ambient-verifier/blob/open-source/src/Ambient/Verifier/SymbolicExecution.hs#L1272-L1280

Conclusions

Indeed, virtually every client of Macaw wants to model the stack, and most of them do
Whatever we implement in Macaw should at least have the option to use an SMT array allocation

GaloisInc / macaw