Access control is one of the most fundamental security mechanisms in use today; however, the specification and management of access control policies remains a challenging problem, and today's administrators have no effective tools to assist them. This research addresses these needs and arising challenges by developing new verification techniques for access control policies, and verification tools that will help administrators specify, understand, and manage their access control policies. In particular, this research studies security analysis and insider threat assessment. Security analysis techniques answer the fundamental question of whether an access control system preserves essential security properties across changes to the authorization state. Insider threat assessment techniques determine what damages insiders can cause if they misuse the trust that has been placed on them. While focusing primarily on the widely-deployed Role-Based Access Control model, this project also aims at developing theoretical foundations and general techniques for access control policy verification. Insights obtained from this research will be applicable to other richer access control models and will help improve the understanding of the power and limitation of access control.
