/*
 * divzero_proof.c -- CODE-LEVEL PROOF for DF-0281
 *
 * This is NOT a kernel trigger. It replicates, in userspace, the EXACT integer
 * arithmetic the DragonFlyBSD netgraph7 RFCOMM stack performs on the confirmed
 * vulnerable path, to demonstrate that a peer-supplied PN frame with mtu=0
 * reaches an unguarded divisor and produces a divide-by-zero (#DE -> kernel
 * panic). It runs entirely in userspace on the audit guest because:
 *
 *   (1) the ng_btsocket module is NOT built into / not loadable on the
 *       X86_64_GENERIC master DEV kernel (kldload ng_btsocket -> ENOENT), and
 *   (2) reaching the live path at runtime additionally requires a real RFCOMM
 *       session over L2CAP/HCI, i.e. real bluetooth hardware, which the QEMU
 *       guest does not have and which DragonFlyBSD provides no virtual/software
 *   HCI device for.
 *
 * WHAT IS PROVEN HERE: the arithmetic. Every line that does an arithmetic /
 * control-flow operation is annotated with the matching kernel source line
 * (sys/netgraph7/bluetooth/socket/ng_btsocket_rfcomm.c). The same sequence of
 * C operations executed in the kernel faults the CPU (#DE) and panics; here it
 * raises SIGFPE, which we catch and report. That is the code-level proof.
 *
 * Build:  cc -O2 -Wall -o divzero_proof divzero_proof.c
 * Run:    ./divzero_proof
 *
 * Expected (bug present, arithmetic path reaches the divisor):
 *   ... SIGFPE: divide by zero at step 3 (send_credits, line 3283) ...
 *   PROOF: pcb->mtu==0 reached the unguarded divisor -> kernel would #DE/panic
 *   (exit 0 via the handler; without the handler the process dies on SIGFPE,
 *    mirroring the kernel panic)
 *
 * On a kernel that GUARDS mtu!=0 (the proposed fix.divzero), step 2 clamps mtu
 * to RFCOMM_DEFAULT_MTU and step 3 completes cleanly ("credits=..."). Re-run
 * with the fix compiled in via -DFIX_MTU to see the guarded behavior.
 */

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <signal.h>
#include <unistd.h>

/* ---- Constants mirrored verbatim from ng_btsocket_rfcomm.h ---- */
#define RFCOMM_DEFAULT_MTU    667    /* include/ng_btsocket_rfcomm.h:45 */
#define RFCOMM_DEFAULT_CREDITS 7     /* :48 */
#define RFCOMM_MAX_CREDITS    40     /* :49 */
#define NG_BTSOCKET_RFCOMM_DLC_CFC  (1 << 1)  /* :272 -- credit flow ctrl */

/* ---- Faithful subset of the per-DLC PCB (header struct, line ~176 ff.) ---- */
typedef struct {
    uint16_t mtu;        /* u_int16_t  -- :176 */
    uint8_t  rx_cred;    /* u_int8_t   */
    uint8_t  tx_cred;    /* u_int8_t   */
    uint32_t flags;      /* contains NG_BTSOCKET_RFCOMM_DLC_CFC */
    long     so_rcv_space; /* stands in for ssb_space(&pcb->so->so_rcv) */
} pcb_t;

/* ssb_space() returns long (sys/sys/socketvar.h:270-282). Modelled here. */
static long ssb_space(pcb_t *p) { return p->so_rcv_space; }

/*
 * Replication of ng_btsocket_rfcomm_set_pn() (lines 3013-3043).
 * The ONLY writer of pcb->mtu that takes a peer-controlled value, with NO
 * validation whatsoever -- line 3019 is `pcb->mtu = le16toh(mtu);` directly.
 */
static void rfcomm_set_pn(pcb_t *pcb, uint8_t cr, uint8_t flow_control,
                          uint8_t credits, uint16_t mtu)
{
    /* line 3019: peer mtu copied in UNVALIDATED */
    pcb->mtu = mtu;

#ifdef FIX_MTU
    /* ---- proposed fix.diff (root-cause): reject a zero MTU ---- */
    if (pcb->mtu == 0)
        pcb->mtu = RFCOMM_DEFAULT_MTU;  /* fall back to default */
#endif

    if (cr) {
        if (flow_control == 0xf0) {          /* line 3022 */
            pcb->flags |= NG_BTSOCKET_RFCOMM_DLC_CFC;
            pcb->tx_cred = credits;
        } else {
            pcb->flags &= ~NG_BTSOCKET_RFCOMM_DLC_CFC;
            pcb->tx_cred = 0;
        }
    }
    /* (the !cr branch is symmetric and irrelevant to the divide) */
}

/*
 * Replication of ng_btsocket_rfcomm_send_credits() (lines 3268-3309).
 * Line 3283 is the unguarded divisor:
 *     credits = ssb_space(&pcb->so->so_rcv) / pcb->mtu;
 * With pcb->mtu == 0 this is `long / 0` -> #DE on x86-64 -> kernel panic.
 */
