Title: Verifying compiled file system code
Authors: Mühlberg, Jan Tobias ×
Lüttgen, Gerald #
Issue Date: 20-Aug-2011
Publisher: Springer Verlag
Series Title: Formal Aspects of Computing vol:24 issue:3 pages:375-391
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.
ISSN: 0934-5043
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Non-KU Leuven Association publications
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
facj-2010.pdfMain article Published 1487KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science