/*
 * DF-0569 — Deterministic arithmetic proof of the alias_port byte-swap OOB.
 *
 * Simulates the exact C expression used in ip_fw3_nat.c:423 and :204:
 *
 *   s->alias_port = htons(krandom() % ALIAS_RANGE + ALIAS_BEGIN);   // :439
 *   alias->tcp_in[s->alias_port - ALIAS_BEGIN] = s2;               // :423
 *
 * On little-endian x86-64, htons swaps the two bytes of the uint16_t.
 * The stored field value (read back as uint16_t) is the BYTE-SWAPPED
 * host value.  When that swapped value is < ALIAS_BEGIN (1024), the
 * subtraction `alias_port - ALIAS_BEGIN` produces a NEGATIVE index,
 * causing an out-of-bounds array access (write at :423, read at :204,
 * write at :721/:723 in nat_state_add_dispatch).
 *
 * This program scans every possible host-order alias port value and
 * counts/prints the OOB cases, confirming the ~1.6% probability and
 * the negative-index range.
 */
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <arpa/inet.h>

#define ALIAS_RANGE  64511
#define ALIAS_BEGIN  1024

int main(void)
{
    uint32_t total = 0, oob = 0;
    int min_idx = 0, max_idx = 0;

    printf("=== DF-0569 alias_port OOB arithmetic proof ===\n\n");
    printf("ALIAS_RANGE=%d  ALIAS_BEGIN=%d  tcp_in[%d] (valid idx [0,%d])\n\n",
           ALIAS_RANGE, ALIAS_BEGIN, ALIAS_RANGE, ALIAS_RANGE - 1);

    /* host value range = krandom()%ALIAS_RANGE + ALIAS_BEGIN = [1024, 65534] */
    for (uint32_t host_val = ALIAS_BEGIN;
         host_val < (uint32_t)ALIAS_BEGIN + ALIAS_RANGE;
         host_val++) {

        /* exactly what ip_fw3_nat.c:439 does */
        uint16_t alias_port = htons((uint16_t)host_val);

        /* exactly what ip_fw3_nat.c:423 does — note: NO ntohs() */
        int idx = (int)alias_port - ALIAS_BEGIN;

        total++;
        if (idx < 0 || idx >= ALIAS_RANGE) {
            if (oob == 0) min_idx = max_idx = idx;
            if (idx < min_idx) min_idx = idx;
            if (idx > max_idx) max_idx = idx;
            oob++;
        }
    }

    printf("Total host values scanned : %u\n", total);
    printf("OOB cases (idx <0 or >=%d): %u  (%.2f%%)\n",
           ALIAS_RANGE, oob, 100.0 * oob / total);
    printf("OOB index range           : [%d, %d]  (all NEGATIVE => writes BEFORE tcp_in)\n",
           min_idx, max_idx);
    printf("Max |offset| from tcp_in  : %d bytes (%d * 8)\n",
           (-min_idx) * 8, -min_idx);
    printf("\n");

    /* Concrete examples from the finding */
    printf("--- Concrete examples (host_val -> htons -> field -> index) ---\n");
    struct { uint16_t hv; } cases[] = {
        {0x0400}, {0x0401}, {0x0402}, {0x0403},   /* low byte 0-3 */
        {0x0500}, {0x0601}, {0x1002},             /* more low-byte 0-2 */
        {0x0800}, {0xD001},                        /* low byte 0/1 */
    };
    for (size_t i = 0; i < sizeof(cases)/sizeof(cases[0]); i++) {
        uint16_t hv = cases[i].hv;
        uint16_t field = htons(hv);
        int idx = (int)field - ALIAS_BEGIN;
        int in_bounds = (idx >= 0 && idx < ALIAS_RANGE);
        printf("  host=0x%04x(%5u) -> htons -> field=0x%04x(%5u) -> idx=%7d  %s\n",
               hv, hv, field, field, idx,
               in_bounds ? "(in bounds)" : "*** OOB ***");
    }
    printf("\n");

    /* The specific case from the finding claim */
    uint16_t hv = 0x0401;   /* 1025 */
    uint16_t field = htons(hv);
    int idx = (int)field - ALIAS_BEGIN;
    printf("--- Finding's example: host_val=0x0401 (1025) ---\n");
    printf("  htons(0x%04x) = 0x%04x (%u)\n", hv, field, field);
    printf("  index = %u - %d = %d\n", (unsigned)field, ALIAS_BEGIN, idx);
    printf("  tcp_in[%d] => offset %d bytes from tcp_in[0]\n", idx, idx * 8);
    printf("  => %s (writes %d bytes BEFORE tcp_in[0])\n",
           idx < 0 ? "OUT OF BOUNDS" : "in bounds",
           -(idx * 8));
    printf("\n");

    printf("=== VERDICT: the index computation is ALWAYS out-of-bounds when\n");
    printf("    the low byte of the host-order port is 0, 1, 2, or 3.\n");
    printf("    Probability = 4/256 = %.4f%% per new NAT'd connection.\n",
           100.0 * 4 / 256);

    return 0;
}