Role-based Access Control Policies and Security Properties Overview
This content provides an overview of Role-based Access Control (RBAC) policies, Administrative RBAC (ARBAC) systems, and security properties in the context of access control in large organizations. It discusses the implementation of RBAC in various software systems, the assignment and revocation of rules in ARBAC, and the importance of security properties such as availability and separation of duties. The focus is on enforcing security requirements and the role-reachability problem in access control. Check out the detailed information on designing, monitoring, and verifying access control policies for organizational security.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
VAC - Verifier of Administrative Role-based Access Control Policies Anna Lisa Ferrara University of Bristol, UK P. Madhusudan University of Illinois, USA Truc Lam Nguyen Gennaro Parlato University of Southampton, UK
Role-based Access Control Policies (RBAC) p1 Professor p2 Dean p3 Student p4 PERMISSIONS ROLES USERS
Role-based Access Control Policies (RBAC) p1 Professor p2 Dean p3 Student p4 PERMISSIONS ROLES USERS implemented in several software: Microsoft SQL Servers Microsoft Active Directory SELinux Oracle DBMS ... suitable for large organizations standardized by NIST
Administrative RBAC (ARBAC) Systems r1 r2 ... rn u1 1 0 ... 1 u2 1 1 ... 0 ... ... ... ... ... Assign / Revoke rules Rules Assign (admin_role, precondition, target_role) Revoke (admin_role, precondition, target_role) conjunction of literals over the set of Roles
Security Properties Designers have security requirements availability - A doctor must always be able to access patients record separation of duties - A doctor cannot be also a receptionist escalation of privileges - A receptionist cannot be granted doctors permissions ...
Security Properties Designers have security properties in mind availability properties - A doctor must always be able to access patients record separation of duties - A doctor cannot be also a receptionist escalation of privileges - A receptionist cannot be granted doctors permissions ... Enforcing security requirements Monitoring may lead to denial-of-service attacks => policies correct by design (Automatic) verification is essential!
Security properties as Role-reachability availability properties - A doctor must always be able to access patients record separation of duties - A doctor cannot be also a receptionist escalation of privileges - A receptionist cannot be granted doctors permissions ... can be rephrased as Role-reachability Problem Can any user gain access to a given target role using Administrative RBAC rules?
Security properties as Role-reachability availability properties - A doctor must always be able to access patients record separation of duties - A doctor cannot be also a receptionist escalation of privileges - A receptionist cannot be granted doctors permissions ... can be rephrased as Role-reachability Problem Can any user gain access to a given target role using Administrative RBAC rules? PSPACE-complete!
VAC tool architecture No Error NO Abstract Transformer Integer Pgm Interproc YES Unknown Z (Z3) HSF Eldarica Input File Horn Pgm No Error NO Pruning Getafix Moped Boolean Pgm Precise Transformer YES Error NuSMV Pgm NuSMV NO C Pgm Unknown CBMC YES Counter Example Error Trace Policy-to-Program TRANSFORMER
No Error NO Abstract Transformer Integer Pgm Interproc YES Unknown Z (Z3) Input File Horn Pgm HSF Eldarica No Error NO Pruning Getafix Moped Boolean Pgm Precise Transformer YES Error NuSMV Pgm NuSMV [Ferrara, Madhusudan, Parlato - TACAS 13] - Remove roles rules, users - 90% policy size reduction NO C Pgm Unknown CBMC YES Counter Example Error Trace Policy-to-Program TRANSFORMER
No Error NO Abstract Transformer Integer Pgm Interproc YES Unknown Z (Z3) Input File Horn Pgm HSF Eldarica No Error NO Pruning Getafix Moped Boolean Pgm Precise Transformer YES Error NuSMV Pgm NuSMV NO C Pgm Unknown CBMC YES Counter Example Error Trace Policy-to-Program TRANSFORMER
[Ferrara, Madhusudan, Parlato - CSF 12] Abstractly simulate the system No Error NO Abstract Transformer Integer Pgm over- Interproc approximation YES Unknown Z (Z3) Input File Horn Pgm HSF Eldarica No Error NO Pruning Getafix Moped Boolean Pgm Precise Transformer YES Error NuSMV Pgm NuSMV NO C Pgm Unknown CBMC YES Counter Example Error Trace Policy-to-Program TRANSFORMER
No Error NO Abstract Transformer Integer Pgm Interproc YES Unknown Z (Z3) Input File Horn Pgm HSF Eldarica No Error NO complete analysis Pruning Getafix Moped Boolean Pgm Precise Transformer Precisely simulates the system YES Error NuSMV Pgm NuSMV Fundamental theorem (track k users) NO C Pgm Unknown CBMC k = # of admin roles YES [Ferrara, Madhusudan, Parlato - TACAS 13] Counter Example Error Trace Policy-to-Program TRANSFORMER
No Error NO Abstract Transformer Integer Pgm Interproc YES Unknown Z (Z3) Input File Horn Pgm HSF Eldarica No Error NO Pruning Getafix Moped Boolean Pgm Precise Transformer Precisely simulates the system YES Error NuSMV Pgm NuSMV Fundamental theorem (track k users) NO C Pgm Unknown CBMC k = # of admin roles under- YES approximation [Ferrara, Madhusudan, Parlato - TACAS 13] Counter Example Error Trace Policy-to-Program TRANSFORMER
Experimental Results (Realistic policies & Case studies) ORIGINAL POLICIES AFTER PRUNING ANALYSIS #roles #users #rules #roles #users #rules Time Violation Hospital Policies 0.099s Yes 21 50 88 3 2 1 0.099s Yes 41 100 176 4 4 2 University Policies 0.101s Yes 201 500 872 2 2 1 0.100s Yes 501 1000 2201 3 2 1 Bank Policies (case studies) 0.239s Yes 4001 10000 17536 2 2 1 2 2 1 0.844s Yes 20000 50000 81210 Three suites of complex policies 2 2 1 1.288s Yes 30000 70000 127713 2 2 1 1.586s Yes 40001 100000 176062
Conclusion VAC is a full-fledged tool o main components: pruning and translation modules o various back-ends: CBMC, Eldarica, Getafix, Interproc, Moped, NuSMV, HSF, and Z3 o counterexample generation Availability: users.ecs.soton.ac.uk/gp4/VAC.html source code, benchmarks, static Linux binaries Related tools o ASASP [Alberti, Armando, Ranise, Truong - CADE 11, STM 10] o Mohawk [Jayaraman, Tripunitara, Ganesh, Rinard, Chapin - CCS 11, TISSEC 13]