static int rfcomm_send_credits(pcb_t *pcb)
{
    int      error = 0;
    uint8_t  credits;

    /* line 3283 -- THE BUG: divisor is pcb->mtu, no != 0 guard */
    credits = ssb_space(pcb) / pcb->mtu;

#ifdef FIX_DIVISOR
    /* ---- alternative/defense-in-depth guard at the fault site ----
     * (not compiled by default; run with -DFIX_DIVISOR to see the guard) */
    if (pcb->mtu == 0)
        return 0;
#endif
    if (credits > 0) {
        if (pcb->rx_cred + credits > RFCOMM_MAX_CREDITS)
            credits = RFCOMM_MAX_CREDITS - pcb->rx_cred;
        pcb->rx_cred += credits;
    }
    return error;
}

static pcb_t P;

/* strlen variant usable from the SIGFPE handler (strlen itself is fine, but
 * keep it dependency-free and obviously async-signal-safe). */
static size_t strlen_safe(const char *s)
{
    size_t n = 0; while (s[n]) n++; return n;
}
static void putss(const char *s) { write(2, s, strlen_safe(s)); }

static void on_sigfpe(int sig)
{
    (void)sig;
    fflush(stdout);
    /* write() straight to fd 2 -- async-signal-safe, unbuffered */
    putss("\n### SIGFPE: divide by zero at step 3 (send_credits, line 3283) ###\n");
    putss("PROOF: pcb->mtu==0 reached the unguarded divisor "
          "-> kernel would #DE/panic\n");
    putss("(In-kernel: CPU raises #DE -> trap -> panic. "
          "In userspace: #DE -> SIGFPE -> caught here.)\n");
    _exit(0);
}

int main(void)
{
    /*
     * STEP 0: a freshly created DLC. Default MTU is non-zero
     * (ng_btsocket_rfcomm_pcb_alloc, line 432).
     */
    P.mtu          = RFCOMM_DEFAULT_MTU;   /* :432 default */
    P.rx_cred      = RFCOMM_DEFAULT_CREDITS;
    P.tx_cred      = RFCOMM_DEFAULT_CREDITS;
    P.flags        = 0;
    P.so_rcv_space = 4096;                 /* plenty of room in so_rcv */

    setvbuf(stdout, NULL, _IONBF, 0);      /* show all STEP prints even when piped */
    signal(SIGFPE, on_sigfpe);

    puts("DF-0281 code-level proof: netgraph7 RFCOMM divide-by-zero via PN mtu=0");
    puts("(userspace replication of the exact kernel arithmetic; NOT a kernel trigger)\n");
    printf("STEP 0: DLC created, default pcb->mtu = %u (line 432)\n", P.mtu);

    /*
     * STEP 1: the remote peer sends a PN (Parameter Negotiation) MCC frame
     * inside a UIH on dlci 0. The frame carries mtu = 0 (16-bit field, all
     * legal bits, attacker-chosen). This is delivered to the RFCOMM task via
     * soreceive(s->l2so,...) at line 1665, dispatched through
     * ng_btsocket_rfcomm_receive_frame -> receive_mcc (:2553) -> receive_pn
     * (:2913/:2931/:2955) -> ng_btsocket_rfcomm_set_pn.
     *
     * receive_pn validates ONLY that dlci != 0 (:2899). It does NOT check
     * pn->mtu. set_pn does NOT check mtu. So mtu=0 lands in pcb->mtu verbatim.
     */
    uint8_t  peer_flow = 0xf0;   /* requests credit-based flow control (:3022) */
    uint16_t peer_mtu  = 0;      /* <-- the malicious value */
    rfcomm_set_pn(&P, /*cr*/1, peer_flow, RFCOMM_DEFAULT_CREDITS, peer_mtu);
    printf("STEP 1: peer PN with mtu=0 processed by set_pn (line 3019); "
           "now pcb->mtu = %u  <-- NO validation was applied\n", P.mtu);
    printf("        CFC flag now %sset (line 3023)\n",
           (P.flags & NG_BTSOCKET_RFCOMM_DLC_CFC) ? "" : "NOT ");

    /*
     * STEP 2: the peer now sends a single UIH data frame on the DLC. In
     * ng_btsocket_rfcomm_receive_uih (line 2356), once data is present
     * (m0->m_pkthdr.len > 0, :2424) and CFC is on (:2426), rx_cred is
     * decremented (:2428) and, if it has fallen to <= MAX_CREDITS/2,
     * ng_btsocket_rfcomm_send_credits(pcb) is called at line 2429.
     *
     * NOTE: that call site (:2429) is BEFORE the mtu-oversize check at
     * line 2438 -- the finding's "division executes before the oversize
     * check" claim is correct.
     */
    P.rx_cred = RFCOMM_MAX_CREDITS / 2 + 1;   /* one decrement crosses the threshold */
    printf("STEP 2: peer UIH data frame arrives; rx_cred=%u -> --rx_cred=%u "
           "<= MAX_CREDITS/2 -> send_credits() called (line 2429)\n",
           P.rx_cred, P.rx_cred - 1);
    --P.rx_cred;   /* :2428 */

    /*
     * STEP 3: send_credits evaluates `credits = ssb_space(...) / pcb->mtu`
     * (line 3283) with pcb->mtu == 0. On x86-64 this is an integer divide
     * with a zero divisor -> #DE. In the kernel: panic. Here: SIGFPE.
     */
    puts("STEP 3: send_credits line 3283: credits = ssb_space / pcb->mtu ...");
    (void)rfcomm_send_credits(&P);

    /* If we get here, mtu was guarded (fix applied) -> no fault. */
    printf("\nNO FAULT: pcb->mtu was guarded before the divisor "
           "(fix active); credits path completed.\n");
    return 0;
}