Detection of the Operating System Configuration Vulnerabilities with Safety Evaluation Facility

摘要

In this paper, we address to formal verification methodologies and the system analyzing facility to verify property of the operating systems safety. Using our technique it becomes possible to discover security drawbacks in any IT-system based on access control model of 'state machine' style. Through our case study of model checking in Sample Vulnerability Checking (SVC), we show how the evaluation tool can be applied in Microsoft Windows 2000 to specify and verify safety problem of system security.