Verification of unloadable C modules - Soundness proof
Verification of unloadable C modules - Soundness proof
复制标题
可卸载 C 模块的验证 - 健全性证明
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
B. Jacobs;Jan Smans;Frank Piessens
C程序可以动态地加载和卸载模块。例如，某些操作系统内核支持设备驱动程序的动态加载和卸载。这导致了验证这些程序和模块的特定困难;特别是，必须验证在模块卸载后没有使用模块中的函数或全局变量。我们提出了一个分离的逻辑为基础的方法来验证这样的程序和模块。我们提出了装载和卸载模块的证明规则，并处理unfunctional模块中的函数指针，以确保可靠性，同时施加最小的验证开销。该方法基于参数化函数类型和断言闭包，两者都可以提及自己和彼此。我们提供了一个机器检查的形式化和可靠性证明，我们报告验证一个小的内核程序使用原型实现的方法在我们的验证器，VeriFast。据我们所知，我们的方法是第一个健全的模块验证的unauthorized模块。验证Uniform C模块的可靠性证明Bart Jacobs，Jan Smans，and Frank Piessens比利时鲁汶天主教大学计算机科学系{bart.jacobs，jan.smans，frank.piessens}@cs.kuleuven.be摘要。C程序可以动态地加载和卸载模块。例如，某些操作系统内核支持设备驱动程序的动态加载和卸载。这导致了验证这些程序和模块的特定困难;特别是，必须验证在模块卸载后没有使用模块中的函数或全局变量。我们提出了一个分离的逻辑为基础的方法来验证这样的程序和模块。我们提出了装载和卸载模块的证明规则，并处理unfunctional模块中的函数指针，以确保可靠性，同时施加最小的验证开销。该方法基于参数化函数类型和断言闭包，两者都可以提及自己和彼此。我们提供了一个机器检查的形式化和可靠性证明，我们报告验证一个小的内核程序使用原型实现的方法在我们的验证器，VeriFast。据我们所知，我们的方法是第一个健全的模块验证的unauthorized模块。C程序可以动态地加载和卸载模块。例如，某些操作系统内核支持设备驱动程序的动态加载和卸载。这导致了验证这些程序和模块的特定困难;特别是，必须验证在模块卸载后没有使用模块中的函数或全局变量。我们提出了一个分离的逻辑为基础的方法来验证这样的程序和模块。我们提出了装载和卸载模块的证明规则，并处理unfunctional模块中的函数指针，以确保可靠性，同时施加最小的验证开销。该方法基于参数化函数类型和断言闭包，两者都可以提及自己和彼此。我们提供了一个机器检查的形式化和可靠性证明，我们报告验证一个小的内核程序使用原型实现的方法在我们的验证器，VeriFast。据我们所知，我们的方法是第一个健全的模块验证的unauthorized模块。
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 kernellike 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. Verification of Unloadable C Modules Soundness Proof Bart Jacobs, Jan Smans, and Frank Piessens Department of Computer Science, Katholieke Universiteit Leuven, Belgium {bart.jacobs,jan.smans,frank.piessens}@cs.kuleuven.be 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. 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.