Automated Analysis Of Access Control Policies
Automated Analysis of Access Control PoliciesAlessandro Armandojoint work with Silvio RaniseArtificial Intelligence Laboratory (AI-Lab)Security & Trust Research UnitDIST, University of GenovaFBK-IRSTGenovaTrentoA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20111 / 52
Access ControlThe process ofmediating requests to resources maintained by a system anddetermining whether a request should be granted or deniedCrucial role in system securityUsually separation betweenpolicies specified by a language with an underlying modelmechanisms enforcing policiesSeparation impliesprotection requirements are independent of their implementationsecurity policies can be analyzed abstractlyA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20112 / 52
Role-based Access rlieCharlieDavidDavidDavidEveEveFredFredGregA. Armando (U. of Genova & ymUseGymAutomated Analysis of Access ControlVTSA11, Sept. 23, 20113 / 52
Role-based Access ControlUser Assignment (UA)UserRoleAlicePCMemberBobFacultyCharlie regUMemberA. Armando (U. of Genova & FBK-IRST)Permission Assignment (PA)RolePermissionPCMember GrantTenurePCMember AssignGradesPCMember ReceiveHBenefitsPCMember GymUEmployee ReceiveHBenefitsUEmployee seGymAutomated Analysis of Access ControlVTSA11, Sept. 23, 20113 / 52
Role-based Access ControlUser Assignment (UA)UserRoleAlicePCMemberBobFacultyCharlie regUMemberPermission Assignment (PA)RolePermissionPCMember loyee ymPCMemberPTEmployeeFTEmployeeUEmployeeRole Hierarchy ( )A. Armando (U. of Genova & FBK-IRST)FacultyAutomated Analysis of Access ControlTAStudentUMemberVTSA11, Sept. 23, 20113 / 52
Administrative RBACChanges to RBAC policies subject to administrative policy.Several administrative models for RBAC: ARBAC97, SARBAC,Oracle DBMS, UARBAC, .Key issue: definition of administrative domains, e.g.ARBAC: admin. domain role-basedUARBAC: admin. domain attribute-basedA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20114 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} emberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} emberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} ntPTEmployeeUMemberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} ntPTEmployeeUMemberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} ntPTEmployeeUMemberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
ARBAC97: URA97 sub-modelIn URA97, administrative actions can onlymodify the User Assignment (UA) relation.can assign:UEmployee : {Student, TA} PTEmployeecan revoke:UEmployee : {Student} eUMemberStatic Mutually Exclusive Roles (SMER):SMER(TA, PTEmployee)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20115 / 52
Administering Access Control Policies(A)RBAC model simplifies specification and administration ofaccess control policies.Yet, in large systems (e.g., Dresdner bank: 40,000 users and1,400 permissions), administration of RBAC policies can be verydifficult.Question: Starting fron an initial RBAC policy and using theadministrative actions in the ARBAC policy, is there a way to grantAlice access to salaries.xls?To predict the effects of changes on policies of real-worldcomplexity by manual inspection is unfeasible:automated support needed!A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20116 / 52
URA97: security analysis problemsLet ψ be an administrative policy.1(Bounded) user-role reachability problem: Given (an integerk 0, resp.) an initial RBAC policy, and a role r , does there exista sequence of administrative actions in ψ (of length k , resp)assigning a user u to role r ?2Role containment: Given an initial RBAC policy and two roles r1and r2 , does every member of role r1 also belong to role r2 in allreachable policies by applying finite sequences of administrativeactions in ψ?3Weakest precondition: Given a user u and a role r , compute theminimal set of RBAC policies from which a sequence ofadministrative actions in ψ can make u a member of role r .4Inductive policy invariant: Check if a property remain unaffectedunder any (finite) sequence of administrative actions in ψ.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20117 / 52
Symbolic Reachability Analysis of ARBACPolicies12345A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proc. of 6th Intl. Workshop onSecurity and Trust Management (STM’10), Athens, September 23-24, 2010.F. Alberti, A. Armando, and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Attribute-basedRBAC-Policies. In Proc. of 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS2011), Hong Kong, March 22-24, 2011.A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies. In theProceedings of the 7th International Workshop on Security and Trust Management (STM’11), Copenhagen (Denmark),July 27-28, 2011.F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Administrative Policies. In Proc. of23rd Intl. Conf. on Automated Deduction (CADE-23), Wroclaw (Poland), Jul 31-Aug 5, 2011.A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies. In theProceedings of the 7th International Workshop on Security and Trust Management, Copenhagen (Denmark), July 27-28,2011.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 20118 / 52
Symbolic Representation of RBAC PoliciesSymbolic representation of RBAC policies and properties, using adecidable fragment of (many-sorted) first-order logic.Sorts: User , RolePredicate symbols: ua : User Role (flexible) : Role Role (rigid) Defining ua: u, r .(ua(u, r ) (u u1 r Role 1) (u u2 r Role 2) )(u u3 r Role 3) .Defining :PCMemberTA Student,PTEmployee UEmployee,UEmployee UMember , .,PTEmployeeFTEmployeeFacultyUEmployee r .(r r ) r1 , r2 , r3 .((r1 r2 r2 r3 ) r1 r3 ) r1 , r2 .((r1 r2 r2 r1 ) r1 r2 )A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlTAStudentUMemberVTSA11, Sept. 23, 20119 / 52
Symbolic Representation of RBAC PoliciesSMER Constraints: No user can be TA and PTEmployee at thesame time: u. (ua(u, TA) ua(u, PTEmployee))Queries: There exists a user who is member of a certain role: u, r .(ua(u, r ) r Student)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201110 / 52
Symbolic Representation of ARBAC PoliciesUEmployee : {Student, TA} PTEmployee ua , ra .(ua(ua , ra ) ra UEmployee) ua(u, Student) r2 .(r2 TA ua(u, r2 )) u. x, y .(ua0 (x, y ) ((x u y PTEmployee) ua(x, y )))UEmployee : {Student} Student ua , ra .(ua(ua , ra ) ra UEmployee) r1 .(ua(u, r1 ) r1 Student) u. x, y .(ua0 (x, y ) ( (x u y Student) ua(x, y )))A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201111 / 52
Security analysis: bounded user-role reachabilityGiven an integer k 0 and symbolic representation ofTRBAC theory constraining RBAC policies ( , SMER constraints)I(ua) initial RBAC policyG(ua) user u is a member of role rτ (ua, ua0 ) administrative actions in ψCheck the satisfiability ofTRBAC I(ua0 ) τ (ua0 , ua1 ) · · · τ (uak 1 , uak ) G(uak )Can be reduced to the satisfiability ofBernays-Shönfinkel-Ramsey formulae Decidable!A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201112 / 52
Security analysis: unbounded user-role reachability (I)Given symbolic representation ofTRBAC theory constraining RBAC policiesI(ua) initial RBAC policyG(ua) user u is a member of role rτ (ua, ua0 ) administrative actions in ψRun a symbolic backward reachability procedureR0 (ua) : G(ua) (goal)Ri 1 (ua) : ua0 .(Ri (ua0 ) τ (ua, ua0 )) (pre-image) for i 0Three requirements123Effective computation of BSR formulae for pre-imagesDecidability of satisfiability of (Ri I) (safety) and validity of(Ri 1 Ri ) (fix-point), both modulo TRBACTermination of backward reachabilityA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201113 / 52
Security analysis: unbounded user-role reachability (II)Effective computation of pre-imagesif pre-processing of negation in pre-conditions ofadministraitve actions to eliminate Satisfiability of (Ri I) and validity of (Ri 1 Ri ) modulo TRBACcan be reduced to satisfiability of BSR formulae Decidable!Termination of backward reachabilityby model-theoretic methods in combination withresults on well-quasi-orderA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201114 / 52
Security analysis: theoretical results, overviewDecidability of parameterized user-role reachabilitywith respect to the number of usersRole containment and weakest precondition can be reduced tounbounded user-role reachabilityInductive policy invariant can be reduced to bounded user-rolereachabilityExtensionsParametric roles (limited use of negation in pre-conditions ofadministrative actions)Attributes (crucial for distributed and open environments)A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201115 / 52
Security analysis: practical results, overview (I)joint work with Francesco AlbertiTool ASASP: Automated Symbolic Analysis of Administrative Policiesarchitecture: client-serverclient: pre-image computation generation of logical problemsserver: state-of-the-art SMT solvers and theorem provers onsatisfiability problems.Z3, incomplete over BSR but incrementalSPASS (refutation) complete but not incrementalhierarchical combinationBenchmarks for unbounded user-role reachability by Stoller et alParameter: goal sizeBetter scalability wrt. tool by Stoller et alTool and benchmarks publicly available at http://st.fbk.euA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201116 / 52
Security analysis: practical results, overview (II)1000ASASPStoller100No role hierarchyTime (sec)1010.10.0112345678Goal sizeA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201117 / 52
Security analysis: practical results, overview (III)With role hierarchyGoal size 1Goal size 210Time (sec)Time (sec)10.1ASASP AxiomASASP CompiledStoller0.010510152025ASASP AxiomASASP CompiledStoller10.13005Hierarchy depthA. Armando (U. of Genova & FBK-IRST)1015202530Hierarchy depthAutomated Analysis of Access ControlVTSA11, Sept. 23, 201118 / 52
Security analysis: practical results, overview (IV)With role hierarchyGoal size 310Goal size 4100ASASP AxiomASASP CompiledStollerTime (sec)Time (sec)10110.1ASASP AxiomASASP CompiledStoller0.105101520253005Hierarchy depthA. Armando (U. of Genova & FBK-IRST)1015202530Hierarchy depthAutomated Analysis of Access ControlVTSA11, Sept. 23, 201119 / 52
Symbolic Reachability Analysis of PersonalHealth Record Policies1A. Armando, R. Carbone, and S. Ranise. Automated Analysis of Semantic-AwareAccess Control Policies: a Logic-Based Approach. In the Proceedings of the IEEEWorkshop on Semantic Computing for Security and Privacy, San Francisco (USA),September 21, 2011.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201120 / 52
Access Control in Online Distributed EnvironmentsIncreasingly large number of security-sensitive applications fore-business, e-health, and e-government are available androutinely used by the general public.Regulate the access to sensitive data (e.g., health records)handled by these applications is a growing concern.Traditional access control models are unsatisfactory:Policy Administration: Separation between policy and policyadministration is usually assumed (c.f. ARBAC).Policy Integration: With the advent of the SaaS paradigm, usersmay give third-party applications access to their own data.The policy may thus span several applications.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201121 / 52
ProjectHealth Design and TreCA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201122 / 52
Regulating Access to PHRsUnderstanding the implications of the PHRs policies goes beyondthe ability of a security administrator, let alone an average user.Automatic analysis techniques and tools for policies are thereforekey.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201123 / 52
An Access Control Model for Personal Health RecordsAn access control policy of user uo is a tuple π (uo , U, R, P, UA, PA),whereU is the set of the user accounts and uo U;R is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereAct is a set of actions endowed with the hierarchy relation wAct ;Res is the set of resources endowed with the hierarchy relationwRes .PA ((U R) P) is the permission assignment relation.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsAn access control policy of user uo is a tuple π (uo , U, R, P, UA, PA),whereU is the set of the user accounts and uo U;R is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereAct is a set of actions endowed with the hierarchy relation wAct ;Res is the set of resources endowed with the hierarchy relationwRes .PA ((U R) P) is the permission assignment relation.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsParentRole HierarchyAn access control policy of user uo is a tuple π (uo , U, R, P,ChildUA, PA),whereFamilyMemberSiblingU is the set of the user accounts and uo U;PhysicianR is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;HealthCareProviderP (Act Res) isthe set of permissions, Act is a set of actions endowed with the hierarchy relation .wAct ;ExternalApplicationRes is the set of resources endowedwith the hierarchy relationHISSystemwRes .TrustedHealthPlanPA ((U R) P) is the permission assignment relation.LaboratorySystemA. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsAn access control policy of user uo is a tuple π (uo , U, R, P, UA, PA),whereU is the set of the user accounts and uo U;R is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereAct is a set of actions endowed with the hierarchy relation wAct ;Res is the set of resources endowed with the hierarchy relationwRes .PA ((U R) P) is the permission assignment relation.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsAn access control policy of user uo is a tuple π (uo , U, R, P, UA, PA),whereU is the set of the user accounts and uo U;R is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereAct is a set of actions endowed with the hierarchy relation wAct ;Res is the set of resources endowed with the hierarchy relationwRes .PA ((U R) P) is the permission assignment relation.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsAn access control policy of user uo is a tuple π (uo , U, R, P, UA, PA),whereU is the set of the user accounts and uo U;R is a set of roles endowed with the hierarchy relation wR ;UA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereAct is a set of actions endowed with the hierarchy relation wAct ;Res is the set of resources endowed with the hierarchy relationwRes .PA ((U R) P) is the permission assignment relation.A. Armando (U. of Genova & FBK-IRST)Automated Analysis of Access ControlVTSA11, Sept. 23, 201124 / 52
An Access Control Model for Personal Health RecordsInsertRecordAction HierarchyAn access control policy of user uo is a tuple π (uo ,AnnotateRecordU, R, P, UA, PA),whereUpdateRecordRecordModificationU is the set of the user accounts and uo U;DeleteRecordR is a set of roles endowed with the hierarchy relation wR ;MaskRecordUA (U R) is the user-role assignment relation;P (Act Res) is the set of permissions, whereReadRecordRecordViewingReadAnnotationAct is a set of actionsendowed with the hierarchyrel
Automated Analysis of Infinite State Workflows with Access Control Policies. In the Proceedings of the 7th International Workshop on Security and Trust Management, Copenhagen (Denmark), July 27-28, 2011. A. Armando (
Automated Micrometer Automated Balance or Interface for Existing Balance Gamlen D500 or D1000 Automated Dashboard Software GamPette Powder Dispenser Gamlen Tablet Tensile Analyser (TTA) Automated Micrometer Automated Balance or Interface for Existing Balance Ideally suited to users with some experience of compaction analysis
Highly automated driving, Dr. René Grosspietsch, 04.09.2015. Seite 5 HOWEVER TRUE AUTOMATED DRIVING STILL MEANS A BIG STEP BECAUSE OF RESPONSIBILITY SWITCH. Source: SAE, VDA, LT-Analyse Readiness to take over / "Eyes-off" Full control 1 Assisted 2 Partly automated 3 Highly automated 4 Autonomous 5 Driverless Autonomous No driver 0 Driver .
of automated container terminals (ACTs), equipped with automated container transshipment systems (consisting of automated cranes and automated guided vehicles etc.), that can meet rapidly increasing demands for higher oper-ational efficiency, lower costs, and smaller variability than what traditional terminals can achieve. There are four
to launch. Qualifier features automated data download via Cell / WiFi, automated data processing, remote data logger configuration update, issue notifications via SMS & Email, automated reports, embedded analysis
12 City Mobil2 in ERTRAC (2015) Automated Driving Roadmap. 7 1.3 Automated Driving in Europe The EU has a long history of investing in research projects contributing to automated . Consulting Group (2015). Revolution in the Driver’s Seat: The Road to Autonomous Vehicles in ERTRAC (2015) Automated Dri
digital road infrastructure for automated driving . ACEA works on a Roadmap for the Deployment of Higher Levels of Automated Driving. . Piloting Automated Driving on European Roads . Objective. Demonstrate automated driving in com
automated driving: Highway autopilot, highly automated freight vehicles on dedicated roads, automated public rapid transit/shuttles in mixed traffic, robot taxis, and driverless maintenance and road works vehicles. The report describes the automated driving
Table of Contents Introduction 1 Brief Background on Automated Vehicles 1 The Role of State Highway Offices 4 State Behavioral Highway Safety Programs and Partnerships 4 State Highway Safety Offices and Automated Vehicles 5 Current State Automated Vehicle Activities 6 Legislation 6 Testing and Deployment 6 Automated Ve
