search

nimble-code / Modex

a model extractor, to automatically extract Spin verification models from multi-threaded C code
20 stars 4 forks source link

NULL Pointer Dereference in set_create_id() #8

Closed AiDaiP closed 2 years ago

AiDaiP commented 2 years ago

NULL Pointer Dereference in set_create_id()

Description

NULL Pointer Dereference in set_create_id() at xtract.c:3797.

If there is no & in the first argument of pthread_t(), s will be NULL and the next strchr() will crash.

void
set_create_id(void) // from the 1st '&(' to the 1st '),' in OutBuf
{   char *s, *e;

    join_id = 0;
    s = strchr(OutBuf, '&');
    e = strchr(s+1, ')');
    if (!e || e-s <= 1) { return; }

    join_id = (char *) e_malloc((e-s) * sizeof(char));
    strncpy(join_id, s+2, (e-s)-1-1);
}
 pthread_create(&t, 0, thread, 0);
 ► 0x55555556aa76 <set_create_id+35>    call   strchr@plt                <strchr@plt>
        s: 0x5555555a2080 (OutBuf) ◂— 'F: pthread_create((&(Pp_main->t)),0,Pp_main->thread,0)'
        c: 0x26
pthread_create(a, 0, thread, 0);
► 0x55555556aa76 <set_create_id+35>    call   strchr@plt                <strchr@plt>
        s: 0x5555555a2080 (OutBuf) ◂— 'F: pthread_create(Pp_main->a,0,Pp_main->thread,0)'
        c: 0x26

version

acfa291

./modex -V
MODEX Version 2.11 - 3 November 2017

System information Ubuntu 20.04 focal, AMD EPYC 7742 64-Core @ 16x 2.25GHz

poc

#include <stdio.h>
#include <pthread.h>
void *thread(){
    puts("hello world");
}
int main(void)
{   pthread_t t;
    pthread_t* a;
    a = &t;
    while(1) {
        pthread_create(a, 0, thread, 0);
    }
}

command

./modex ./poc.c

Result

./modex ./poc.c
MODEX Version 2.11 - 3 November 2017
[1]    2056163 segmentation fault  ./modex ./poc.c

gdb

pwndbg>
0x000055555556aa8f      3797            e = strchr(s+1, ')');
LEGEND: STACK | HEAP | CODE | DATA | RWX | RODATA
────────────────────────────────────────────[ REGISTERS ]─────────────────────────────────────────────
 RAX  0x1
 RBX  0x55555558c0f0 (__libc_csu_init) ◂— endbr64
 RCX  0x0
 RDX  0x0
*RDI  0x1
 RSI  0x29
 R8   0x212
 R9   0x5555555a2080 (OutBuf) ◂— 'F: pthread_create(Pp_main->t,0,Pp_main->thread,0)'
 R10  0x1e
 R11  0x7fffffffb757 ◂— 0x4c16e0b189dd0030 /* '0' */
 R12  0x5555555585c0 (_start) ◂— endbr64
 R13  0x7fffffffe0f0 ◂— 0x2
 R14  0x0
 R15  0x0
 RBP  0x7fffffffbea0 —▸ 0x7fffffffbee0 —▸ 0x7fffffffc140 —▸ 0x7fffffffc5b0 —▸ 0x7fffffffc5d0 ◂— ...
 RSP  0x7fffffffbe90 ◂— 0x0
*RIP  0x55555556aa8f (set_create_id+60) ◂— call   0x555555558410
──────────────────────────────────────────────[ DISASM ]──────────────────────────────────────────────
   0x55555556aa7b <set_create_id+40>    mov    qword ptr [rbp - 0x10], rax
   0x55555556aa7f <set_create_id+44>    mov    rax, qword ptr [rbp - 0x10]
   0x55555556aa83 <set_create_id+48>    add    rax, 1
   0x55555556aa87 <set_create_id+52>    mov    esi, 0x29
   0x55555556aa8c <set_create_id+57>    mov    rdi, rax
 ► 0x55555556aa8f <set_create_id+60>    call   strchr@plt                <strchr@plt>
        s: 0x1
        c: 0x29

   0x55555556aa94 <set_create_id+65>    mov    qword ptr [rbp - 8], rax
   0x55555556aa98 <set_create_id+69>    cmp    qword ptr [rbp - 8], 0
   0x55555556aa9d <set_create_id+74>    je     set_create_id+155                <set_create_id+155>

   0x55555556aa9f <set_create_id+76>    mov    rax, qword ptr [rbp - 8]
   0x55555556aaa3 <set_create_id+80>    sub    rax, qword ptr [rbp - 0x10]
──────────────────────────────────────────[ SOURCE (CODE) ]───────────────────────────────────────────
In file: /home/aidai/fuzzing/model_checking/Modex-test/Src/xtract.c
   3792 set_create_id(void)     // from the 1st '&(' to the 1st '),' in OutBuf
   3793 {       char *s, *e;
   3794
   3795         join_id = 0;
   3796         s = strchr(OutBuf, '&');
 ► 3797         e = strchr(s+1, ')');
   3798         if (!e || e-s <= 1) { return; }
   3799
   3800         join_id = (char *) e_malloc((e-s) * sizeof(char));
   3801         strncpy(join_id, s+2, (e-s)-1-1);
   3802 }
