MODEL CHECKING FOR VERIFICATION OF MANDATORY ACCESS CONTROL MODELS AND PROPERTIES

摘要: Mandatory access control (MAC) mechanisms which users or processes have to resources in a system. MAC policies are increasingly specified facilitate managing and maintaining control. However, the correct specification of is very challenging problem. To formally precisely capture security properties that should adhere to, models usually written bridge rather wide gap abstraction between mechanisms. In this paper, we propose general approach for property verification models. The defines standardized structure models, providing both automated generation test cases. expresses language model checker generic language. Then uses verify integrity, coverage, confinement these finally generates cases via combinatorial covering array system implementations