Análisis formal del estándar NIST para modelos RBAC

Abstract

Role Based Access Control (RBAC) es un enfoque basado en el conepto de rol para implementar polï?ticas de control de acceso. Actualmente es considerado uno de los modelos mïas generales, debido a su neutralidad respecto a las polï?ticas de control de acceso y a su flexibilidad, que le permiten simular enfoques alternativos como MAC y DAC. Debido a la existencia de mïultiples variantes de modelos e implementaciones RBAC, el National Institute of Standards and Technology (NIST) realizïo una propuesta de estandarizaciïon, definiendo un modelo de referencia. Si bien la especificaciïon se desarrolla en un lenguaje de especificaciïon formal (en lenguaje Z), la propuesta no incluye un anïalisis de su correcciïon, ni la verificaciïon de propiedades de seguridad. Este artï?culo presenta un anïalisis formal, sin precedentes, de los modelos bïasico (Core RBAC) y jerïarquico (Hierarchical RBAC) del estïandar NIST, que pone en evidencia la existencia de imprecisiones, omisiones y errores en la especificaciïon de referencia. Asimsimo, este trabajo introduce una nueva especificaciïon formal de Core RBAC y Hierarchical RBAC que subsana los problemas encontrados. En torno a la nueva formalizaciïon, desarrollada en el Cïalculo de Construcciones Inductivas, se demuestran algunas propiedades relevantes de seguridad inherentes a los modelos RBAC, usando el asistente de pruebas Coq.