Model Checking Applied To Verification Of OS Kernel

Trusted OS is a base of security of computer system and Trusted Computing. Because of a kernel of OS is complicated and huge, modern software verification is limited to its ability to find hidden bug in OS kernel. As a automated verification method, Model Checking could find some errors those can't be found by other methods.In recent years, Model Checking applied to to Verification of OS Kernel have made several breakthroughs. Though there are unsettled problems, such as Model Checking complicated module in OS kernel; state explosion; handling balance between consumption of resource and code coverage. In this paper, a model system of kernel scheduler is proposed for model checking, which includes environment model based on the occasion to triggering kernel scheduler and scheduler model described by Promela. By modeling Linux2.6.11 kernel scheduler and verifying the model system in Spin, result shows that model system is effective for modeling a module with complex interfaces in operating system.