Efficient algorithmic safety analysis of HRU security models

In order to achieve a high degree of security, IT systems with sophisticated security requirements increasingly apply security models for specifying, analyzing and implementing their security policies. While this approach achieves considerable improvements in effectiveness and correctness of a system´s security properties, model specification, analysis and implementation are yet quite complex and expensive. This paper focuses on the efficient algorithmic safety analysis of HRU security models. We present the theory and practical application of a method that decomposes a model into smaller and autonomous sub-models that are more efficient to analyze. A recombination of the results then allows to infer safety properties of the original model. A security model for a real-world enterprise resource planning system demonstrates the approach.