Memory Safety in Linux Device Drivers: Enhancing Security with Formal Verification

Resumo

Resumo

Memory safety remains one of the most critical challenges in embedded systems, particularly within the Linux kernel, where device drivers are a primary source of vulnerabilities due to their close interaction with hardware and complex execution contexts. Such behavior is even more pronounced on consumer electronics devices, where restricted resources amplify the existing vulnerabilities. Traditional testing approaches, while effective at uncovering shallow bugs, often fail to guarantee the absence of subtle or deeply nested memory-safety issues. In this paper, we propose a formal verification methodology based on Bounded Model Checking (BMC) to detect memory safety violations in Linux device drivers. Using a methodology based on LSVerifier, we systematically analyzed newly integrated device drivers across multiple kernel versions. Our approach uncovered three vulnerabilities, including out-of-bounds writes, out-of-bounds reads, and null pointer dereferences. It demon strates that formal methods can uncover critical flaws early in the development process, complementing dynamic tools and strengthening kernel security.

palavras-chave

Palavras-chave

memory safetyLinux device driversformal verificationbounded model checkingkernel securitynull pointer dereferenceembedded systemsvulnerability detection

links

Links e arquivos