Automated Detection of Information Leakage in Access Control

摘要: The prevention of information flow is an important concern in several access control models. Even though this property stated the model specification, it not easy to verify actual implementation a given security policy. In paper we model-check rewrite-based implementations policies. We propose general algorithm that allows one automatically identify leakage. apply our approach well-known Bell and LaPadula show its generalization proposed by McLean does protect system against