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.

• Type: Conference
• Year: 2009
• Where: SBMF
• Authors: Jan Tobias Mühlberg, Gerald Lüttgen
• Keywords: Case Study, Formal Methods, SBMF 2009, SOCA Verier, Software Model Checkers