CVE-2021-46168: Out-of-bounds Write in lex() · Issue #56 · nimble-code/Spin

Out-of-bounds Write in lex()****Description

Out-of-bounds Write in lex() at spinlex.c:1707

If there are 129 {，the yyin will add 1

int scope_seq[128], scope_level = 0; //… case '{’: scope_seq[scope_level++]++; set_cur_scope(); break;

then, the fclose(yyin) at main:1162 will crash.

If there are more } than {, the scope_level will be negative.

case '}': scope_level--; set_cur_scope(); break;

then, the variables before scope_seq will add 1.

Should there be a limit?

version

045a0a5

./spin -V
Spin Version 6.5.1 -- 3 June 2021

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

poc

{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{{

command

Result

spin ./poc.pml
spin: ./poc.pml:1, Error: syntax error  saw ''{' = 123'
[1]    3640076 segmentation fault  ./spin ./poc.pml

gdb

pwndbg> c Continuing. [Detaching after vfork from child process 3024771]

Hardware watchpoint 2: yyin

Old value = (FILE *) 0x7ffff7fab980 <_IO_2_1_stdin_> New value = (FILE *) 0x5555556d32a0 0x00005555555ce524 in main (argc=2, argv=0x7fffffffe188) at main.c:1106 1106 if (!(yyin = fopen(out1, “r”))) LEGEND: STACK | HEAP | CODE | DATA | RWX | RODATA ────────────────────────────────────────────[ REGISTERS ]───────────────────────────────────────────── *RAX 0x5555556d32a0 ◂— 0xfbad2488 RBX 0x5555556111f0 (__libc_csu_init) ◂— endbr64 *RCX 0x1e *RDX 0x0 *RDI 0x555555618c9e ◂— 0x63203a6e69707300 *RSI 0x2c *R8 0x8 *R9 0x1 *R10 0x0 *R11 0x246 R12 0x5555555bc660 (_start) ◂— endbr64 R13 0x7fffffffe180 ◂— 0x2 R14 0x0 R15 0x0 RBP 0x7fffffffe090 ◂— 0x0 RSP 0x7fffffffdc30 —▸ 0x7fffffffe188 —▸ 0x7fffffffe47d ◂— ‘/home/aidai/fuzzing/model_checking/Spin-test/Src/spin’ *RIP 0x5555555ce524 (main+3399) ◂— mov rax, qword ptr [rip + 0xfd135] ──────────────────────────────────────────────[ DISASM ]────────────────────────────────────────────── ► 0x5555555ce524 <main+3399> mov rax, qword ptr [rip + 0xfd135] <0x5555556cb660> 0x5555555ce52b <main+3406> test rax, rax 0x5555555ce52e <main+3409> jne main+3445 <main+3445> ↓ 0x5555555ce552 <main+3445> mov rax, qword ptr [rbp - 0x460] 0x5555555ce559 <main+3452> add rax, 8 0x5555555ce55d <main+3456> mov rax, qword ptr [rax] 0x5555555ce560 <main+3459> mov rdi, rax 0x5555555ce563 <main+3462> call strlen@plt strlen@plt

0x5555555ce568 <main+3467> add rax, 1 0x5555555ce56c <main+3471> cmp rax, 0x1ff 0x5555555ce572 <main+3477> jbe main+3510 <main+3510> ──────────────────────────────────────────[ SOURCE (CODE) ]─────────────────────────────────────────── In file: /home/aidai/fuzzing/model_checking/Spin-test/Src/main.c 1101 1102 if (preprocessonly) 1103 { alldone(0); 1104 } 1105 ► 1106 if (!(yyin = fopen(out1, “r”))) 1107 { printf("spin: cannot open %s\n", out1); 1108 alldone(1); 1109 } 1110 1111 assert(strlen(argv[1])+1 < sizeof(cmd)); ──────────────────────────────────────────────[ STACK ]─────────────────────────────────────────────── 00:0000│ rsp 0x7fffffffdc30 —▸ 0x7fffffffe188 —▸ 0x7fffffffe47d ◂— ‘/home/aidai/fuzzing/model_checking/Spin-test/Src/spin’ 01:0008│ 0x7fffffffdc38 ◂— 0x2f7fdb1e9 02:0010│ 0x7fffffffdc40 ◂— 0x1 03:0018│ 0x7fffffffdc48 ◂— 0x61d1ad40f7fb2a08 04:0020│ 0x7fffffffdc50 ◂— 0x0 05:0028│ 0x7fffffffdc58 ◂— 0x0 06:0030│ 0x7fffffffdc60 —▸ 0x7ffff7fac6a0 (_IO_2_1_stdout_) ◂— 0xfbad2084 07:0038│ 0x7fffffffdc68 —▸ 0x7ffff7ffd9e8 (_rtld_global+2440) —▸ 0x7ffff7fcf000 ◂— 0x10102464c457f ────────────────────────────────────────────[ BACKTRACE ]───────────────────────────────────────────── ► f 0 0x5555555ce524 main+3399 f 1 0x7ffff7de70b3 __libc_start_main+243 ────────────────────────────────────────────────────────────────────────────────────────────────────── pwndbg> p yyin $9 = (FILE *) 0x5555556d32a0 pwndbg> c Continuing. spin: ./poc.pml:1, Error: syntax error saw ‘’{’ = 123’

Hardware watchpoint 2: yyin

Old value = (FILE *) 0x5555556d32a0 New value = (FILE *) 0x5555556d32a1 lex () at spinlex.c:1707 1707 case '{’: scope_seq[scope_level++]++; set_cur_scope(); break; LEGEND: STACK | HEAP | CODE | DATA | RWX | RODATA ────────────────────────────────────────────[ REGISTERS ]───────────────────────────────────────────── *RAX 0x5555556cb460 (scope_seq) ◂— 0x100000001 RBX 0x5555556111f0 (__libc_csu_init) ◂— endbr64 *RCX 0x556d32a1 *RDX 0x200 *RDI 0x7b *RSI 0x6e *R8 0x7b *R9 0x3 *R10 0x555555619116 ◂— 0x5c00745c00625c00 *R11 0x7ffff7fabbe0 (main_arena+96) —▸ 0x5555556d7aa0 ◂— 0x0 R12 0x5555555bc660 (_start) ◂— endbr64 R13 0x7fffffffe180 ◂— 0x2 R14 0x0 R15 0x0 *RBP 0x7fffffffd300 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 —▸ 0x7fffffffe090 ◂— 0x0 *RSP 0x7fffffffd140 ◂— 0x3000000018 *RIP 0x5555555c6b08 (lex+3177) ◂— call 0x5555555c5954 ──────────────────────────────────────────────[ DISASM ]────────────────────────────────────────────── ► 0x5555555c6b08 <lex+3177> call set_cur_scope <set_cur_scope>

0x5555555c6b0d <lex+3182> jmp lex+3213 <lex+3213>

0x5555555c6b0f <lex+3184> mov eax, dword ptr [rip + 0xe13cf] <0x5555556a7ee4> 0x5555555c6b15 <lex+3190> sub eax, 1 0x5555555c6b18 <lex+3193> mov dword ptr [rip + 0xe13c6], eax <0x5555556a7ee4> 0x5555555c6b1e <lex+3199> call set_cur_scope <set_cur_scope>

0x5555555c6b23 <lex+3204> jmp lex+3213 <lex+3213>

0x5555555c6b25 <lex+3206> nop 0x5555555c6b26 <lex+3207> jmp lex+3213 <lex+3213>

0x5555555c6b28 <lex+3209> nop 0x5555555c6b29 <lex+3210> jmp lex+3213 <lex+3213> ──────────────────────────────────────────[ SOURCE (CODE) ]─────────────────────────────────────────── In file: /home/aidai/fuzzing/model_checking/Spin-test/Src/spinlex.c 1702 case '?’: c = follow('?’, R_RCV, RCV); break; 1703 case '&’: c = follow('&’, AND, ‘&’); break; 1704 case '|’: c = follow('|’, OR, ‘|’); break; 1705 case ';’: c = SEMI; break; 1706 case '.’: c = follow('.’, DOTDOT, ‘.’); break; ► 1707 case '{’: scope_seq[scope_level++]++; set_cur_scope(); break; 1708 case '}’: scope_level–; set_cur_scope(); break; 1709 default : break; 1710 } 1711 ValToken(0, c) 1712 } ──────────────────────────────────────────────[ STACK ]─────────────────────────────────────────────── 00:0000│ rsp 0x7fffffffd140 ◂— 0x3000000018 01:0008│ 0x7fffffffd148 ◂— 0x7bffffd220 02:0010│ 0x7fffffffd150 —▸ 0x7fffffffd160 —▸ 0x7fffffffd260 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 ◂— … 03:0018│ 0x7fffffffd158 ◂— 0x3f55a706937ce400 04:0020│ 0x7fffffffd160 —▸ 0x7fffffffd260 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 —▸ 0x7fffffffe090 ◂— … 05:0028│ 0x7fffffffd168 —▸ 0x7ffff7e24ebf (printf+175) ◂— mov rcx, qword ptr [rsp + 0x18] 06:0030│ 0x7fffffffd170 ◂— 0x7b /* ‘{’ */ 07:0038│ 0x7fffffffd178 ◂— 0x0 ────────────────────────────────────────────[ BACKTRACE ]───────────────────────────────────────────── ► f 0 0x5555555c6b08 lex+3177 f 1 0x5555555c7235 yylex+61 f 2 0x5555555bca8d yyparse+796 f 3 0x5555555ce8d8 main+4347 f 4 0x7ffff7de70b3 __libc_start_main+243 ────────────────────────────────────────────────────────────────────────────────────────────────────── pwndbg> x/70gx scope_seq 0x5555556cb460 <scope_seq>: 0x0000000100000001 0x0000000100000001 0x5555556cb470 <scope_seq+16>: 0x0000000100000001 0x0000000100000001 0x5555556cb480 <scope_seq+32>: 0x0000000100000001 0x0000000100000001 0x5555556cb490 <scope_seq+48>: 0x0000000100000001 0x0000000100000001 0x5555556cb4a0 <scope_seq+64>: 0x0000000100000001 0x0000000100000001 0x5555556cb4b0 <scope_seq+80>: 0x0000000100000001 0x0000000100000001 0x5555556cb4c0 <scope_seq+96>: 0x0000000100000001 0x0000000100000001 0x5555556cb4d0 <scope_seq+112>: 0x0000000100000001 0x0000000100000001 0x5555556cb4e0 <scope_seq+128>: 0x0000000100000001 0x0000000100000001 0x5555556cb4f0 <scope_seq+144>: 0x0000000100000001 0x0000000100000001 0x5555556cb500 <scope_seq+160>: 0x0000000100000001 0x0000000100000001 0x5555556cb510 <scope_seq+176>: 0x0000000100000001 0x0000000100000001 0x5555556cb520 <scope_seq+192>: 0x0000000100000001 0x0000000100000001 0x5555556cb530 <scope_seq+208>: 0x0000000100000001 0x0000000100000001 0x5555556cb540 <scope_seq+224>: 0x0000000100000001 0x0000000100000001 0x5555556cb550 <scope_seq+240>: 0x0000000100000001 0x0000000100000001 0x5555556cb560 <scope_seq+256>: 0x0000000100000001 0x0000000100000001 0x5555556cb570 <scope_seq+272>: 0x0000000100000001 0x0000000100000001 0x5555556cb580 <scope_seq+288>: 0x0000000100000001 0x0000000100000001 0x5555556cb590 <scope_seq+304>: 0x0000000100000001 0x0000000100000001 0x5555556cb5a0 <scope_seq+320>: 0x0000000100000001 0x0000000100000001 0x5555556cb5b0 <scope_seq+336>: 0x0000000100000001 0x0000000100000001 0x5555556cb5c0 <scope_seq+352>: 0x0000000100000001 0x0000000100000001 0x5555556cb5d0 <scope_seq+368>: 0x0000000100000001 0x0000000100000001 0x5555556cb5e0 <scope_seq+384>: 0x0000000100000001 0x0000000100000001 0x5555556cb5f0 <scope_seq+400>: 0x0000000100000001 0x0000000100000001 0x5555556cb600 <scope_seq+416>: 0x0000000100000001 0x0000000100000001 0x5555556cb610 <scope_seq+432>: 0x0000000100000001 0x0000000100000001 0x5555556cb620 <scope_seq+448>: 0x0000000100000001 0x0000000100000001 0x5555556cb630 <scope_seq+464>: 0x0000000100000001 0x0000000100000001 0x5555556cb640 <scope_seq+480>: 0x0000000100000001 0x0000000100000001 0x5555556cb650 <scope_seq+496>: 0x0000000100000001 0x0000000100000001 0x5555556cb660 <yyin>: 0x00005555556d32a1 0x0000000000000000 0x5555556cb670: 0x0000000000000000 0x0000000000000000 0x5555556cb680 <yytext>: 0x6d702e636f70007b 0x64003e656e69006c

poc

command

Result

./model_checking/Spin/Src/spin ./poc.pml
spin: ./poc.pml:1, Error: syntax error  saw ''{' = 123'
0 processes created

gdb

pwndbg> c Continuing.

Breakpoint 4, lex () at spinlex.c:1707 1707 case '{’: scope_seq[scope_level++]++; set_cur_scope(); break; LEGEND: STACK | HEAP | CODE | DATA | RWX | RODATA ────────────────────────────────────────────[ REGISTERS ]───────────────────────────────────────────── RAX 0x5555555c6acd (lex+3118) ◂— mov eax, dword ptr [rip + 0xe1411] RBX 0x5555556111f0 (__libc_csu_init) ◂— endbr64 *RCX 0x5555556d5520 ◂— 0x0 RDX 0x555555616628 ◂— 0xfffb04fdfffb03f0 RDI 0x7b *RSI 0x6e R8 0x7b R9 0x3 R10 0x555555619116 ◂— 0x5c00745c00625c00 R11 0x7ffff7fabbe0 (main_arena+96) —▸ 0x5555556d5520 ◂— 0x0 R12 0x5555555bc660 (_start) ◂— endbr64 R13 0x7fffffffe180 ◂— 0x2 R14 0x0 R15 0x0 RBP 0x7fffffffd300 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 —▸ 0x7fffffffe090 ◂— 0x0 RSP 0x7fffffffd140 ◂— 0x3000000018 RIP 0x5555555c6acd (lex+3118) ◂— mov eax, dword ptr [rip + 0xe1411] ──────────────────────────────────────────────[ DISASM ]────────────────────────────────────────────── ► 0x5555555c6acd <lex+3118> mov eax, dword ptr [rip + 0xe1411] <0x5555556a7ee4> 0x5555555c6ad3 <lex+3124> lea edx, [rax + 1] 0x5555555c6ad6 <lex+3127> mov dword ptr [rip + 0xe1408], edx <0x5555556a7ee4> 0x5555555c6adc <lex+3133> movsxd rdx, eax 0x5555555c6adf <lex+3136> lea rcx, [rdx*4] 0x5555555c6ae7 <lex+3144> lea rdx, [rip + 0x104972] <0x5555556cb460> 0x5555555c6aee <lex+3151> mov edx, dword ptr [rcx + rdx] 0x5555555c6af1 <lex+3154> lea ecx, [rdx + 1] 0x5555555c6af4 <lex+3157> cdqe 0x5555555c6af6 <lex+3159> lea rdx, [rax*4] 0x5555555c6afe <lex+3167> lea rax, [rip + 0x10495b] <0x5555556cb460> ──────────────────────────────────────────[ SOURCE (CODE) ]─────────────────────────────────────────── In file: /home/aidai/fuzzing/model_checking/Spin-test/Src/spinlex.c 1702 case '?’: c = follow('?’, R_RCV, RCV); break; 1703 case '&’: c = follow('&’, AND, ‘&’); break; 1704 case '|’: c = follow('|’, OR, ‘|’); break; 1705 case ';’: c = SEMI; break; 1706 case '.’: c = follow('.’, DOTDOT, ‘.’); break; ► 1707 case '{’: scope_seq[scope_level++]++; set_cur_scope(); break; 1708 case '}’: scope_level–; set_cur_scope(); break; 1709 default : break; 1710 } 1711 ValToken(0, c) 1712 } ──────────────────────────────────────────────[ STACK ]─────────────────────────────────────────────── 00:0000│ rsp 0x7fffffffd140 ◂— 0x3000000018 01:0008│ 0x7fffffffd148 ◂— 0x7bffffd220 02:0010│ 0x7fffffffd150 —▸ 0x7fffffffd160 —▸ 0x7fffffffd260 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 ◂— … 03:0018│ 0x7fffffffd158 ◂— 0x6e01a8e24c007700 04:0020│ 0x7fffffffd160 —▸ 0x7fffffffd260 —▸ 0x7fffffffd330 —▸ 0x7fffffffdc20 —▸ 0x7fffffffe090 ◂— … 05:0028│ 0x7fffffffd168 —▸ 0x7ffff7e24ebf (printf+175) ◂— mov rcx, qword ptr [rsp + 0x18] 06:0030│ 0x7fffffffd170 ◂— 0x7b /* ‘{’ */ 07:0038│ 0x7fffffffd178 ◂— 0x0 ────────────────────────────────────────────[ BACKTRACE ]───────────────────────────────────────────── ► f 0 0x5555555c6acd lex+3118 f 1 0x5555555c7235 yylex+61 f 2 0x5555555bca8d yyparse+796 f 3 0x5555555ce8d8 main+4347 f 4 0x7ffff7de70b3 __libc_start_main+243 ────────────────────────────────────────────────────────────────────────────────────────────────────── pwndbg> p scope_level $15 = -2 pwndbg> x/10gx scope_seq 0x5555556cb460 <scope_seq>: 0x0000000100000001 0x0000000000000000 0x5555556cb470 <scope_seq+16>: 0x0000000000000000 0x0000000000000000 0x5555556cb480 <scope_seq+32>: 0x0000000000000000 0x0000000000000000 0x5555556cb490 <scope_seq+48>: 0x0000000000000000 0x0000000000000000 0x5555556cb4a0 <scope_seq+64>: 0x0000000000000000 0x0000000000000000 pwndbg> x/10gx scope_seq-0x10 0x5555556cb420 <can>: 0x0000000000000000 0x0000000000000000 0x5555556cb430 <Caches>: 0x0000000000000000 0x0000000000000000 0x5555556cb440 <yynerrs>: 0xfffffffe00000001 0x00005555556d54e0 0x5555556cb450: 0x0000000100000000 0x0000000000000000 0x5555556cb460 <scope_seq>: 0x0000000100000001 0x0000000000000000 pwndbg>