CVE-2021-46168

Vulnerability

Affected versions: Spin version 6.5.1 (commit 045a0a5) contains an out-of-bounds write vulnerability in the lex() function within spinlex.c (line 1707). Specifically, the scope_seq array is declared with size 128, but the code increments scope_seq[scope_level++] without checking if scope_level exceeds 127. When a Spin Promela file contains 129 or more opening braces {, the scope_level index overflows the array, causing an out-of-bounds write. Additionally, if there are more closing braces } than opening ones, scope_level becomes negative, leading to writing before the array [1].

Exploitation

An attacker can trigger this vulnerability by providing a specially crafted Promela file to the spin parser. No authentication or special privileges are required; the attacker only needs to invoke the spin command-line tool on the malicious file. The issue is demonstrated with a PoC input containing multiple { characters. When parsed, the out-of-bounds write corrupts memory, and subsequently the fclose(yyin) call at main:1162 causes a segmentation fault [1].

Impact

Successful exploitation leads to a segmentation fault (crash) due to memory corruption. This could potentially be escalated to arbitrary code execution depending on the memory layout, but the reference only confirms a crash. The immediate impact is denial of service via application termination [1].

Mitigation

As of the reference date (January 2022), no official patch was available. Users should avoid parsing untrusted Spin Promela files with version 6.5.1. The issue was reported on GitHub [1], so users should monitor the Spin repository for a fix. No workaround is provided.