97 lines
4.1 KiB
Python
97 lines
4.1 KiB
Python
#!/usr/bin/env python3
|
|
"""Independent shifted-boundary ablation and branch-exposure audit."""
|
|
import hashlib
|
|
import json
|
|
import struct
|
|
from pathlib import Path
|
|
|
|
root = Path("/home/alex/sots-re")
|
|
out = root / "verify/results/research-completion-abi-independent/run-d94d4516b9d898793318805e"
|
|
data = (root / "dumps/sots.exe").read_bytes()
|
|
pe = struct.unpack_from("<I", data, 0x3c)[0]
|
|
assert data[pe:pe + 4] == b"PE\0\0"
|
|
nsec = struct.unpack_from("<H", data, pe + 6)[0]
|
|
opt_size = struct.unpack_from("<H", data, pe + 20)[0]
|
|
opt = pe + 24
|
|
assert struct.unpack_from("<H", data, opt)[0] == 0x10b
|
|
base = struct.unpack_from("<I", data, opt + 28)[0]
|
|
table = opt + opt_size
|
|
sections = []
|
|
for i in range(nsec):
|
|
pos = table + 40 * i
|
|
name = data[pos:pos + 8].rstrip(b"\0").decode("ascii")
|
|
vsize, va, raw_size, raw = struct.unpack_from("<IIII", data, pos + 8)
|
|
sections.append((name, va, max(vsize, raw_size), raw, raw_size))
|
|
|
|
def read_va(address, size):
|
|
rva = address - base
|
|
for name, va, span, raw, raw_size in sections:
|
|
if va <= rva and rva + size <= va + span:
|
|
delta = rva - va
|
|
assert delta + size <= raw_size
|
|
return data[raw + delta:raw + delta + size]
|
|
raise AssertionError(hex(address))
|
|
|
|
targets = {
|
|
"observed-alloc": (0x57E5E3, "c20400"),
|
|
"player-append": (0x86C62D, "c20400"),
|
|
"player-copy": (0x7694BF, "c20400"),
|
|
"observed-push": (0x7B739E, "c20400"),
|
|
"observed-realloc": (0x7B35EE, "c20400"),
|
|
"string-alloc": (0x424AD9, "c20800"),
|
|
"dedup": (0x825E64, "c20800"),
|
|
}
|
|
ablations = []
|
|
for name, (address, expected_hex) in targets.items():
|
|
expected = bytes.fromhex(expected_hex)
|
|
exact = read_va(address, len(expected))
|
|
minus = read_va(address - 1, len(expected))
|
|
plus = read_va(address + 1, len(expected))
|
|
record = {
|
|
"name": name, "address": hex(address), "expected": expected_hex,
|
|
"exact": exact.hex(), "minus_one": minus.hex(), "plus_one": plus.hex(),
|
|
"exact_pass": exact == expected,
|
|
"shifted_negative_control_pass": minus != expected and plus != expected,
|
|
}
|
|
assert record["exact_pass"] and record["shifted_negative_control_pass"]
|
|
ablations.append(record)
|
|
|
|
def text(name):
|
|
return (out / (name + ".stdout.txt")).read_text()
|
|
|
|
exposures = {
|
|
"observed_stride_0x2c": "imul ecx,ecx,0x2c" in text("observed-alloc-wide"),
|
|
"observed_deep_copy_call": "call 0x79a150" in text("observed-push-wide"),
|
|
"player_stride_0x74": "add DWORD PTR [edi+0x4],0x74" in text("player-append-wide"),
|
|
"player_deep_copy_call": "call 0x7693f0" in text("player-append-wide"),
|
|
"player_three_delete_calls": text("player-dtor-control").count("call 0x924faa") == 3,
|
|
"description_inequality_call": "call 0x46f8c0" in text("dedup-wide"),
|
|
"dedup_stride_0x74": "add DWORD PTR [ebp+0x8],0x74" in text("dedup-wide"),
|
|
"three_float_unordered_or_unequal_rejections":
|
|
text("dedup-wide").count("fucompp") == 3
|
|
and text("dedup-wide").count("test ah,0x44") == 3
|
|
and text("dedup-wide").count("jp 0x825e25") == 3,
|
|
}
|
|
assert all(exposures.values())
|
|
state = json.loads((out / "independent-state.json").read_text())
|
|
actual_state = {
|
|
"evnxid_has_4": 4 in state["evnxid_values"],
|
|
"turn3_bucket_has_2": 2 in state["turn3_bucket_counts"],
|
|
"event3_position_defaults": state["event3"]["position_words"] == [2139095039] * 3,
|
|
"whole_state_rebuild": state["coverage"] == {
|
|
"ok": True, "rebuiltBytes": 609080, "inflatedBytes": 609080, "firstDiff": None},
|
|
"rng_leaf": state["rng"]["valueBytes"] == 2503
|
|
and state["rng"]["digest"] == "0978fdf34ff7962f76c2de810dc93e0a",
|
|
}
|
|
assert all(actual_state.values())
|
|
result = {
|
|
"schema": "sots-abi-heldout/1",
|
|
"session": "run-d94d4516b9d898793318805e",
|
|
"binary_sha256": hashlib.sha256(data).hexdigest(),
|
|
"challenge": "direct PE exact versus minus-one/plus-one shifted return encodings",
|
|
"ablations": ablations,
|
|
"branch_exposures": exposures,
|
|
"actual_state_checks": actual_state,
|
|
"pass": True,
|
|
}
|
|
(out / "heldout-boundary.json").write_text(json.dumps(result, indent=2) + "\n")
|