⬢ DragonFlyBSD Kernel Audit
DF-0907 / harness.c
← back to finding ↓ download raw 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
/*
 * DF-0907 deterministic arithmetic harness.
 *
 * Transcribes the EXACT pointer arithmetic of smbfs_vfsops.c:165-178 into a
 * userspace model so the signed underflow is provable without the kernel.
 * The model uses the real MNAMELEN (80) and a real-sized username buffer.
 *
 * Output proves:
 *   - pe-pc-2 == -1  (as ptrdiff_t) at the second strncpy
 *   - which becomes SIZE_MAX when coerced to size_t (strncpy's 3rd arg)
 *
 * Build:  cc -o harness harness.c
 * Run:    ./harness
 */
#include <stdio.h>
#include <stddef.h>
#include <string.h>

#define MNAMELEN 80   /* sys/sys/mount.h: #define MNAMELEN 80 */

int main(void)
{
    char buf[MNAMELEN];          /* stand-in for f_mntfromname */
    char *pc, *pe;
    const char *vc_username;
    /* SMB_MAXUSERNAMELEN-1 = 127 chars accepted; we use 80 (>= 76). */
    char userbuf[128];
    size_t bound1, bound2_signed_view;
    long diff;

    memset(userbuf, 'A', 80);
    userbuf[80] = '\0';
    vc_username = userbuf;

    pc = buf;
    pe = pc + sizeof(buf);          /* pe = buf + 80            */
    memset(pc, 0, MNAMELEN);        /* bzero(pc, MNAMELEN);     */
    *pc++ = '/';                    /* buf[0]='/', pc=buf+1     */
    *pc++ = '/';                    /* buf[1]='/', pc=buf+2     */

    /* line 170: strncpy(pc, vc_username, pe-pc-2) */
    diff = (pe - pc - 2);
    printf("line 170: pe-pc-2 = (buf+80)-(buf+2)-2 = %ld  (bound)\n", diff);
    /* strncpy bound = 78-2 = 76 */
    bound1 = (size_t)diff;
    printf("           -> size_t bound = %zu\n", bound1);
    /* emulate strncpy: writes min(76, 80)=76 bytes, NO NUL terminator */
    {
        size_t n = bound1;
        size_t srclen = strlen(vc_username);
        size_t tocopy = (srclen < n) ? srclen : n;
        memcpy(pc, vc_username, tocopy);
        if (srclen < n) {
            /* strncpy zero-pads; here we don't since srclen>=n */
        }
        /* buf[2..77] = 'A'*76, buf[78..79] still 0 from memset */
    }
    /* index(pc, 0): scan past the 76 'A's, find buf[78]=0 */
    {
        char *p = pc;
        while (*p != 0) p++;
        pc = p;
    }
    printf("           after index: pc = buf+%ld (NUL at buf+78)\n", (long)(pc - buf));

    /* line 171: if (pc < pe-1) */
    if (pc < pe - 1) {              /* buf+78 < buf+79 -> TRUE */
        printf("line 171: pc < pe-1  ->  TRUE\n");
        /* line 172: *(pc++)='@'; overwrites buf[78]=0, pc=buf+79 */
        *pc++ = '@';
        printf("line 172: wrote '@' at buf+%ld, pc now buf+%ld\n",
               (long)(pc - 1 - buf), (long)(pc - buf));

        /* line 173: strncpy(pc, vc_srvname, pe-pc-2) */
        diff = (pe - pc - 2);
        printf("line 173: pe-pc-2 = (buf+80)-(buf+79)-2 = %ld  (ptrdiff_t)\n", diff);
        bound2_signed_view = (size_t)diff;
        printf("           coerced to size_t (strncpy 3rd arg) = %zu\n",
               bound2_signed_view);
        printf("           SIZE_MAX = %zu\n", (size_t)-1);
        if (bound2_signed_view == (size_t)-1) {
            printf("*** CONFIRMED: bound is (size_t)-1 == SIZE_MAX ***\n");
            printf("*** strncpy would write vc_srvname + ~SIZE_MAX zero-padding ***\n");
            printf("*** => heap overflow past f_mntfromname into struct statfs/mount ***\n");
            return 0;
        } else {
            printf("UNEXPECTED: bound is not SIZE_MAX\n");
            return 1;
        }
    } else {
        printf("line 171: pc < pe-1 -> FALSE (no overflow)\n");
        return 1;
    }
}