We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The main advantage of the approach is to reason regardless of the number of users of the system in which the policy is enforced. This permits to obtain more useful results from the analysis; for instance, ensuring that sensitive permissions cannot be leaked regardless of the number of users in the system. We also briefly discuss how some heuristics make the technique scalable to handle (very) large policies. This is demonstrated by a comparative experimental evaluation with state-of-the-art tools for the analysis of access control policies.

Parameterized model checking for security policy analysis

Ranise, Silvio;Traverso, Riccardo
2016

Abstract

We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The main advantage of the approach is to reason regardless of the number of users of the system in which the policy is enforced. This permits to obtain more useful results from the analysis; for instance, ensuring that sensitive permissions cannot be leaked regardless of the number of users in the system. We also briefly discuss how some heuristics make the technique scalable to handle (very) large policies. This is demonstrated by a comparative experimental evaluation with state-of-the-art tools for the analysis of access control policies.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/307037
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact