Title: Verification of unloadable C modules - Soundness proof
Authors: Jacobs, Bart
Smans, Jan
Piessens, Frank
Issue Date: Nov-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW570
Abstract: C programs may dynamically load and unload modules. For example, some operating system kernels support dynamic loading and unloading of device drivers. This causes specific difficulties in the verification of such programs and modules; in particular, it must be verified that no functions or global variables from the module are used after the module is unloaded.

We propose a separation-logic-based approach for the verification of such programs and modules. We propose proof rules for loading and unloading modules, and for dealing with pointers to functions in unloadable modules, that ensure soundness while imposing minimal verification overhead. The approach is based on parameterized function types and assertion closures, both of which may mention themselves and each other. We offer a machine-checked formalization and soundness proof and we report on verifying a small kernel-like program using a prototype implementation of the approach in our verifier, VeriFast. To the best of our knowledge, ours is the first approach for sound modular verification of unloadable modules.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW570.pdfDocument Published 295KbAdobe PDFView/Open


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