Verifying Compiled File System Code

9 years 5 months ago
Verifying Compiled File System Code
Abstract. This paper presents a case study on retrospective verication of the Linux Virtual File System (VFS), which is aimed at checking for violations of API usage rules and memory properties. Since VFS maintains dynamic data structures and is written in a mixture of C and inlined assembly, modern software model checkers cannot be applied. Our case study centres around our novel, verication tool, the SOCA Verier, which symbolically executes and analyses compiled code. We describe how this verier deals with complex program features such as memory access, pointer aliasing and computed jumps, while reducing manual modelling to the bare minimum. Our results show that the SOCA Verier is capable of reliably analysing complex operating system components such as the Linux VFS, thereby going beyond traditional testing tools and into niches that current software model checkers do not reach.
Jan Tobias Mühlberg, Gerald Lüttgen
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SBMF
Authors Jan Tobias Mühlberg, Gerald Lüttgen
Comments (0)