──────────────────────────────────────────────[ STACK ]───────────────────────────────────────────────
00:0000│ rsp 0x7fffffffbe90 ◂— 0x0
01:0008│     0x7fffffffbe98 ◂— 0x0
02:0010│ rbp 0x7fffffffbea0 —▸ 0x7fffffffbee0 —▸ 0x7fffffffc140 —▸ 0x7fffffffc5b0 —▸ 0x7fffffffc5d0 ◂— ...
03:0018│     0x7fffffffbea8 —▸ 0x55555556b0ce (handle_pthread_create+20) ◂— call   0x55555556aaf1
04:0020│     0x7fffffffbeb0 ◂— 0x0
05:0028│     0x7fffffffbeb8 ◂— 0x5558c0f0
06:0030│     0x7fffffffbec0 —▸ 0x7fffffffc140 —▸ 0x7fffffffc5b0 —▸ 0x7fffffffc5d0 —▸ 0x7fffffffca40 ◂— ...
07:0038│     0x7fffffffbec8 —▸ 0x5555555585c0 (_start) ◂— endbr64
────────────────────────────────────────────[ BACKTRACE ]─────────────────────────────────────────────
 ► f 0   0x55555556aa8f set_create_id+60
   f 1   0x55555556b0ce handle_pthread_create+20
   f 2   0x55555556cc32 modex_recur+4535
   f 3   0x55555556ee66 modex_node+266
   f 4   0x55555557050c modex_any+85
   f 5   0x55555556f98c modex_node+3120
   f 6   0x55555557050c modex_any+85
   f 7   0x55555556f894 modex_node+2872
──────────────────────────────────────────────────────────────────────────────────────────────────────
pwndbg> bt
#0  0x000055555556aa8f in set_create_id () at xtract.c:3797
#1  0x000055555556b0ce in handle_pthread_create (which=0) at xtract.c:3966
#2  0x000055555556cc32 in modex_recur (root=0x7ffff7b6e3d8) at xtract.c:4425
#3  0x000055555556ee66 in modex_node (node=0x7ffff7b6e3d8, tabs=2) at xtract.c:5197
#4  0x000055555557050c in modex_any (child=0x7ffff7b6e3d8, tabs=2) at xtract.c:5746
#5  0x000055555556f98c in modex_node (node=0x7ffff7b6e658, tabs=2) at xtract.c:5505
#6  0x000055555557050c in modex_any (child=0x7ffff7b6e658, tabs=2) at xtract.c:5746
#7  0x000055555556f894 in modex_node (node=0x7ffff7b6e6f8, tabs=2) at xtract.c:5484
#8  0x000055555557050c in modex_any (child=0x7ffff7b6e6f8, tabs=2) at xtract.c:5746
#9  0x000055555556f8af in modex_node (node=0x7ffff7b6e108, tabs=2) at xtract.c:5485
#10 0x000055555557050c in modex_any (child=0x7ffff7b6e108, tabs=2) at xtract.c:5746
#11 0x0000555555570357 in modex_for (forn=0x7ffff7b6e1f8, tabs=1) at xtract.c:5701
#12 0x0000555555570545 in modex_any (child=0x7ffff7b6e1f8, tabs=1) at xtract.c:5756
#13 0x000055555556f98c in modex_node (node=0x7ffff7b6e6a8, tabs=1) at xtract.c:5505
#14 0x000055555557050c in modex_any (child=0x7ffff7b6e6a8, tabs=1) at xtract.c:5746
#15 0x0000555555570b19 in modex_tree (root=0x7ffff7b6e6a8, lut=0x55555558d215 "none.lut") at xtract.c:5852
#16 0x000055555555f962 in main (argc=2, argv=0x7fffffffe0f8) at modex.c:1337
#17 0x00007ffff7c980b3 in __libc_start_main (main=0x55555555f510 <main>, argc=2, argv=0x7fffffffe0f8, init=<optimized out>, fini=<optimized out>, rtld_fini=<optimized out>, stack_end=0x7fffffffe0e8) at ../csu/libc-start.c:308
#18 0x00005555555585ee in _start ()

fix

Should we add some code here to handle it?

If there is no &，get the substring from the 1st '(' to the 1st ',' in OutBuf.

void
set_create_id(void) // from the 1st '&(' to the 1st '),' in OutBuf or from the 1st '(' to the 1st ',' in OutBuf
{   char *s, *e;

    join_id = 0;
    s = strchr(OutBuf, '&');
    if (s != NULL)
    {   e = strchr(s+1, ')');
    }
    else
    {
        s = strchr(OutBuf, '(')-1;
        e = strchr(s+1, ',');
    }
    if (!e || e-s <= 1) { return; }

    join_id = (char *) e_malloc((e-s) * sizeof(char));
    strncpy(join_id, s+2, (e-s)-1-1);
}
nimble-code commented 2 years ago

Uploaded a fix for this case -- but rather than attempting to handle it, the function just returns without further action, just like when there's no comma. Note, there could also be a missing '(' which would then still recreate the null pointer deref thanks for reporting this!