Abstract

Managing physical access control policies is a complex task. To check that policy changes do not introduce security or configuration mistakes, formal verification can be employed. Unfortunately, most existing access control policy verifiers are not designed to analyze evolving policies. They reverify the policy and all policy invariants from scratch after each small change. This is highly inefficient when dealing with evolving policies. A better approach would be to verify policies incrementally, i.e. to re-use intermediary computations from previous verification attempts. In this research, we show how policy invariants on realistic evolving physical access control systems can be verified incrementally. This is done with the help of VIATRA: an open-source incremental model query and transformation framework based on incremental graph pattern matching. Through extensive benchmarking, we conclude that incremental verification is a promising avenue to speed-up reverification.

References

1. Essay (Digital version available here)