Anomaly analysis for Physical Access Control security configuration

Physical Access Controls, such as supervised doors, surveillance cameras and alarms, act as important points of demarcation between physical zones (areas/rooms) of different levels of trust. They do so by controlling personnel flow to and from areas in accordance with the enterprise security policy. A significant challenge in providing physical access control for (restricted) areas is attaining a degree of confidence that a Physical Access Control security configuration adequately addresses the threats. A misconfiguration may result in a threat of unapproved personnel access or the denial of approved personnel access to a restricted zone. In practice, Physical Access Control security configurations typically span multiple zones, involve many users and run to many thousands of access-control rules, and such complexity may increase the likelihood of misconfiguration. In this paper, a formal model for Physical Access Control security configurations is presented. This model, implemented in SAT, captures a number of unique anomalies specific to Physical Access Control domain. A preliminary set of experiments that evaluate our approach is presented.