Verifying compiled file system code |
| |
Authors: | Email author" target="_blank">Jan?Tobias?MühlbergEmail author Gerald?Lüttgen |
| |
Affiliation: | 1.Software Technologies Research Group,The University of Bamberg,Bamberg,Germany |
| |
Abstract: | This article presents a case study on retrospective verification of the Linux Virtual File System (VFS), which is aimed at
checking 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
automated software verification tool, the SOCA Verifier, which symbolically executes and analyses compiled code. We describe
how this verifier deals with complex features such as memory access, pointer aliasing and computed jumps in the VFS implementation,
while reducing manual modelling to a minimum. Our results show that the SOCA Verifier is capable of analysing the complex
Linux VFS implementation reliably and efficiently, thereby going beyond traditional testing tools and into niches that current
software model checkers do not reach. This testifies to the SOCA Verifier’s suitability as an effective and efficient bug-finding
tool during the development of operating system components. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|