Forum:
I found out about BGGP3 late, but I wanted to make a late entry to say hi to da slop pit. I was able to slightly modify some symbolic execution tooling I have been playing with to quickly generate a minimal crashing case.
Procmod64.exe falls over easily when loading PML files and I've been using the crashes to show off some of my symbolic execution triage tooling. I'll post a larger blog post about using symbolic execution for effective triage and RE soon, but I wanted to put a small BGGP inspired post here first.
To make a minimal testcase, I used symbolic execution with Triton. Using symbolic execution to trace the input for each of the crashes out of my fuzzer run, I was able to identify a group of crashes that did not depend on any input bytes outside of the minimum required file size.
output:
[inst] : 0x7ff76be37f25: mov edx, dword ptr [rdx]
[crash] : Stepped to an exception: Expected to singlestep 22816, but got exception: (22816)EXCEPTION_ACCESS_VIOLATION(0xc0000005) @ 0x7ff76be37f25 read at 0x238f943a224
[crash] : Got an access violation, checking for symbolic access
[crash] : Loaded from symbolic address: (bvadd (bvadd (_ bv2443723276288 64) (concat INPUT_267 INPUT_266 INPUT_265 INPUT_264 INPUT_263 INPUT_262 INPUT_261 INPUT_260)) (bvmul (_ bv18446744073709551615 64) (concat INPUT_257 INPUT_256 INPUT_255 INPUT_254 INPUT_253 INPUT_252 (_ bv0 16))))
In [1]: set([x.strip('()') for x in str(ctx.simplify(ctx.getPathPredicate(), True)).split() if 'INPUT' in x])
Out [1]:
{
# ... shows required input bytes are all under the minimum PML file size of 0x3a8 bytes.
}
I used the symbolic information gathered from the run to generate a new test case that was the minimum PML size. This didn't work at first, because my symbolic tooling isn't aware of systemcalls. It didn't know what conditions were required to make a call to MapViewOfFile not fail with the newly small input file. So adding my own constraints to ensure that call passed, I was able to reach the bad dereference.
c = astctx.land([
# used for dwFileOffsetLow for MapViewOfFile, lets keep it zero
astctx.variable(ctx.getSymbolicVariable("INPUT_253")) == 0,
astctx.variable(ctx.getSymbolicVariable("INPUT_252")) == 0,
# used for dwFileOffsetHigh for MapViewOfFile, lets keep it zero
astctx.variable(ctx.getSymbolicVariable("INPUT_257")) == 0,
astctx.variable(ctx.getSymbolicVariable("INPUT_256")) == 0,
astctx.variable(ctx.getSymbolicVariable("INPUT_255")) == 0,
astctx.variable(ctx.getSymbolicVariable("INPUT_254")) == 0,
# we want to stay on the path that reaches this crash, add the predicate
ctx.getPathPredicate(),
# try and make the deref'd address to have a bunch of 33h's
# (randomized allocations means it won't be fully 33 other runs)
inst.getLoadAccess()[0][0].getLeaAst() == 0x3333333333333333,
])
model = ctx.getModel(c)
With those conditions I generated the following file! The 0x40s are filler characters, the rest was all decided by the solver. The cool part is I didn't have to have any understanding of the file format to create this. The sad part is I can't make an informative .xx file of it. So instead you get the unimformative one below.
We can at least look at the path constraints to understand why the solver choose what it did.
In [6]: for pc in ctx.getPathConstraints():
...: ast = pc.getTakenPredicate()
...: print(f"->{pc.getTakenAddress():x}")
...: print(expand_ast(ctx.simplify(ast, True)))
┌───────────────────────┐
--═╡ a PROCMON64.EXE crash ╞═--
└───────────┬───────────┴────────────────────────────┐
│@000: │
"PML_" ════════════════════════════╪═The solver says these have to be PML_ │
│ Who am I to argue? │
│ (and │
│ (= INPUT_0 (_ bv80 8 ) ) │
│ (= INPUT_1 (_ bv77 8 ) ) │
│ (= INPUT_2 (_ bv76 8 ) ) │
│ (= INPUT_3 (_ bv95 8 ) ) │
│ ) │
│ │
│@004: │
09000000 ═════════════════════════╪═There is some flex here in the │
│ constraints, but these look good to me │
│ │
│@008: │
01 ═══════════════════════════════╪═This low bit must be 1, the others │
│ just choose not to be │
│ (not │
│ (= │
│ ((_ extract 0 0 ) INPUT_8) │
│ (_ bv0 1 ) │
│ ) │
│ ) │
│ │
│@009: │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╪═These can be whatever you want! │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ Lauren Ipman or whatever, you choose │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@" ═════════╡ │
│ │
│@240: │
ff00000000000000 ═════════════════╪═Reliable sources (z3) tell me that │
│ this value just has to be non-zero to │
│ stay on the path to our crash │
│ │
│@248: │
ff00000000000000 ═════════════════╪═Another non-zero value │
│ │
│@250: │
00ff000000000000 ═════════════════╪═Non-zero, and we also added our own │
│ constraints here so MapViewOfFile │
│ would work with our small file │
│ │
│@258: │
ff00000000000000 ═════════════════╪═Path constraints say non-zero again, │
│ And some of these values end up in the │
│ AST for our derefrenced pointer │
│ │
│@260: │
33337a34cd303333 ═════════════════╪═This value can't be zero, and is the │
│ most controllable part of our pointer │
│ that gets drefrenced, as the below AST │
│ for the pointer shows: │
│ (bvadd │
│ (bvadd │
│ (_ bv0x20e02fa0000 64 ) │
│ (concat │
│ INPUT_267 │
│ INPUT_266 │
│ INPUT_265 │
│ INPUT_264 │
│ INPUT_263 │
│ INPUT_262 │
│ INPUT_261 │
│ INPUT_260 │
│ ) │
│ ) │
│ (bvmul │
│ (_ bv0xffffffffffffffff 64 ) │
│ (concat │
│ INPUT_257 │
│ INPUT_256 │
│ INPUT_255 │
│ INPUT_254 │
│ INPUT_253 │
│ INPUT_252 │
│ (_ bv0 16 ) │
│ ) │
│ ) │
│ ) │
│ │
│@268: │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╪═More empty space you can use as you see│
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ fit. I didn't, but you still can │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@" ╡ │
"@@@@@@@@@@@@@@@@" ════════════════╡ │
│ │
│@398: │
a8030000 ═════════════════════════╪═Look, just trust the solver, okay? │
│ This is the value you want │
│ │
│@39C: │
"@@@@@@@@@@@@" ════════════════════╪═A little tail to pad us out to min size│
│ │
└────────────────────────────────────────┘
Report Topic
