⬢ DragonFlyBSD Kernel Audit
DF-4875 / proof.c
← back to finding ↓ download raw
/*
 * DF-4875 arithmetic proof (host-side).
 *
 * afd_describe() (sys/dev/disk/nata/atapi-fd.c:446-451) does
 *
 *     char sizestring[16];
 *     if (fdp->mediasize > 1048576 * 5)
 *         ksprintf(sizestring, "%juMB", fdp->mediasize / 1048576);
 *
 * mediasize is u_int64_t and fully device controlled:
 *   - READ_CAPACITY path   : mediasize = (u64)be32toh(cap) * blocksize
 *                            (atapi-fd.c:384) — up to (2^32-1)^2
 *   - READ_CAPACITY_16 path: mediasize = be64toh(cap) * blocksize  (mod 2^64)
 *                            (atapi-fd.c:396) — arbitrary 64-bit value
 *
 * A device that reports e.g. capacity=0xC0000000, blocksize=0xC0000000 makes
 * mediasize ~1.47e19, so mediasize/1048576 has 14 decimal digits and the
 * ksprintf writes 14 + 2 ("MB") + 1 (NUL) = 17 bytes into char[16].
 *
 * This program computes the exact rendered length for representative hostile
 * values and the worst case over the whole u64 range.
 */
#include <stdio.h>
#include <stdint.h>

static int ndigits(uint64_t v) { int n = 1; while (v >= 10) { v /= 10; n++; } return n; }

int main(void) {
    uint64_t cap32 = 0xC0000000ull, bs32 = 0xC0000000ull;
    uint64_t ms_cap  = cap32 * bs32;                    /* READ_CAPACITY path */
    uint64_t ms_big  = 0xFFFFFFFFull * 512ull;          /* READ_CAPACITY_16 wrap */
    uint64_t ms_max  = UINT64_MAX;

    printf("struct afd_capacity   path: cap=0x%llx bs=0x%llx -> mediasize=%llu "
           "-> /1MiB=%llu -> \"%lluMB\" = %d chars + NUL = %d bytes (buffer=16)\n",
           (unsigned long long)cap32, (unsigned long long)bs32,
           (unsigned long long)ms_cap, (unsigned long long)(ms_cap >> 20),
           (unsigned long long)(ms_cap >> 20),
           ndigits(ms_cap >> 20) + 2, ndigits(ms_cap >> 20) + 3);
    printf("struct afd_capacity_big path: cap=0xFFFFFFFF*512 -> mediasize=%llu "
           "-> /1MiB=%llu -> %d chars + NUL = %d bytes (buffer=16)\n",
           (unsigned long long)ms_big, (unsigned long long)(ms_big >> 20),
           ndigits(ms_big >> 20) + 2, ndigits(ms_big >> 20) + 3);
    printf("worst case u64: (2^64-1)/2^20 = %llu -> %d digits -> %d bytes total"
           " -> OVERFLOW of char[16] by %d byte(s)\n",
           (unsigned long long)(ms_max >> 20), ndigits(ms_max >> 20),
           ndigits(ms_max >> 20) + 3, ndigits(ms_max >> 20) + 3 - 16);
    printf("smallest triggering mediasize: %llu (> %d bytes)\n",
           (unsigned long long)10000000000000ull * 1048576ull, 16);
    return 0;
}