⬢ DragonFlyBSD Kernel Audit
DF-0243 / math_proof.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
/*
 * math_proof.c -- standalone proof that the size_t underflow at
 * sys/kern/imgact_shell.c:126 is mathematically equivalent to the intended
 * signed subtraction, for ALL THREE mutated fields (begin_envv, endp, space).
 *
 * Build: cc -O2 -Wall -o math_proof math_proof.c
 * Run:   ./math_proof
 *
 * The "buggy-path" column reproduces the kernel's exact arithmetic. The
 * "intended" column shows what the code is conceptually trying to compute
 * (signed). The "expected" column shows the correct post-rearrangement value
 * (new content is "/bin/sh\0/tmp/df0243_s\0" = 22 bytes, so endp = buf+22
 * and space = ARG_MAX - 22). All three columns match for every field.
 */
#include <stdio.h>
#include <stdint.h>
#include <stddef.h>
#include <string.h>

#define ARG_MAX 262144

int main(void)
{
    /* argv[0]=256*'A' (len 257), interp="/bin/sh", fname="/tmp/df0243_s" */
    size_t offset = 8 + strlen("/tmp/df0243_s") + 1;   /* line 117 -> 22 */
    size_t length = 257;                                /* line 118 */
    printf("offset=%zu length=%zu (offset<length: underflow branch active)\n\n",
           offset, length);

    uintptr_t buf        = 0x1000;
    uintptr_t begin_envv = buf + 257;
    uintptr_t endp       = buf + 257;
    int       space      = ARG_MAX - 257;

    /* === "buggy" path: lines 126-129 exactly as in sys/kern/imgact_shell.c === */
    size_t off_buggy = offset;
    off_buggy -= length;                        /* line 126: wraps to SIZE_MAX-234 */
    uintptr_t be_b = begin_envv + off_buggy;    /* line 127 */
    uintptr_t ep_b = endp + off_buggy;          /* line 128 */
    int       sp_b = (int)((size_t)space - off_buggy);  /* line 129 */

    /* === intended signed semantics: content shrank by (length-offset),
     *     so begin_envv/endp move BACK by (length-offset) and space grows. === */
    long      shrink = (long)length - (long)offset;     /* +235 */
    uintptr_t be_i   = begin_envv - (uintptr_t)shrink;
    uintptr_t ep_i   = endp - (uintptr_t)shrink;
    int       sp_i   = space + (int)shrink;

    /* === expected: new content is 22 bytes ("/bin/sh\0/tmp/df0243_s\0") === */
    uintptr_t be_exp = buf + 22;
    int       sp_exp = ARG_MAX - 22;

    printf("field        buggy-path      intended        expected        verdict\n");
    printf("begin_envv   0x%-12lx 0x%-12lx 0x%-12lx %s\n", be_b, be_i, be_exp,
           (be_b == be_i && be_b == be_exp) ? "ALL MATCH" : "MISMATCH");
    printf("endp         0x%-12lx 0x%-12lx 0x%-12lx %s\n", ep_b, ep_i, be_exp,
           (ep_b == ep_i && ep_b == be_exp) ? "ALL MATCH" : "MISMATCH");
    printf("space        %-14d %-14d %-14d %s\n", sp_b, sp_i, sp_exp,
           (sp_b == sp_i && sp_b == sp_exp) ? "ALL MATCH" : "MISMATCH");

    printf("\nbegin_envv = buf + %ld  (well inside the ARG_MAX+PATH_MAX buffer)\n",
           (long)(be_b - buf));
    printf("=> the size_t wrap is mathematically equivalent to the signed op.\n");
    printf("=> NO wild pointer, NO corruption, NO panic. FALSE POSITIVE.\n");
    return 0;
}