A Formal Analysis Framework for Operating System Security Verification
Hao Wu · Computer Engineering and Science · 2009
By studying the characteristics of the formal verification methods and the security model of operating systems,various conditions for the application of these methods to OS security analysis are introduced.We introduce a model checking method to OS security evaluation with the benefit of the traditional theorem proving methods.In the new method,we apply theorem proving to the analysis from the security model to specifications,and the model checking method to the analysis from implementation to specifications.