Liferay is the leading opensource portal for the enterprise, implementing a role-based access control (RBAC) mechanism for user and content management. Despite its critical importance, however, the access control system implemented in Liferay is poorly documented and lacks automated tools to assist portal administrators in configuring it correctly. To make matters worse, although strongly based on the RBAC model and named around it, the access control mechanism implemented in Liferay has a number of unconventional features, which significantly complicate verification. In this paper we introduce a formal semantics for Liferay RBAC and we propose a verification technique based on abstract model-checking, discussing sufficient conditions for the soundness and the completeness of the analysis. We then present a tool, called LifeRBAC, which implements our theory to verify the security of real Liferay portals. We show that the tool is effective at proving the absence of security flaws, while efficient enough to be of practical use.

Formal verification of Liferay RBAC

CALZAVARA, STEFANO;Rabitti, Alvise;BUGLIESI, Michele
2015-01-01

Abstract

Liferay is the leading opensource portal for the enterprise, implementing a role-based access control (RBAC) mechanism for user and content management. Despite its critical importance, however, the access control system implemented in Liferay is poorly documented and lacks automated tools to assist portal administrators in configuring it correctly. To make matters worse, although strongly based on the RBAC model and named around it, the access control mechanism implemented in Liferay has a number of unconventional features, which significantly complicate verification. In this paper we introduce a formal semantics for Liferay RBAC and we propose a verification technique based on abstract model-checking, discussing sufficient conditions for the soundness and the completeness of the analysis. We then present a tool, called LifeRBAC, which implements our theory to verify the security of real Liferay portals. We show that the tool is effective at proving the absence of security flaws, while efficient enough to be of practical use.
2015
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
File in questo prodotto:
File Dimensione Formato  
essos15.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 380.87 kB
Formato Adobe PDF
380.87 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA 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: https://hdl.handle.net/10278/3679815
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
social impact