Cree: a Performant Tool for Safety Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
Access control deals with the roles and privileges to which a user is authorized, and is an important aspect of the security of a system. As enterprise access control systems need to scale to several users, roles and privileges, it is common for access control models to support delegation: a trusted security administrator is able to give semi-trusted users the ability to change portions of the authorization state. With delegation comes the danger that semi-trusted users, perhaps in collusion, may effect a state that violates enterprise policy, which in turn results in the problem called safety analysis, which is regarded as a fundamental and technically challenging problem in access control. Safety analysis is used by a trusted security administrator to answer “what if” questions before she grants privileges to a semi-trusted user. Safety analysis has been studied for various access control schemes in the literature; we address safety analysis in the context of Administrative Temporal Role-Based Access Control (ATRBAC), an administrative model for TRBAC, which is an extension to the traditional RBAC. ATRBAC has new features, which introduce new technical challenges for safety analysis: (i) a time-dimension: two new components in each administrative rule that specify in which time periods an administrative action may be effected, and a user is authorized to a role, and, (ii) two new kinds of rules for whether a role is enabled for administrative action. We propose a software tool, which we call Cree, for safety analysis of ATRBAC policies. In Cree we reduce ATRBAC-Safety to model checking and use an off-the-shelf model checker, NuSMV. The foundation for Cree is the observation from our prior work that ATRBAC safety is PSPACE. Along with an efficient reduction to model checking, we include in Cree four techniques to further improve performance: Polynomial Time Solving when possible, Forward and Backwards Pruning, Abstraction Refinement, and Bound Estimation. These are inspired by prior work, but our algorithms are different in that they address the new challenges that ATRBAC introduces. We discuss our design of Cree, and the results of a thorough empirical assessment across our approach, and five other prior tools for ATRBAC safety. Our results suggest that there are input classes for which Cree outperforms existing tools, and for the remainder, Cree's performance is no worse. We have made Cree available as open-source for public download.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.001 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.001 |
| Science and technology studies | 0.001 | 0.000 |
| Scholarly communication | 0.000 | 0.000 |
| Open science | 0.000 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it