Verification of unloadable C modules (Extended version)

Programs in unsafe languages, like C and C++, 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 present the approach we used to add support for loading and unloading modules to our separation-logic-based program verifier VeriFast. Our approach to the specification and verification of function pointer calls, based on parameterizing function types by predicates, is sound in the presence of unloading, but at the same time does not complicate the verification of programs that perform no unloading, and does not require callers to distinguish between function pointers that point into unloadable modules and ones that do not. We offer a machine-checked formalization and soundness proof and we report on verifying a small kernel-like program using VeriFast. To the best of our knowledge, ours is the first approach for sound modular verification of C programs that load and unload modules. Verification of Unloadable Modules