Verification of Unloadable Modules
Verification of Unloadable Modules
复制标题
可卸载模块的验证
DOI：
10.1007/978-3-642-21437-0_30
复制
发表时间：
2011
影响因子：
0.5
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
B. Jacobs;Jan Smans;Frank Piessens
不安全语言(如C和C++)中的程序可能会动态加载和卸载模块。例如，一些操作系统内核支持设备驱动程序的动态加载和卸载。这在验证此类程序和模块时造成了特定的困难；尤其是，必须验证在卸载模块之后没有使用模块中的任何函数或全局变量。
我们介绍了用于向基于分离逻辑的程序验证器VeriFast添加对加载和卸载模块的支持的方法。我们对函数指针调用的规范和验证的方法，基于使用谓词将函数类型参数化，在存在卸载的情况下是合理的，但同时不会使不执行卸载的程序的验证复杂化，也不要求调用者区分指向可卸载模块的函数指针和不指向可卸载模块的函数指针。
我们提供了机器检查的形式化和可靠性证明，并报告了使用VeriFast验证一个小的类似内核的程序。据我们所知，我们的方法是对加载和卸载模块的C程序进行合理的模块验证的第一种方法。
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.